mirror of
https://github.com/sdiehl/wiwinwlh.git
synced 2024-09-11 12:05:25 +03:00
merge 2.1
This commit is contained in:
Stephen Diehl
parent
492b66537b
commit
8a060cbf34
1
.gitignore
vendored
1
.gitignore
vendored
@ -8,3 +8,4 @@ dist/
|
||||
*.o
|
||||
includes
|
||||
*.html
|
||||
*.agdai
|
||||
|
||||
@ -20,7 +20,7 @@ h1, h2, h3, h4, h5 {
|
||||
}
|
||||
|
||||
pre code {
|
||||
font: 15px/19px Inconsolata,Monaco,"Lucida Console",Terminal,"Courier New",Courier;
|
||||
font: 15px/19px Inconsolata, Monaco,"Lucida Console",Terminal,"Courier New",Courier;
|
||||
}
|
||||
|
||||
img {
|
||||
@ -77,6 +77,64 @@ li code, p code, table code {
|
||||
border-radius: 8px;
|
||||
}
|
||||
|
||||
/* Language Extensions Table */
|
||||
|
||||
.table-striped .verical {
|
||||
-webkit-transform: rotate(-90deg);
|
||||
-moz-transform: rotate(-90deg);
|
||||
-ms-transform: rotate(-90deg);
|
||||
-o-transform: rotate(-90deg);
|
||||
transform: rotate(-90deg);
|
||||
}
|
||||
|
||||
.table-striped .striped-header td {
|
||||
/*border-bottom: 1px solid black;*/
|
||||
}
|
||||
|
||||
.table-striped .striped-header td {
|
||||
padding-left: 10px;
|
||||
padding-right: 10px;
|
||||
font-weight: bold;
|
||||
font-size: 8pt;
|
||||
}
|
||||
|
||||
.table-striped {
|
||||
text-align: center;
|
||||
border-spacing: 0px;
|
||||
padding: 0px;
|
||||
}
|
||||
|
||||
.table-striped td:first-child {
|
||||
text-align: left;
|
||||
}
|
||||
|
||||
.table-striped td:nth-child(5) {
|
||||
text-align: left;
|
||||
padding-right: 10px;
|
||||
}
|
||||
|
||||
.table-striped td:nth-child(6) {
|
||||
text-align: left;
|
||||
padding-right: 10px;
|
||||
}
|
||||
|
||||
|
||||
.table-striped a {
|
||||
text-decoration: underline;
|
||||
}
|
||||
|
||||
.table-striped
|
||||
|
||||
.table-striped tr:nth-child(even) {
|
||||
background-color: white;
|
||||
}
|
||||
|
||||
.table-striped tr:nth-child(odd) {
|
||||
background-color: #eeeeee;
|
||||
}
|
||||
|
||||
/* */
|
||||
|
||||
.center {
|
||||
text-align: center;
|
||||
}
|
||||
@ -181,11 +239,13 @@ ul.sections > li > div {
|
||||
@media only screen and (min-width: 481px) {
|
||||
}
|
||||
|
||||
/*
|
||||
@media only screen and (max-width: 1025px) {
|
||||
.toc {
|
||||
display: none;
|
||||
}
|
||||
}
|
||||
*/
|
||||
|
||||
@media only screen and (min-width: 1025px) {
|
||||
body {
|
||||
@ -196,6 +256,19 @@ ul.sections > li > div {
|
||||
position: fixed;
|
||||
width: 270px !important;
|
||||
margin-left: 0px;
|
||||
z-index: 1000;
|
||||
}
|
||||
|
||||
.side ul ul {
|
||||
display: none;
|
||||
}
|
||||
|
||||
.side ul ul.active {
|
||||
display: block;
|
||||
}
|
||||
|
||||
.side .active {
|
||||
font-weight: bold;
|
||||
}
|
||||
|
||||
.body {
|
||||
|
||||
93
extensions.csv
Normal file
93
extensions.csv
Normal file
@ -0,0 +1,93 @@
|
||||
,Benign,Historical,Extends Syntax,Use,Use,GHC Reference
|
||||
AllowAmbiguousTypes,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#ambiguity
|
||||
Arrows,,,✓,Specialized,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/arrow-notation.html
|
||||
AutoDeriveTypeable,,,,Specialized,Metaprogramming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/deriving.html#auto-derive-typeable
|
||||
BangPatterns,✓,,✓,General,Strictness Annotation,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/bang-patterns.html
|
||||
CApiFFI,,,,Specialized,FFI,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/ffi.html#ffi-capi
|
||||
ConstrainedClassMethods,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#class-method-types
|
||||
ConstraintKinds,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/constraint-kind.html
|
||||
CPP,✓,,✓,General,Preprocessor,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/options-phases.html#c-pre-processor
|
||||
DataKinds,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/promotion.html
|
||||
DatatypeContexts,,✓,✓,Deprecated,Deprecated,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/data-type-extensions.html#datatype-contexts
|
||||
DefaultSignatures,✓,,,Specialized,Generic Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#class-default-signatures
|
||||
DeriveDataTypeable,✓,,,General,Generic Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/deriving.html#deriving-typeable
|
||||
DeriveFoldable,✓,,,General,Generic Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/deriving.html#deriving-typeable
|
||||
DeriveFunctor,✓,,,General,Generic Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/deriving.html#deriving-typeable
|
||||
DeriveGeneric,✓,,,General,Generic Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/deriving.html#deriving-typeable
|
||||
DeriveTraversable,✓,,,General,Generic Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/deriving.html#deriving-typeable
|
||||
DisambiguateRecordFields,✓,,✓,Specialized,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#disambiguate-fields
|
||||
DoRec,,✓,✓,Specialized,Syntax Extension,http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/syntax-extns.html#recursive-do-notation
|
||||
EmptyCase,,,,Specialized,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#empty-case
|
||||
EmptyDataDecls,✓,,,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/data-type-extensions.html#nullary-types
|
||||
ExistentialQuantification,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/data-type-extensions.html#existential-quantification
|
||||
ExplicitForAll,,,✓,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#explicit-foralls
|
||||
ExplicitNamespaces,✓,,✓,Specialized,Syntax Disambiguation,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#explicit-namespaces
|
||||
ExtendedDefaultRules,✓,,,Specialized,Generic Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/interactive-evaluation.html#extended-default-rules
|
||||
FlexibleContexts,,,,General,Typeclass Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#flexible-contexts
|
||||
FlexibleInstances,,,,General,Typeclass Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#instance-rules
|
||||
ForeignFunctionInterface,,,✓,General,FFI,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/ffi.html
|
||||
FunctionalDependencies,,,,General,Typeclass Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#functional-dependencies
|
||||
GADTs,,,,General,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/data-type-extensions.html#gadt
|
||||
GADTSyntax,,,✓,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/data-type-extensions.html#gadt-style
|
||||
GeneralizedNewtypeDeriving,,,,General,Typeclass Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/deriving.html#newtype-deriving
|
||||
GHCForeignImportPrim,,,,Specialized,FFI,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/ffi.html#ffi-prim
|
||||
ImplicitParams,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#implicit-parameters
|
||||
ImpredicativeTypes,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#impredicative-polymorphism
|
||||
IncoherentInstances,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#instance-overlap
|
||||
InstanceSigs,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#instance-sigs
|
||||
InterruptibleFFI,,,,Specialized,FFI,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/ffi.html#ffi-interruptible
|
||||
KindSignatures,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#kinding
|
||||
LambdaCase,✓,,✓,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#lambda-case
|
||||
LiberalTypeSynonyms,,,,Specialized,Typeclass Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/data-type-extensions.html#type-synonyms
|
||||
MagicHash,,,,Specialized,GHC Internals,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#magic-hash
|
||||
MonadComprehensions,,,✓,Specialized,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#monad-comprehensions
|
||||
MonoPatBinds,,,,Specialized,Type Disambiguation,http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/monomorphism.html
|
||||
MultiParamTypeClasses,✓,,,General,Typeclass Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#multi-param-type-classes
|
||||
MultiWayIf,,,✓,Specialized,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#multi-way-if
|
||||
NamedFieldPuns,,,✓,Specialized,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#record-puns
|
||||
NegativeLiterals,,,,General,Type Disambiguation,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#negative-literals
|
||||
NoImplicitPrelude,,,,Specialized,Import Disambiguation,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#rebindable-syntax
|
||||
NoMonoLocalBinds,,,,General,Type Disambiguation,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#mono-local-binds
|
||||
NoMonomorphismRestriction,,,,General,Type Disambiguation,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#monomorphism
|
||||
NPlusKPatterns,,✓,✓,Deprecated,Deprecated,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#n-k-patterns
|
||||
NullaryTypeClasses,,,,Specialized,Typeclass Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#nullary-type-classes
|
||||
NumDecimals,,,,General,Type Disambiguation,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#num-decimals
|
||||
OverlappingInstances,,,,Specialized,Typeclass Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#instance-overlap
|
||||
OverloadedLists,,,✓,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#overloaded-lists
|
||||
OverloadedStrings,,,,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#overloaded-strings
|
||||
PackageImports,,,✓,General,Import Disambiguation,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#package-imports
|
||||
ParallelArrays,,,,Specialized,Data Parallel Haskell,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/lang-parallel.html
|
||||
ParallelListComp,,,✓,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#parallel-list-comprehensions
|
||||
PatternGuards,,,✓,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#pattern-guards
|
||||
PatternSynonyms,✓,,✓,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#pattern-synonyms
|
||||
PolyKinds,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/kind-polymorphism.html
|
||||
PolymorphicComponents,,✓,,Specialized,Deprecated,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#universal-quantification
|
||||
PostfixOperators,✓,,✓,Specialized,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#postfix-operators
|
||||
QuasiQuotes,,,,Specialized,Metaprogramming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/template-haskell.html#th-quasiquotation
|
||||
Rank2Types,,✓,,Specialized,Historical Artificat,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#universal-quantification
|
||||
RankNTypes,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#universal-quantification
|
||||
RebindableSyntax,,,✓,Specialized,Metaprogramming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#rebindable-syntax
|
||||
RecordPuns,✓,,✓,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#record-puns
|
||||
RecordWildCards,✓,,✓,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#record-wildcards
|
||||
RecursiveDo,,,,Specialized,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#recursive-do-notation
|
||||
RelaxedPolyRec,,,,Specialized,Type Disambiguation,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#typing-binds
|
||||
Role Annotations,,,,Specialized,Type Disambiguation,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/roles.html
|
||||
Safe,,,,Specialized,Security Auditing,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/safe-haskell.html
|
||||
Safe Imports,,,,Specialized,Security Auditing,
|
||||
ScopedTypeVariables,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/other-type-extensions.html#scoped-type-variables
|
||||
StandaloneDeriving,✓,,✓,General,Typeclass Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/deriving.html#stand-alone-deriving
|
||||
TemplateHaskell,✓,,✓,Specialized,Metaprogramming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/template-haskell.html
|
||||
TraditionalRecordSyntax,,✓,✓,Specialized,Historical Artificat,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#traditional-record-syntax
|
||||
TransformListComp,,,✓,Specialized,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#generalised-list-comprehensions
|
||||
Trustworthy,,,,Specialized,Security Auditing,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/safe-haskell.html
|
||||
TupleSections,✓,,,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#tuple-sections
|
||||
TypeFamilies,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-families.html
|
||||
TypeHoles,✓,,,General,Interactive Typing,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/typed-holes.html
|
||||
TypeOperators,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/data-type-extensions.html#type-operators
|
||||
TypeSynonymInstances,✓,,,General,Typeclass Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#flexible-instance-head
|
||||
UnboxedTuples,,,,Specialized,FFI,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/primitives.html#unboxed-tuples
|
||||
UndecidableInstances,,,,Specialized,Typelevel Programming,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-class-extensions.html#undecidable-instances
|
||||
UnicodeSyntax,,,✓,Specialized,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#unicode-syntax
|
||||
UnliftedFFITypes,,,,Specialized,FFI,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/primitives.html
|
||||
Unsafe,,,,Specialized,Security Auditing,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/safe-haskell.html
|
||||
ViewPatterns,✓,,✓,General,Syntax Extension,http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/syntax-extns.html#view-patterns
|
||||
|
1011
extensions.html
Normal file
1011
extensions.html
Normal file
File diff suppressed because it is too large
Load Diff
5
img/graph1.dot
Normal file
5
img/graph1.dot
Normal file
@ -0,0 +1,5 @@
|
||||
digraph graphname {
|
||||
a -> b;
|
||||
b -> c;
|
||||
c -> a;
|
||||
}
|
||||
BIN
img/graph1.png
Normal file
BIN
img/graph1.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 8.4 KiB |
11
img/graph2.dot
Normal file
11
img/graph2.dot
Normal file
@ -0,0 +1,11 @@
|
||||
digraph ex2 {
|
||||
a -> b;
|
||||
b -> c;
|
||||
c -> a;
|
||||
|
||||
d -> e;
|
||||
e -> f;
|
||||
e -> e;
|
||||
f -> d;
|
||||
f -> e;
|
||||
}
|
||||
BIN
img/graph2.png
Normal file
BIN
img/graph2.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 17 KiB |
BIN
img/matrix.png
Normal file
BIN
img/matrix.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 28 KiB |
1084
img/matrix.svg
Normal file
1084
img/matrix.svg
Normal file
File diff suppressed because it is too large
Load Diff
|
After Width: | Height: | Size: 54 KiB |
10
includes.hs
10
includes.hs
@ -1,3 +1,5 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
-- includes.hs
|
||||
import Text.Pandoc
|
||||
|
||||
@ -8,6 +10,14 @@ doInclude cb@(CodeBlock (id, classes, namevals) contents) =
|
||||
Nothing -> return cb
|
||||
doInclude x = return x
|
||||
|
||||
doHtml :: Block -> IO Block
|
||||
doHtml cb@(CodeBlock (id, classes, namevals) contents) =
|
||||
case lookup "literal" namevals of
|
||||
Just f -> return . (RawBlock "html") =<< readFile f
|
||||
Nothing -> return cb
|
||||
doHtml x = return x
|
||||
|
||||
main :: IO ()
|
||||
main = getContents >>= bottomUpM doInclude . readMarkdown def
|
||||
>>= bottomUpM doHtml
|
||||
>>= putStrLn . writeMarkdown def
|
||||
|
||||
26
nav.js
26
nav.js
@ -15,7 +15,7 @@ Sections.prototype = {
|
||||
this.names = $('h2').map(function(idx, ele) {
|
||||
return {
|
||||
id: this.id,
|
||||
offset: $(this).offset().top - 20,
|
||||
offset: $(this).offset().top + 30,
|
||||
title: $(this).find(':header:first').html()
|
||||
};
|
||||
}).get();
|
||||
@ -35,11 +35,13 @@ Sections.prototype = {
|
||||
$el = $("[href='#" + this.names[i].id + "']");
|
||||
var s = $el.parents('ul')[0];
|
||||
|
||||
$el.addClass('active');
|
||||
// $el.addClass('active');
|
||||
|
||||
if (s !== window.section) {
|
||||
$(window.section).slideUp();
|
||||
$(s).slideDown();
|
||||
//$(window.section).slideUp();
|
||||
$(window.section).hide();
|
||||
//$(s).slideDown();
|
||||
$(s).show();
|
||||
window.section = s;
|
||||
}
|
||||
|
||||
@ -52,13 +54,15 @@ Sections.prototype = {
|
||||
if (index !== this.names.length - 1) {
|
||||
this.setLink(this.links.next, this.names[index + 1]);
|
||||
} else {
|
||||
this.links.next.slideUp(100);
|
||||
//this.links.next.slideUp(100);
|
||||
this.links.next.hide();
|
||||
}
|
||||
|
||||
if (index !== 0) {
|
||||
this.setLink(this.links.prev, this.names[index - 1]);
|
||||
} else {
|
||||
this.links.prev.slideUp(100);
|
||||
//this.links.prev.slideUp(100);
|
||||
this.links.next.hide();
|
||||
}
|
||||
},
|
||||
|
||||
@ -117,9 +121,11 @@ Page.prototype = {
|
||||
};
|
||||
|
||||
$(document).ready(function() {
|
||||
var page = new Page();
|
||||
page.scrolllast = new Date();
|
||||
if ($(window).width() > 481) {
|
||||
var page = new Page();
|
||||
page.scrolllast = new Date();
|
||||
}
|
||||
|
||||
$('.side ul ul').hide();
|
||||
$('.side ul ul').first().show();
|
||||
//$('.side ul ul').hide();
|
||||
//$('.side ul ul').first().show();
|
||||
});
|
||||
|
||||
@ -2,7 +2,7 @@
|
||||
<html lang="en">
|
||||
<head>
|
||||
<meta charset="utf-8">
|
||||
<title>What I Wish I Knew When Learning Haskell ( Stephen Diehl )</title>
|
||||
<title>What I Wish I Knew When Learning Haskell 2.1 ( Stephen Diehl )</title>
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1.0">
|
||||
<meta name="description" content="">
|
||||
<meta name="author" content="">
|
||||
@ -55,7 +55,7 @@
|
||||
</div>
|
||||
|
||||
<div class="span9 body">
|
||||
<h1>What I Wish I Knew When Learning Haskell 2.0</h1>
|
||||
<h1>What I Wish I Knew When Learning Haskell 2.1</h1>
|
||||
$body$
|
||||
</div>
|
||||
</div>
|
||||
|
||||
124
src/Antiquote.hs
Normal file
124
src/Antiquote.hs
Normal file
@ -0,0 +1,124 @@
|
||||
{-# LANGUAGE QuasiQuotes #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE DeriveDataTypeable #-}
|
||||
|
||||
module Antiquote where
|
||||
|
||||
import Data.Generics
|
||||
import Language.Haskell.TH
|
||||
import Language.Haskell.TH.Quote
|
||||
|
||||
import Text.Parsec
|
||||
import Text.Parsec.String (Parser)
|
||||
import Text.Parsec.Language (emptyDef)
|
||||
|
||||
import qualified Text.Parsec.Expr as Ex
|
||||
import qualified Text.Parsec.Token as Tok
|
||||
|
||||
data Expr
|
||||
= Tr
|
||||
| Fl
|
||||
| Zero
|
||||
| Succ Expr
|
||||
| Pred Expr
|
||||
| Antiquote String
|
||||
deriving (Eq, Show, Data, Typeable)
|
||||
|
||||
lexer :: Tok.TokenParser ()
|
||||
lexer = Tok.makeTokenParser emptyDef
|
||||
|
||||
parens :: Parser a -> Parser a
|
||||
parens = Tok.parens lexer
|
||||
|
||||
reserved :: String -> Parser ()
|
||||
reserved = Tok.reserved lexer
|
||||
|
||||
identifier :: Parser String
|
||||
identifier = Tok.identifier lexer
|
||||
|
||||
semiSep :: Parser a -> Parser [a]
|
||||
semiSep = Tok.semiSep lexer
|
||||
|
||||
reservedOp :: String -> Parser ()
|
||||
reservedOp = Tok.reservedOp lexer
|
||||
|
||||
oper s f assoc = Ex.Prefix (reservedOp s >> return f)
|
||||
|
||||
table = [ oper "succ" Succ Ex.AssocLeft
|
||||
, oper "pred" Pred Ex.AssocLeft
|
||||
]
|
||||
|
||||
expr :: Parser Expr
|
||||
expr = Ex.buildExpressionParser [table] factor
|
||||
|
||||
true, false, zero :: Parser Expr
|
||||
true = reserved "true" >> return Tr
|
||||
false = reserved "false" >> return Fl
|
||||
zero = reservedOp "0" >> return Zero
|
||||
|
||||
antiquote :: Parser Expr
|
||||
antiquote = do
|
||||
char '$'
|
||||
var <- identifier
|
||||
return $ Antiquote var
|
||||
|
||||
factor :: Parser Expr
|
||||
factor = true
|
||||
<|> false
|
||||
<|> zero
|
||||
<|> antiquote
|
||||
<|> parens expr
|
||||
|
||||
contents :: Parser a -> Parser a
|
||||
contents p = do
|
||||
Tok.whiteSpace lexer
|
||||
r <- p
|
||||
eof
|
||||
return r
|
||||
|
||||
parseExpr :: String -> Either ParseError Expr
|
||||
parseExpr s = parse (contents expr) "<stdin>" s
|
||||
|
||||
|
||||
class Expressible a where
|
||||
express :: a -> Expr
|
||||
|
||||
instance Expressible Expr where
|
||||
express = id
|
||||
|
||||
instance Expressible Bool where
|
||||
express True = Tr
|
||||
express False = Fl
|
||||
|
||||
instance Expressible Integer where
|
||||
express 0 = Zero
|
||||
express n = Succ (express (n - 1))
|
||||
|
||||
|
||||
exprE :: String -> Q Exp
|
||||
exprE s = do
|
||||
filename <- loc_filename `fmap` location
|
||||
case parse (contents expr) filename s of
|
||||
Left err -> error (show err)
|
||||
Right exp -> dataToExpQ (const Nothing `extQ` antiExpr) exp
|
||||
|
||||
exprP :: String -> Q Pat
|
||||
exprP s = do
|
||||
filename <- loc_filename `fmap` location
|
||||
case parse (contents expr) filename s of
|
||||
Left err -> error (show err)
|
||||
Right exp -> dataToPatQ (const Nothing `extQ` antiExprPat) exp
|
||||
|
||||
-- antiquote RHS
|
||||
antiExpr :: Expr -> Maybe (Q Exp)
|
||||
antiExpr (Antiquote v) = Just embed
|
||||
where embed = [| express $(varE (mkName v)) |]
|
||||
antiExpr _ = Nothing
|
||||
|
||||
-- antiquote LHS
|
||||
antiExprPat :: Expr -> Maybe (Q Pat)
|
||||
antiExprPat (Antiquote v) = Just $ varP (mkName v)
|
||||
antiExprPat _ = Nothing
|
||||
|
||||
mini :: QuasiQuoter
|
||||
mini = QuasiQuoter exprE exprP undefined undefined
|
||||
40
src/Class.hs
Normal file
40
src/Class.hs
Normal file
@ -0,0 +1,40 @@
|
||||
{-# LANGUAGE QuasiQuotes #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
|
||||
module Class where
|
||||
|
||||
import Language.Haskell.TH
|
||||
|
||||
class Pretty a where
|
||||
ppr :: a -> String
|
||||
|
||||
normalCons :: Con -> Name
|
||||
normalCons (NormalC n _) = n
|
||||
|
||||
getCons :: Info -> [Name]
|
||||
getCons cons = case cons of
|
||||
TyConI (DataD _ _ _ tcons _) -> map normalCons tcons
|
||||
con -> error $ "Can't derive for:" ++ (show con)
|
||||
|
||||
pretty :: Name -> Q [Dec]
|
||||
pretty dt = do
|
||||
info <- reify dt
|
||||
Just cls <- lookupTypeName "Pretty"
|
||||
let datatypeStr = nameBase dt
|
||||
let cons = getCons info
|
||||
let dtype = mkName (datatypeStr)
|
||||
let mkInstance xs =
|
||||
InstanceD
|
||||
[] -- Context
|
||||
(AppT
|
||||
(ConT cls) -- Instance
|
||||
(ConT dtype)) -- Head
|
||||
[(FunD (mkName "ppr") xs)] -- Methods
|
||||
let methods = map cases cons
|
||||
return $ [mkInstance methods]
|
||||
|
||||
-- Pattern matches on the ``ppr`` method
|
||||
cases :: Name -> Clause
|
||||
cases a = Clause [ConP a []] (NormalB (LitE (StringL (nameBase a)))) []
|
||||
17
src/EnumFamily.hs
Normal file
17
src/EnumFamily.hs
Normal file
@ -0,0 +1,17 @@
|
||||
module EnumFamily where
|
||||
import Language.Haskell.TH
|
||||
|
||||
enumFamily :: (Integer -> Integer -> Integer)
|
||||
-> Name
|
||||
-> Integer
|
||||
-> Q [Dec]
|
||||
enumFamily f bop upper = return decls
|
||||
where
|
||||
decls = do
|
||||
i <- [1..upper]
|
||||
j <- [2..upper]
|
||||
return $ TySynInstD bop (rhs i j)
|
||||
|
||||
rhs i j = TySynEqn
|
||||
[LitT (NumTyLit i), LitT (NumTyLit j)]
|
||||
(LitT (NumTyLit (i `f` j)))
|
||||
10
src/Insert.hs
Normal file
10
src/Insert.hs
Normal file
@ -0,0 +1,10 @@
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
|
||||
import Splice
|
||||
|
||||
spliceF
|
||||
spliceG "argument"
|
||||
|
||||
main = do
|
||||
print $ f 1 2
|
||||
print $ g ()
|
||||
101
src/Quasiquote.hs
Normal file
101
src/Quasiquote.hs
Normal file
@ -0,0 +1,101 @@
|
||||
{-# LANGUAGE QuasiQuotes #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
|
||||
module Quasiquote where
|
||||
|
||||
import Language.Haskell.TH
|
||||
import Language.Haskell.TH.Syntax
|
||||
import Language.Haskell.TH.Quote
|
||||
|
||||
import Text.Parsec
|
||||
import Text.Parsec.String (Parser)
|
||||
import Text.Parsec.Language (emptyDef)
|
||||
|
||||
import qualified Text.Parsec.Expr as Ex
|
||||
import qualified Text.Parsec.Token as Tok
|
||||
|
||||
import Control.Monad.Identity
|
||||
|
||||
data Expr
|
||||
= Tr
|
||||
| Fl
|
||||
| Zero
|
||||
| Succ Expr
|
||||
| Pred Expr
|
||||
deriving (Eq, Show)
|
||||
|
||||
instance Lift Expr where
|
||||
lift Tr = [| Tr |]
|
||||
lift Fl = [| Tr |]
|
||||
lift Zero = [| Zero |]
|
||||
lift (Succ a) = [| Succ a |]
|
||||
lift (Pred a) = [| Pred a |]
|
||||
|
||||
type Op = Ex.Operator String () Identity
|
||||
|
||||
lexer :: Tok.TokenParser ()
|
||||
lexer = Tok.makeTokenParser emptyDef
|
||||
|
||||
parens :: Parser a -> Parser a
|
||||
parens = Tok.parens lexer
|
||||
|
||||
reserved :: String -> Parser ()
|
||||
reserved = Tok.reserved lexer
|
||||
|
||||
semiSep :: Parser a -> Parser [a]
|
||||
semiSep = Tok.semiSep lexer
|
||||
|
||||
reservedOp :: String -> Parser ()
|
||||
reservedOp = Tok.reservedOp lexer
|
||||
|
||||
prefixOp :: String -> (a -> a) -> Op a
|
||||
prefixOp x f = Ex.Prefix (reservedOp x >> return f)
|
||||
|
||||
table :: [[Op Expr]]
|
||||
table = [
|
||||
[ prefixOp "succ" Succ
|
||||
, prefixOp "pred" Pred
|
||||
]
|
||||
]
|
||||
|
||||
expr :: Parser Expr
|
||||
expr = Ex.buildExpressionParser table factor
|
||||
|
||||
true, false, zero :: Parser Expr
|
||||
true = reserved "true" >> return Tr
|
||||
false = reserved "false" >> return Fl
|
||||
zero = reservedOp "0" >> return Zero
|
||||
|
||||
factor :: Parser Expr
|
||||
factor =
|
||||
true
|
||||
<|> false
|
||||
<|> zero
|
||||
<|> parens expr
|
||||
|
||||
contents :: Parser a -> Parser a
|
||||
contents p = do
|
||||
Tok.whiteSpace lexer
|
||||
r <- p
|
||||
eof
|
||||
return r
|
||||
|
||||
toplevel :: Parser [Expr]
|
||||
toplevel = semiSep expr
|
||||
|
||||
parseExpr :: String -> Either ParseError Expr
|
||||
parseExpr s = parse (contents expr) "<stdin>" s
|
||||
|
||||
parseToplevel :: String -> Either ParseError [Expr]
|
||||
parseToplevel s = parse (contents toplevel) "<stdin>" s
|
||||
|
||||
calcExpr :: String -> Q Exp
|
||||
calcExpr str = do
|
||||
filename <- loc_filename `fmap` location
|
||||
case parse (contents expr) filename str of
|
||||
Left err -> error (show err)
|
||||
Right tag -> [| tag |]
|
||||
|
||||
calc :: QuasiQuoter
|
||||
calc = QuasiQuoter calcExpr err err err
|
||||
where err = error "Only defined for values"
|
||||
54
src/Singleton.hs
Normal file
54
src/Singleton.hs
Normal file
@ -0,0 +1,54 @@
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE QuasiQuotes #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
|
||||
module Singleton where
|
||||
|
||||
import Text.Read
|
||||
import Language.Haskell.TH
|
||||
import Language.Haskell.TH.Quote
|
||||
|
||||
data Nat = Z | S Nat
|
||||
|
||||
data SNat :: Nat -> * where
|
||||
SZero :: SNat Z
|
||||
SSucc :: SNat n -> SNat (S n)
|
||||
|
||||
-- Quasiquoter for Singletons
|
||||
|
||||
sval :: String -> Q Exp
|
||||
sval str = do
|
||||
case readEither str of
|
||||
Left err -> fail (show err)
|
||||
Right n -> do
|
||||
Just suc <- lookupValueName "SSucc"
|
||||
Just zer <- lookupValueName "SZero"
|
||||
return $ foldr AppE (ConE zer) (replicate n (ConE suc))
|
||||
|
||||
stype :: String -> Q Type
|
||||
stype str = do
|
||||
case readEither str of
|
||||
Left err -> fail (show err)
|
||||
Right n -> do
|
||||
Just scon <- lookupTypeName "SNat"
|
||||
Just suc <- lookupValueName "S"
|
||||
Just zer <- lookupValueName "Z"
|
||||
let nat = foldr AppT (PromotedT zer) (replicate n (PromotedT suc))
|
||||
return $ AppT (ConT scon) nat
|
||||
|
||||
spat :: String -> Q Pat
|
||||
spat str = do
|
||||
case readEither str of
|
||||
Left err -> fail (show err)
|
||||
Right n -> do
|
||||
Just suc <- lookupValueName "SSucc"
|
||||
Just zer <- lookupValueName "SZero"
|
||||
return $ foldr (\x y -> ConP x [y]) (ConP zer []) (replicate n (suc))
|
||||
|
||||
sdecl :: String -> a
|
||||
sdecl _ = error "Cannot make toplevel declaration for snat."
|
||||
|
||||
snat :: QuasiQuoter
|
||||
snat = QuasiQuoter sval spat stype sdecl
|
||||
17
src/Splice.hs
Normal file
17
src/Splice.hs
Normal file
@ -0,0 +1,17 @@
|
||||
{-# LANGUAGE QuasiQuotes #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
|
||||
module Splice where
|
||||
|
||||
import Language.Haskell.TH
|
||||
import Language.Haskell.TH.Syntax
|
||||
|
||||
spliceF :: Q [Dec]
|
||||
spliceF = do
|
||||
let f = mkName "f"
|
||||
a <- newName "a"
|
||||
b <- newName "b"
|
||||
return [ FunD f [ Clause [VarP a, VarP b] (NormalB (VarE a)) [] ] ]
|
||||
|
||||
spliceG :: Lift a => a -> Q [Dec]
|
||||
spliceG n = runQ [d| g a = n |]
|
||||
51
src/Vector.agda
Normal file
51
src/Vector.agda
Normal file
@ -0,0 +1,51 @@
|
||||
module Vector where
|
||||
|
||||
infixr 10 _∷_
|
||||
|
||||
data ℕ : Set where
|
||||
zero : ℕ
|
||||
suc : ℕ → ℕ
|
||||
|
||||
{-# BUILTIN NATURAL ℕ #-}
|
||||
{-# BUILTIN ZERO zero #-}
|
||||
{-# BUILTIN SUC suc #-}
|
||||
|
||||
infixl 6 _+_
|
||||
|
||||
_+_ : ℕ → ℕ → ℕ
|
||||
0 + n = n
|
||||
suc m + n = suc (m + n)
|
||||
|
||||
data Vec (A : Set) : ℕ → Set where
|
||||
[] : Vec A 0
|
||||
_∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
|
||||
|
||||
_++_ : ∀ {A n m} → Vec A n → Vec A m → Vec A (n + m)
|
||||
[] ++ ys = ys
|
||||
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
|
||||
|
||||
infix 4 _≡_
|
||||
|
||||
data _≡_ {A : Set} (x : A) : A → Set where
|
||||
refl : x ≡ x
|
||||
|
||||
subst : {A : Set} → (P : A → Set) → ∀{x y} → x ≡ y → P x → P y
|
||||
subst P refl p = p
|
||||
|
||||
cong : {A B : Set} (f : A → B) → {x y : A} → x ≡ y → f x ≡ f y
|
||||
cong f refl = refl
|
||||
|
||||
vec : ∀ {A} (k : ℕ) → Set
|
||||
vec {A} k = Vec A k
|
||||
|
||||
plus_zero : {n : ℕ} → n + 0 ≡ n
|
||||
plus_zero {zero} = refl
|
||||
plus_zero {suc n} = cong suc plus_zero
|
||||
|
||||
plus_suc : {n : ℕ} → n + (suc 0) ≡ suc n
|
||||
plus_suc {zero} = refl
|
||||
plus_suc {suc n} = cong suc (plus_suc {n})
|
||||
|
||||
reverse : ∀ {A n} → Vec A n → Vec A n
|
||||
reverse [] = []
|
||||
reverse {A} {suc n} (x ∷ xs) = subst vec (plus_suc {n}) (reverse xs ++ (x ∷ []))
|
||||
26
src/abstract_constraints.hs
Normal file
26
src/abstract_constraints.hs
Normal file
@ -0,0 +1,26 @@
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
|
||||
import Data.List
|
||||
import Data.Type.Equality
|
||||
import GHC.Exts (Constraint)
|
||||
|
||||
type C1 a = (Num a, Ord a)
|
||||
type C2 a = (C1 a, Fractional a)
|
||||
|
||||
f :: C1 a => a -> a -> [a]
|
||||
f a b = sort [(a+b)^n | n <- [1..25]]
|
||||
|
||||
g :: C2 a => a -> a -> [a]
|
||||
g a b = sort [(a+b)^n | n <- [1..25]]
|
||||
|
||||
-- Translate propositional equality proof as constraint over type variables.
|
||||
type EqP a b r = ((a ~ b) => r)
|
||||
|
||||
gcastWith' :: (a :~: b) -> EqP a b r -> r
|
||||
gcastWith' Refl x = x
|
||||
|
||||
castWith' :: (a :~: b) -> a -> b
|
||||
castWith' Refl x = gcastWith' Refl x
|
||||
42
src/async.hs
Normal file
42
src/async.hs
Normal file
@ -0,0 +1,42 @@
|
||||
import Control.Monad
|
||||
import Control.Applicative
|
||||
import Control.Concurrent
|
||||
import Control.Concurrent.Async
|
||||
import Data.Time
|
||||
|
||||
timeit :: IO a -> IO (a,Double)
|
||||
timeit io = do
|
||||
t0 <- getCurrentTime
|
||||
a <- io
|
||||
t1 <- getCurrentTime
|
||||
return (a, realToFrac (t1 `diffUTCTime` t0))
|
||||
|
||||
worker :: Int -> IO Int
|
||||
worker n = do
|
||||
-- simulate some work
|
||||
threadDelay (10^2 * n)
|
||||
return (n * n)
|
||||
|
||||
-- Spawn 2 threads in parallel, halt on both finished.
|
||||
test1 :: IO (Int, Int)
|
||||
test1 = do
|
||||
val1 <- async $ worker 1000
|
||||
val2 <- async $ worker 2000
|
||||
(,) <$> wait val1 <*> wait val2
|
||||
|
||||
-- Spawn 2 threads in parallel, halt on first finished.
|
||||
test2 :: IO (Either Int Int)
|
||||
test2 = do
|
||||
let val1 = worker 1000
|
||||
let val2 = worker 2000
|
||||
race val1 val2
|
||||
|
||||
-- Spawn 10000 threads in parallel, halt on all finished.
|
||||
test3 :: IO [Int]
|
||||
test3 = mapConcurrently worker [0..10000]
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
print =<< timeit test1
|
||||
print =<< timeit test2
|
||||
print =<< timeit test3
|
||||
55
src/biplate.hs
Normal file
55
src/biplate.hs
Normal file
@ -0,0 +1,55 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
|
||||
import Data.Generics.Uniplate.Direct
|
||||
|
||||
type Name = String
|
||||
|
||||
data Expr
|
||||
= Var Name
|
||||
| Lam Name Expr
|
||||
| App Expr Expr
|
||||
deriving Show
|
||||
|
||||
data Stmt
|
||||
= Decl [Stmt]
|
||||
| Let Name Expr
|
||||
deriving Show
|
||||
|
||||
instance Uniplate Expr where
|
||||
uniplate (Var x ) = plate Var |- x
|
||||
uniplate (App x y) = plate App |* x |* y
|
||||
uniplate (Lam x y) = plate Lam |- x |* y
|
||||
|
||||
instance Biplate Expr Expr where
|
||||
biplate = plateSelf
|
||||
|
||||
instance Uniplate Stmt where
|
||||
uniplate (Decl x ) = plate Decl ||* x
|
||||
uniplate (Let x y) = plate Let |- x |- y
|
||||
|
||||
instance Biplate Stmt Stmt where
|
||||
biplate = plateSelf
|
||||
|
||||
instance Biplate Stmt Expr where
|
||||
biplate (Decl x) = plate Decl ||+ x
|
||||
biplate (Let x y) = plate Let |- x |* y
|
||||
|
||||
rename :: Name -> Name -> Expr -> Expr
|
||||
rename from to = rewrite f
|
||||
where
|
||||
f (Var a) | a == from = Just (Var to)
|
||||
f (Lam a b) | a == from = Just (Lam to b)
|
||||
f _ = Nothing
|
||||
|
||||
s, k, sk :: Expr
|
||||
s = Lam "x" (Lam "y" (Lam "z" (App (App (Var "x") (Var "z")) (App (Var "y") (Var "z")))))
|
||||
k = Lam "x" (Lam "y" (Var "x"))
|
||||
sk = App s k
|
||||
|
||||
m :: Stmt
|
||||
m = descendBi f $ Decl [ (Let "s" s) , Let "k" k , Let "sk" sk ]
|
||||
where
|
||||
f = rename "x" "a"
|
||||
. rename "y" "b"
|
||||
. rename "z" "c"
|
||||
@ -4,9 +4,9 @@ import qualified Data.ByteString as S
|
||||
import qualified Data.ByteString.Char8 as S8
|
||||
|
||||
-- From pack
|
||||
myBStr1 :: S.ByteString
|
||||
myBStr1 = S.pack ("foo" :: String)
|
||||
bstr1 :: S.ByteString
|
||||
bstr1 = S.pack ("foo" :: String)
|
||||
|
||||
-- From overloaded string literal.
|
||||
myBStr2 :: S.ByteString
|
||||
myBStr2 = "bar"
|
||||
bstr2 :: S.ByteString
|
||||
bstr2 = "bar"
|
||||
|
||||
@ -6,10 +6,10 @@ import Data.Serialize
|
||||
|
||||
import GHC.Generics
|
||||
|
||||
data Foo = A [Foo] | B [(Foo, Foo)] | C
|
||||
data Val = A [Val] | B [(Val, Val)] | C
|
||||
deriving (Generic, Show)
|
||||
|
||||
instance Serialize Foo where
|
||||
instance Serialize Val where
|
||||
|
||||
encoded :: ByteString
|
||||
encoded = encode (A [B [(C, C)]])
|
||||
@ -19,5 +19,5 @@ bytes :: [Word8]
|
||||
bytes = unpack encoded
|
||||
-- [0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,1,2,2]
|
||||
|
||||
decoded :: Either String Foo
|
||||
decoded :: Either String Val
|
||||
decoded = decode encoded
|
||||
|
||||
109
src/church_encoding.hs
Normal file
109
src/church_encoding.hs
Normal file
@ -0,0 +1,109 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE TypeSynonymInstances #-}
|
||||
|
||||
import Prelude hiding (not, succ, pred, fst, snd, tail, head)
|
||||
|
||||
type CBool = forall a. a -> a -> a
|
||||
|
||||
-- Booleans
|
||||
true, false :: CBool
|
||||
true x y = x
|
||||
false x y = y
|
||||
|
||||
-- Logic
|
||||
not p = p false true
|
||||
and p q = p q false
|
||||
or p q = p true q
|
||||
cond p x y = p x y
|
||||
xor p q = p (not q) q
|
||||
|
||||
-- Tuples
|
||||
fst p = p true
|
||||
snd p = p false
|
||||
pair a b f = f a b
|
||||
|
||||
-- Combinators
|
||||
i x = x
|
||||
k x y = x
|
||||
s x y z = x z (y z)
|
||||
|
||||
b x y z = x (y z)
|
||||
c x y z = x z y
|
||||
w x y = x y y
|
||||
|
||||
-- Church Arithmetic
|
||||
iszero n = n (\x -> false) true
|
||||
succ n f x = f (n f x)
|
||||
|
||||
plus m n f x = n f (m f x)
|
||||
sub m n = (n pred) m
|
||||
|
||||
mult m n f = m (n f)
|
||||
pow m n = n m
|
||||
pred n f x = n (\g h -> h (g f)) (\u -> x) i
|
||||
|
||||
leq m n = iszero (sub m n)
|
||||
geq m n = not (leq m n)
|
||||
|
||||
-- Church Numbers
|
||||
type CNat = forall a. (a -> a) -> a -> a
|
||||
|
||||
zero, one, two, three :: CNat
|
||||
zero f x = x
|
||||
one f x = f x
|
||||
two f x = f (f x)
|
||||
three f x = f (f (f x))
|
||||
|
||||
-- Scott Lists (lists as nested tuples)
|
||||
nil z = z
|
||||
cons x y = pair false (pair x y)
|
||||
null z = z true
|
||||
head z = fst (snd z)
|
||||
tail z = snd (snd z)
|
||||
index xs n = head (n tail xs)
|
||||
|
||||
-- data Nat = Z | S Nat
|
||||
ezero = \s z -> z
|
||||
esucc n = \s z -> s (n s z)
|
||||
|
||||
-- data Expr = Lam Expr | App Expr Expr | Var Int
|
||||
elam f = \l a v -> l f
|
||||
eapp t u = \l a v -> a t u
|
||||
evar n = \l a v -> v n
|
||||
|
||||
-- Convert between Ints and Church Numbers
|
||||
unchurch :: CNat -> Integer
|
||||
unchurch n = n (\i -> i + 1) 0
|
||||
|
||||
church :: Int -> CNat
|
||||
church n =
|
||||
if n == 0
|
||||
then zero
|
||||
else \f x -> f (church (n-1) f x)
|
||||
|
||||
unbool :: (Bool -> Bool -> t) -> t
|
||||
unbool n = n True False
|
||||
|
||||
|
||||
|
||||
ex1 :: Integer
|
||||
ex1 = unchurch (pow three three)
|
||||
-- 27
|
||||
|
||||
ex2 :: Bool
|
||||
ex2 = unbool (iszero (pred one))
|
||||
-- True
|
||||
|
||||
ex3 :: Integer
|
||||
ex3 = snd (pair 1 2)
|
||||
-- 2
|
||||
|
||||
ex4 :: Integer
|
||||
ex4 = head (tail (cons 1 (cons 2 nil)))
|
||||
-- 2
|
||||
|
||||
ex5 :: Bool
|
||||
ex5 = unbool (true `xor` false)
|
||||
-- True
|
||||
33
src/church_list.hs
Normal file
33
src/church_list.hs
Normal file
@ -0,0 +1,33 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
newtype List a = List (forall b. (a -> b -> b) -> b -> b)
|
||||
|
||||
fromList :: [a] -> List a
|
||||
fromList xs = List (\n c -> foldr n c xs)
|
||||
|
||||
toList :: List a -> [a]
|
||||
toList xs = unList xs (:) []
|
||||
|
||||
unList :: List a
|
||||
-> (a -> b -> b) -- Cons
|
||||
-> b -- Nil
|
||||
-> b
|
||||
unList (List l) = l
|
||||
|
||||
nil :: List a
|
||||
nil = List (\n c -> c)
|
||||
|
||||
cons :: a -> List a -> List a
|
||||
cons x xs = List (\n c -> n x (unList xs n c))
|
||||
|
||||
append :: List a -> List a -> List a
|
||||
append xs ys = List (\n c -> unList xs n (unList ys n c))
|
||||
|
||||
singleton :: a -> List a
|
||||
singleton x = List (\n c -> n x c)
|
||||
|
||||
length :: List a -> Integer
|
||||
length (List l) = l (\_ n -> n + 1) 0
|
||||
|
||||
test :: [Integer]
|
||||
test = toList (fromList [1,2,3] `append` fromList [4,5,6])
|
||||
63
src/closed_typefamily.hs
Normal file
63
src/closed_typefamily.hs
Normal file
@ -0,0 +1,63 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
import GHC.TypeLits
|
||||
import Data.Proxy
|
||||
import Data.Type.Equality
|
||||
|
||||
-- Type-level functions over type-level lists.
|
||||
|
||||
type family Reverse (xs :: [k]) :: [k] where
|
||||
Reverse '[] = '[]
|
||||
Reverse xs = Rev xs '[]
|
||||
|
||||
type family Rev (xs :: [k]) (ys :: [k]) :: [k] where
|
||||
Rev '[] i = i
|
||||
Rev (x ': xs) i = Rev xs (x ': i)
|
||||
|
||||
type family Length (as :: [k]) :: Nat where
|
||||
Length '[] = 0
|
||||
Length (x ': xs) = 1 + Length xs
|
||||
|
||||
type family If (p :: Bool) (a :: k) (b :: k) :: k where
|
||||
If True a b = a
|
||||
If False a b = b
|
||||
|
||||
type family Concat (as :: [k]) (bs :: [k]) :: [k] where
|
||||
Concat a '[] = a
|
||||
Concat '[] b = b
|
||||
Concat (a ': as) bs = a ': Concat as bs
|
||||
|
||||
type family Map (f :: a -> b) (as :: [a]) :: [b] where
|
||||
Map f '[] = '[]
|
||||
Map f (x ': xs) = f x ': Map f xs
|
||||
|
||||
type family Sum (xs :: [Nat]) :: Nat where
|
||||
Sum '[] = 0
|
||||
Sum (x ': xs) = x + Sum xs
|
||||
|
||||
ex1 :: Reverse [1,2,3] ~ [3,2,1] => Proxy a
|
||||
ex1 = Proxy
|
||||
|
||||
ex2 :: Length [1,2,3] ~ 3 => Proxy a
|
||||
ex2 = Proxy
|
||||
|
||||
ex3 :: (Length [1,2,3]) ~ (Length (Reverse [1,2,3])) => Proxy a
|
||||
ex3 = Proxy
|
||||
|
||||
-- Reflecting type level computations back to the value level.
|
||||
ex4 :: Integer
|
||||
ex4 = natVal (Proxy :: Proxy (Length (Concat [1,2,3] [4,5,6])))
|
||||
-- 6
|
||||
|
||||
ex5 :: Integer
|
||||
ex5 = natVal (Proxy :: Proxy (Sum [1,2,3]))
|
||||
-- 6
|
||||
|
||||
-- Couldn't match type ‘2’ with ‘1’
|
||||
ex6 :: Reverse [1,2,3] ~ [3,1,2] => Proxy a
|
||||
ex6 = Proxy
|
||||
@ -16,7 +16,7 @@ m = (100,200,200) & _3 %~ (+100)
|
||||
-- (100,200,300)
|
||||
|
||||
n :: Num a => [a]
|
||||
n = [100,200,300] & traverse %~ (+1)
|
||||
n = [100,200,300] & traverse +~ 1
|
||||
-- [101,201,301]
|
||||
|
||||
o :: Char
|
||||
@ -36,22 +36,25 @@ r = [Just 1, Just 2, Just 3] & traverse._Just +~ 1
|
||||
-- [Just 2, Just 3, Just 4]
|
||||
|
||||
s :: Maybe String
|
||||
s = Map.fromList [("foo", "bar")] ^.at "foo"
|
||||
s = Map.fromList [("foo", "bar")] ^. at "foo"
|
||||
-- "bar"
|
||||
|
||||
t :: Integral a => Maybe a
|
||||
t = "1010110" ^? binary
|
||||
-- Just 86
|
||||
|
||||
u :: RealFloat a => Complex a
|
||||
u :: Complex Float
|
||||
u = (mkPolar 1 pi/2) & _phase +~ pi
|
||||
-- 0.5 :+ 8.742278e-8
|
||||
|
||||
v :: IO [String]
|
||||
v = ["first","second","third"] ^!! folded.act ((>> getLine) . putStrLn)
|
||||
-- first
|
||||
-- a
|
||||
-- second
|
||||
-- b
|
||||
-- third
|
||||
-- c
|
||||
-- ["a","b","c"]
|
||||
v :: [Integer]
|
||||
v = [1..10] ^.. folded.filtered even
|
||||
-- [2,4,6,8,10]
|
||||
|
||||
w :: [Integer]
|
||||
w = [1, 2, 3, 4] & each . filtered even *~ 10
|
||||
-- [1, 20, 3, 40]
|
||||
|
||||
x :: Num a => Maybe a
|
||||
x = Left 3 ^? _Left
|
||||
-- Just 3
|
||||
|
||||
37
src/constraint_list.hs
Normal file
37
src/constraint_list.hs
Normal file
@ -0,0 +1,37 @@
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
import GHC.Exts (Constraint)
|
||||
|
||||
infixr 5 :::
|
||||
|
||||
data HList (ts :: [ * ]) where
|
||||
Nil :: HList '[]
|
||||
(:::) :: t -> HList ts -> HList (t ': ts)
|
||||
|
||||
type family Map (f :: a -> b) (xs :: [a]) :: [b]
|
||||
type instance Map f '[] = '[]
|
||||
type instance Map f (x ': xs) = f x ': Map f xs
|
||||
|
||||
type family Constraints (cs :: [Constraint]) :: Constraint
|
||||
type instance Constraints '[] = ()
|
||||
type instance Constraints (c ': cs) = (c, Constraints cs)
|
||||
|
||||
type AllHave (c :: k -> Constraint) (xs :: [k]) = Constraints (Map c xs)
|
||||
|
||||
showHList :: AllHave Show xs => HList xs -> [String]
|
||||
showHList Nil = []
|
||||
showHList (x ::: xs) = (show x) : showHList xs
|
||||
|
||||
instance AllHave Show xs => Show (HList xs) where
|
||||
show = show . showHList
|
||||
|
||||
example1 :: HList '[Bool, String , Double , ()]
|
||||
example1 = True ::: "foo" ::: 3.14 ::: () ::: Nil
|
||||
-- ["True","\"foo\"","3.14","()"]
|
||||
47
src/cont.hs
Normal file
47
src/cont.hs
Normal file
@ -0,0 +1,47 @@
|
||||
import Control.Monad
|
||||
import Control.Monad.Cont
|
||||
|
||||
add :: Int -> Int -> Cont k Int
|
||||
add x y = return $ x + y
|
||||
|
||||
mult :: Int -> Int -> Cont k Int
|
||||
mult x y = return $ x * y
|
||||
|
||||
contt :: ContT () IO ()
|
||||
contt = do
|
||||
k <- do
|
||||
callCC $ \exit -> do
|
||||
lift $ putStrLn "Entry"
|
||||
exit $ \_ -> do
|
||||
putStrLn "Exit"
|
||||
lift $ putStrLn "Inside"
|
||||
lift $ k ()
|
||||
|
||||
callcc :: Cont String Integer
|
||||
callcc = do
|
||||
a <- return 1
|
||||
b <- callCC (\k -> k 2)
|
||||
return $ a+b
|
||||
|
||||
ex1 :: IO ()
|
||||
ex1 = print $ runCont (f >>= g) id
|
||||
where
|
||||
f = add 1 2
|
||||
g = mult 3
|
||||
-- 9
|
||||
|
||||
ex2 :: IO ()
|
||||
ex2 = print $ runCont callcc show
|
||||
-- "3"
|
||||
|
||||
ex3 :: IO ()
|
||||
ex3 = runContT contt print
|
||||
-- Entry
|
||||
-- Inside
|
||||
-- Exit
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
ex1
|
||||
ex2
|
||||
ex3
|
||||
11
src/cont_impl.hs
Normal file
11
src/cont_impl.hs
Normal file
@ -0,0 +1,11 @@
|
||||
newtype Cont r a = Cont { runCont :: ((a -> r) -> r) }
|
||||
|
||||
instance Monad (Cont r) where
|
||||
return a = Cont $ \k -> k a
|
||||
(Cont c) >>= f = Cont $ \k -> c (\a -> runCont (f a) k)
|
||||
|
||||
class (Monad m) => MonadCont m where
|
||||
callCC :: ((a -> m b) -> m a) -> m a
|
||||
|
||||
instance MonadCont (Cont r) where
|
||||
callCC f = Cont $ \k -> runCont (f (\a -> Cont $ \_ -> k a)) k
|
||||
22
src/countargs.hs
Normal file
22
src/countargs.hs
Normal file
@ -0,0 +1,22 @@
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
import Data.Proxy
|
||||
import GHC.TypeLits
|
||||
|
||||
type family Count (f :: *) :: Nat where
|
||||
Count (a -> b) = 1 + (Count b)
|
||||
Count x = 1
|
||||
|
||||
type Fn1 = Int -> Int
|
||||
type Fn2 = Int -> Int -> Int -> Int
|
||||
|
||||
fn1 :: Integer
|
||||
fn1 = natVal (Proxy :: Proxy (Count Fn1))
|
||||
-- 2
|
||||
|
||||
fn2 :: Integer
|
||||
fn2 = natVal (Proxy :: Proxy (Count Fn2))
|
||||
-- 4
|
||||
48
src/cquote.hs
Normal file
48
src/cquote.hs
Normal file
@ -0,0 +1,48 @@
|
||||
{-# LANGUAGE QuasiQuotes #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
|
||||
import Text.PrettyPrint.Mainland
|
||||
import qualified Language.C.Syntax as C
|
||||
import qualified Language.C.Quote.CUDA as Cuda
|
||||
|
||||
cuda_fun :: String -> Int -> Float -> C.Func
|
||||
cuda_fun fn n a = [Cuda.cfun|
|
||||
|
||||
__global__ void $id:fn (float *x, float *y) {
|
||||
int i = blockIdx.x*blockDim.x + threadIdx.x;
|
||||
if ( i<$n ) { y[i] = $a*x[i] + y[i]; }
|
||||
}
|
||||
|
||||
|]
|
||||
|
||||
cuda_driver :: String -> Int -> C.Func
|
||||
cuda_driver fn n = [Cuda.cfun|
|
||||
|
||||
void driver (float *x, float *y) {
|
||||
float *d_x, *d_y;
|
||||
|
||||
cudaMalloc(&d_x, $n*sizeof(float));
|
||||
cudaMalloc(&d_y, $n*sizeof(float));
|
||||
|
||||
cudaMemcpy(d_x, x, $n, cudaMemcpyHostToDevice);
|
||||
cudaMemcpy(d_y, y, $n, cudaMemcpyHostToDevice);
|
||||
|
||||
$id:fn<<<($n+255)/256, 256>>>(d_x, d_y);
|
||||
|
||||
cudaFree(d_x);
|
||||
cudaFree(d_y);
|
||||
return 0;
|
||||
}
|
||||
|
||||
|]
|
||||
|
||||
makeKernel :: String -> Float -> Int -> [C.Func]
|
||||
makeKernel fn a n = [
|
||||
cuda_fun fn n a
|
||||
, cuda_driver fn n
|
||||
]
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
let ker = makeKernel "saxpy" 2 65536
|
||||
mapM_ (print . ppr) ker
|
||||
18
src/creal.hs
Normal file
18
src/creal.hs
Normal file
@ -0,0 +1,18 @@
|
||||
import Data.Number.CReal
|
||||
|
||||
-- algebraic
|
||||
phi :: CReal
|
||||
phi = (1 + sqrt 5) / 2
|
||||
|
||||
-- transcendental
|
||||
ramanujan :: CReal
|
||||
ramanujan = exp (pi * sqrt 163)
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
putStrLn $ showCReal 30 pi
|
||||
-- 3.141592653589793238462643383279
|
||||
putStrLn $ showCReal 30 phi
|
||||
-- 1.618033988749894848204586834366
|
||||
putStrLn $ showCReal 15 ramanujan
|
||||
-- 262537412640768743.99999999999925
|
||||
@ -2,10 +2,10 @@ import Criterion.Main
|
||||
import Criterion.Config
|
||||
|
||||
-- Naive recursion for fibonacci numbers.
|
||||
fib :: Int -> Int
|
||||
fib 0 = 0
|
||||
fib 1 = 1
|
||||
fib n = fib (n-1) + fib (n-2)
|
||||
fib1 :: Int -> Int
|
||||
fib1 0 = 0
|
||||
fib1 1 = 1
|
||||
fib1 n = fib1 (n-1) + fib1 (n-2)
|
||||
|
||||
-- Use the De Moivre closed form for fibonacci numbers.
|
||||
fib2 :: Int -> Int
|
||||
@ -17,8 +17,8 @@ fib2 x = truncate $ ( 1 / sqrt 5 ) * ( phi ^ x - psi ^ x )
|
||||
suite :: [Benchmark]
|
||||
suite = [
|
||||
bgroup "naive" [
|
||||
bench "fib 10" $ whnf fib 5
|
||||
, bench "fib 20" $ whnf fib 10
|
||||
bench "fib 10" $ whnf fib1 5
|
||||
, bench "fib 20" $ whnf fib1 10
|
||||
],
|
||||
bgroup "de moivre" [
|
||||
bench "fib 10" $ whnf fib2 5
|
||||
|
||||
@ -39,7 +39,6 @@ zipVec :: Vec n a -> Vec n b -> Vec n (a,b)
|
||||
zipVec Nil Nil = Nil
|
||||
zipVec (Cons x xs) (Cons y ys) = Cons (x,y) (zipVec xs ys)
|
||||
|
||||
|
||||
vec4 :: Vec Four Int
|
||||
vec4 = fromList [0, 1, 2, 3]
|
||||
|
||||
|
||||
94
src/debruijn.hs
Normal file
94
src/debruijn.hs
Normal file
@ -0,0 +1,94 @@
|
||||
import Control.Monad
|
||||
import Text.PrettyPrint
|
||||
import qualified Data.Map as Map
|
||||
|
||||
-- de Bruijn indices
|
||||
data DExp
|
||||
= Var Integer
|
||||
| Lam DExp
|
||||
| App DExp DExp
|
||||
deriving (Eq)
|
||||
|
||||
subst :: DExp -> Integer -> DExp -> DExp
|
||||
subst e n (Var n')
|
||||
| n == n' = e
|
||||
| otherwise = (Var n')
|
||||
subst e n (Lam e') = Lam $ subst e (n+1) e'
|
||||
subst e n (App e1 e2) = App (subst e n e1) (subst e n e2)
|
||||
|
||||
nf :: DExp -> DExp
|
||||
nf e@(Var _) = e
|
||||
nf (Lam e) = Lam (nf e)
|
||||
nf (App f a) =
|
||||
case whnf f of
|
||||
Lam b -> nf (subst a 0 b)
|
||||
f' -> App (nf f') (nf a)
|
||||
|
||||
whnf :: DExp -> DExp
|
||||
whnf e@(Var _) = e
|
||||
whnf e@(Lam _) = e
|
||||
whnf (App f a) =
|
||||
case whnf f of
|
||||
Lam b -> whnf (subst a 0 b)
|
||||
f' -> App f' a
|
||||
|
||||
|
||||
-- Pretty printer
|
||||
|
||||
parensIf :: Bool -> Doc -> Doc
|
||||
parensIf True = parens
|
||||
parensIf False = id
|
||||
|
||||
class Pretty p where
|
||||
ppr :: Int -> p -> Doc
|
||||
|
||||
instance Pretty DExp where
|
||||
ppr _ (Var v) = integer (v+1)
|
||||
ppr p (Lam f) = parensIf (p>0) $ text "λ " <> ppr p f
|
||||
ppr p (App f x) = ppr' f <+> ppr' x
|
||||
where
|
||||
ppr' (Var v) = integer (v+1)
|
||||
ppr' expr = parens $ ppr p expr
|
||||
|
||||
ppexpr :: DExp -> String
|
||||
ppexpr = render . ppr 0
|
||||
|
||||
-- Locally named
|
||||
data NExp
|
||||
= EVar String
|
||||
| ELam String NExp
|
||||
| EApp NExp NExp
|
||||
deriving (Show)
|
||||
|
||||
type Ctx = Map.Map String Integer
|
||||
|
||||
letters :: [String]
|
||||
letters = [1..] >>= flip replicateM ['a'..'z']
|
||||
|
||||
shift :: Ctx -> NExp -> DExp
|
||||
shift c (EVar v) = Var (c Map.! v)
|
||||
shift c (EApp a b) = App (shift c a) (shift c b)
|
||||
shift c (ELam v body) = Lam (shift c' body)
|
||||
where c' = Map.insert v 0 (Map.map (+1) c)
|
||||
|
||||
toDeBruijn :: NExp -> DExp
|
||||
toDeBruijn = shift Map.empty
|
||||
|
||||
fromDeBruijn :: DExp -> NExp
|
||||
fromDeBruijn = from 0
|
||||
where from n (Var i) = EVar (letters !! (n - (fromIntegral i) - 1))
|
||||
from n (Lam b) = ELam (letters !! n) (from (succ n) b)
|
||||
from n (App f a) = EApp (from n f) (from n a)
|
||||
|
||||
i = ELam "a" (EVar "a")
|
||||
k = ELam "a" (ELam "b" (EVar "a"))
|
||||
s = ELam "a" (ELam "b" (ELam "c" (EApp (EApp (EVar "a") (EVar "c")) (EApp (EVar "b") (EVar "c")))))
|
||||
|
||||
ex1 = ppexpr $ toDeBruijn i
|
||||
-- λ 1
|
||||
ex2 = ppexpr $ toDeBruijn k
|
||||
-- λ λ 2
|
||||
ex3 = ppexpr $ toDeBruijn s
|
||||
-- λ λ λ (3 1) (2 1)
|
||||
ex4 = fromDeBruijn $ toDeBruijn s
|
||||
-- ELam "a" (ELam "b" (ELam "c" (EApp (EApp (EVar "a") (EVar "c")) (EApp (EVar "b") (EVar "c")))))
|
||||
@ -8,9 +8,10 @@ data Failure
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
putStrLn "Enter a positive number."
|
||||
s <- getLine
|
||||
|
||||
e <- runEitherT $ do
|
||||
liftIO $ putStrLn "Enter a positive number."
|
||||
s <- liftIO getLine
|
||||
n <- tryRead (ReadError s) s
|
||||
if n > 0
|
||||
then return $ n + 1
|
||||
|
||||
35
src/enum_family_splice.hs
Normal file
35
src/enum_family_splice.hs
Normal file
@ -0,0 +1,35 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
|
||||
import EnumFamily
|
||||
|
||||
import Data.Proxy
|
||||
import GHC.TypeLits
|
||||
|
||||
type family Mod (m :: Nat) (n :: Nat) :: Nat
|
||||
type family Add (m :: Nat) (n :: Nat) :: Nat
|
||||
type family Pow (m :: Nat) (n :: Nat) :: Nat
|
||||
|
||||
enumFamily mod ''Mod 10
|
||||
enumFamily (+) ''Add 10
|
||||
enumFamily (^) ''Pow 10
|
||||
|
||||
a :: Integer
|
||||
a = natVal (Proxy :: Proxy (Mod 6 4))
|
||||
-- 2
|
||||
|
||||
b :: Integer
|
||||
b = natVal (Proxy :: Proxy (Pow 3 (Mod 6 4)))
|
||||
-- 9
|
||||
|
||||
-- enumFamily mod ''Mod 3
|
||||
-- ======>
|
||||
-- template_typelevel_splice.hs:7:1-14
|
||||
-- type instance Mod 2 1 = 0
|
||||
-- type instance Mod 2 2 = 0
|
||||
-- type instance Mod 2 3 = 2
|
||||
-- type instance Mod 3 1 = 0
|
||||
-- type instance Mod 3 2 = 1
|
||||
-- type instance Mod 3 3 = 0
|
||||
-- ...
|
||||
27
src/equal.hs
27
src/equal.hs
@ -1,16 +1,33 @@
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE ExplicitForAll #-}
|
||||
|
||||
-- a ≡ b
|
||||
data Eql a b where
|
||||
Refl :: Eql a a
|
||||
|
||||
sym :: Eql a b -> Eql b a
|
||||
sym Refl = Refl
|
||||
|
||||
-- Congruence
|
||||
-- (f : A → B) {x y} → x ≡ y → f x ≡ f y
|
||||
cong :: Eql a b -> Eql (f a) (f b)
|
||||
cong Refl = Refl
|
||||
|
||||
-- Symmetry
|
||||
-- {a b : A} → a ≡ b → a ≡ b
|
||||
sym :: Eql a b -> Eql b a
|
||||
sym Refl = Refl
|
||||
|
||||
-- Transitivity
|
||||
-- {a b c : A} → a ≡ b → b ≡ c → a ≡ c
|
||||
trans :: Eql a b -> Eql b c -> Eql a c
|
||||
trans Refl Refl = Refl
|
||||
|
||||
cast :: Eql a b -> a -> b
|
||||
cast Refl = id
|
||||
-- Coerce one type to another given a proof of their equality.
|
||||
-- {a b : A} → a ≡ b → a → b
|
||||
castWith :: Eql a b -> a -> b
|
||||
castWith Refl = id
|
||||
|
||||
-- Trival cases
|
||||
a :: forall n. Eql n n
|
||||
a = Refl
|
||||
|
||||
b :: forall. Eql () ()
|
||||
b = Refl
|
||||
|
||||
29
src/existential.hs
Normal file
29
src/existential.hs
Normal file
@ -0,0 +1,29 @@
|
||||
{-# LANGUAGE ExistentialQuantification #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
-- ∃ t. (t, t → t, t → String)
|
||||
data Box = forall a. Box a (a -> a) (a -> String)
|
||||
|
||||
boxa :: Box
|
||||
boxa = Box 1 negate show
|
||||
|
||||
boxb :: Box
|
||||
boxb = Box "foo" reverse show
|
||||
|
||||
apply :: Box -> String
|
||||
apply (Box x f p) = p (f x)
|
||||
|
||||
-- ∃ t. Show t => t
|
||||
data SBox = forall a. Show a => SBox a
|
||||
|
||||
boxes :: [SBox]
|
||||
boxes = [SBox (), SBox 2, SBox "foo"]
|
||||
|
||||
showBox :: SBox -> String
|
||||
showBox (SBox a) = show a
|
||||
|
||||
main :: IO ()
|
||||
main = mapM_ (putStrLn . showBox) boxes
|
||||
-- ()
|
||||
-- 2
|
||||
-- "foo"
|
||||
10
src/existential2.hs
Normal file
10
src/existential2.hs
Normal file
@ -0,0 +1,10 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
-- The functor is a fixed implementation of the library internals.
|
||||
type Exists a b = forall f. Functor f => (b -> f b) -> (a -> f a)
|
||||
|
||||
type Get a b = a -> b
|
||||
type Set a b = a -> b -> a
|
||||
|
||||
example :: Get a b -> Set a b -> Exists a b
|
||||
example f g l a = fmap (g a) (l (f a))
|
||||
@ -1,5 +1,3 @@
|
||||
{-# LANGUAGE NoMonomorphismRestriction #-}
|
||||
|
||||
import Prelude hiding (id)
|
||||
|
||||
class Expr rep where
|
||||
@ -17,7 +15,6 @@ instance Expr Interpret where
|
||||
eval :: Interpret a -> a
|
||||
eval e = reify e
|
||||
|
||||
|
||||
e1 :: Expr rep => rep Int
|
||||
e1 = app (lam (\x -> x)) (lit 3)
|
||||
|
||||
|
||||
1
src/foo.txt
Normal file
1
src/foo.txt
Normal file
@ -0,0 +1 @@
|
||||
foo
|
||||
44
src/free.hs
44
src/free.hs
@ -1,44 +0,0 @@
|
||||
{-# LANGUAGE NoMonomorphismRestriction #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
|
||||
import Control.Monad.Free
|
||||
import Control.Monad
|
||||
|
||||
import Data.Monoid
|
||||
|
||||
data Cons a b = Cons a b deriving (Eq, Show)
|
||||
|
||||
instance Functor (Cons a) where
|
||||
fmap f (Cons a b) = Cons a (f b)
|
||||
|
||||
type List a = Free (Cons a) ()
|
||||
|
||||
nil :: List a
|
||||
nil = Pure ()
|
||||
|
||||
cons :: a -> List a -> List a
|
||||
cons x xs = Free (Cons x xs)
|
||||
|
||||
append :: a -> List a
|
||||
append x = cons x nil
|
||||
|
||||
example1 :: List Int
|
||||
example1 = 1 `cons` (2 `cons` nil)
|
||||
|
||||
example2 :: List Int
|
||||
example2 = append 1 >> append 2 >> append 3
|
||||
|
||||
example3 :: Free [] Int
|
||||
example3 = liftF [1..5]
|
||||
|
||||
example4 :: [Int]
|
||||
example4 = retract example3
|
||||
|
||||
example5 :: Free Maybe Int
|
||||
example5 = liftF (Just 3)
|
||||
|
||||
example6 :: Maybe Int
|
||||
example6 = iterM join example5
|
||||
|
||||
example7 :: [Int]
|
||||
example7 = iterM join example3
|
||||
26
src/function.hs
Normal file
26
src/function.hs
Normal file
@ -0,0 +1,26 @@
|
||||
import Control.Monad
|
||||
|
||||
id' :: (->) a a
|
||||
id' = id
|
||||
|
||||
const' :: (->) a ((->) b a)
|
||||
const' = const
|
||||
|
||||
-- Monad m => a -> m a
|
||||
fret :: a -> b -> a
|
||||
fret = return
|
||||
|
||||
-- Monad m => m a -> (a -> m b) -> m b
|
||||
fbind :: (r -> a) -> (a -> (r -> b)) -> (r -> b)
|
||||
fbind f k = f >>= k
|
||||
|
||||
-- Monad m => m (m a) -> m a
|
||||
fjoin :: (r -> (r -> a)) -> (r -> a)
|
||||
fjoin = join
|
||||
|
||||
fid :: a -> a
|
||||
fid = const >>= id
|
||||
|
||||
-- Functor f => (a -> b) -> f a -> f b
|
||||
fcompose :: (a -> b) -> (r -> a) -> (r -> b)
|
||||
fcompose = (.)
|
||||
24
src/graph.hs
Normal file
24
src/graph.hs
Normal file
@ -0,0 +1,24 @@
|
||||
import Data.Tree
|
||||
import Data.Graph
|
||||
|
||||
data Grph node key = Grph
|
||||
{ _graph :: Graph
|
||||
, _vertices :: Vertex -> (node, key, [key])
|
||||
}
|
||||
|
||||
fromList :: Ord key => [(node, key, [key])] -> Grph node key
|
||||
fromList = uncurry Grph . graphFromEdges'
|
||||
|
||||
vertexLabels :: Functor f => Grph b t -> (f Vertex) -> f b
|
||||
vertexLabels g = fmap (vertexLabel g)
|
||||
|
||||
vertexLabel :: Grph b t -> Vertex -> b
|
||||
vertexLabel g = (\(vi, _, _) -> vi) . (_vertices g)
|
||||
|
||||
-- Topologically sort graph
|
||||
topo' :: Grph node key -> [node]
|
||||
topo' g = vertexLabels g $ topSort (_graph g)
|
||||
|
||||
-- Strongly connected components of graph
|
||||
scc' :: Grph node key -> [[node]]
|
||||
scc' g = fmap (vertexLabels g . flatten) $ scc (_graph g)
|
||||
72
src/hasfield.hs
Normal file
72
src/hasfield.hs
Normal file
@ -0,0 +1,72 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE FunctionalDependencies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
|
||||
|
||||
import GHC.TypeLits
|
||||
import Data.Type.Equality
|
||||
|
||||
data Label (l :: Symbol) = Get
|
||||
|
||||
class Has a l b | a l -> b where
|
||||
from :: a -> Label l -> b
|
||||
|
||||
data Point2D = Point2 Double Double deriving Show
|
||||
data Point3D = Point3 Double Double Double deriving Show
|
||||
|
||||
instance Has Point2D "x" Double where
|
||||
from (Point2 x _) _ = x
|
||||
|
||||
instance Has Point2D "y" Double where
|
||||
from (Point2 _ y) _ = y
|
||||
|
||||
|
||||
instance Has Point3D "x" Double where
|
||||
from (Point3 x _ _) _ = x
|
||||
|
||||
instance Has Point3D "y" Double where
|
||||
from (Point3 _ y _) _ = y
|
||||
|
||||
instance Has Point3D "z" Double where
|
||||
from (Point3 _ _ z) _ = z
|
||||
|
||||
|
||||
infixl 6 #
|
||||
|
||||
(#) :: a -> (a -> b) -> b
|
||||
(#) = flip ($)
|
||||
|
||||
_x :: Has a "x" b => a -> b
|
||||
_x pnt = from pnt (Get :: Label "x")
|
||||
|
||||
_y :: Has a "y" b => a -> b
|
||||
_y pnt = from pnt (Get :: Label "y")
|
||||
|
||||
_z :: Has a "z" b => a -> b
|
||||
_z pnt = from pnt (Get :: Label "z")
|
||||
|
||||
type Point a r = (Has a "x" r, Has a "y" r)
|
||||
|
||||
distance :: (Point a r, Point b r, Floating r) => a -> b -> r
|
||||
distance p1 p2 = sqrt (d1^2 + d2^2)
|
||||
where
|
||||
d1 = (p1 # _x) + (p1 # _y)
|
||||
d2 = (p2 # _x) + (p2 # _y)
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
print $ (Point2 10 20) # _x
|
||||
|
||||
-- Fails with: No instance for (Has Point2D "z" a0)
|
||||
-- print $ (Point2 10 20) # _z
|
||||
|
||||
print $ (Point3 10 20 30) # _x
|
||||
print $ (Point3 10 20 30) # _z
|
||||
|
||||
print $ distance (Point2 1 3) (Point2 2 7)
|
||||
print $ distance (Point2 1 3) (Point3 2 7 4)
|
||||
print $ distance (Point3 1 3 5) (Point3 2 7 3)
|
||||
@ -6,16 +6,16 @@ import Data.HashTable.ST.Basic
|
||||
-- Hashtable parameterized by ST "thread"
|
||||
type HT s = HashTable s String String
|
||||
|
||||
example1 :: ST s (HT s)
|
||||
example1 = do
|
||||
set :: ST s (HT s)
|
||||
set = do
|
||||
ht <- new
|
||||
insert ht "key" "value1"
|
||||
return ht
|
||||
|
||||
example2 :: HT s -> ST s (Maybe String)
|
||||
example2 ht = do
|
||||
get :: HT s -> ST s (Maybe String)
|
||||
get ht = do
|
||||
val <- lookup ht "key"
|
||||
return val
|
||||
|
||||
example3 :: Maybe String
|
||||
example3 = runST (example1 >>= example2)
|
||||
example :: Maybe String
|
||||
example = runST (set >>= get)
|
||||
|
||||
18
src/hblas.hs
Normal file
18
src/hblas.hs
Normal file
@ -0,0 +1,18 @@
|
||||
import Foreign.Storable
|
||||
import Numerical.HBLAS.BLAS
|
||||
import Numerical.HBLAS.MatrixTypes
|
||||
|
||||
-- Generate the constant mutable square matrix of the given type and dimensions.
|
||||
constMatrix :: Storable a => Int -> a -> IO (IODenseMatrix Row a)
|
||||
constMatrix n k = generateMutableDenseMatrix SRow (n,n) (const k)
|
||||
|
||||
example_dgemm :: IO ()
|
||||
example_dgemm = do
|
||||
left <- constMatrix 2 (2 :: Double)
|
||||
right <- constMatrix 2 (3 :: Double)
|
||||
out <- constMatrix 2 (0 :: Double)
|
||||
|
||||
dgemm NoTranspose NoTranspose 1.0 1.0 left right out
|
||||
|
||||
resulting <- mutableVectorToList $ _bufferDenMutMat out
|
||||
print resulting
|
||||
@ -19,8 +19,8 @@ hlength Nil = 0
|
||||
hlength (_ ::: b) = 1 + (hlength b)
|
||||
|
||||
|
||||
example1 :: (Bool, (String, (Double, ())))
|
||||
example1 = (True, ("foo", (3.14, ())))
|
||||
tuple :: (Bool, (String, (Double, ())))
|
||||
tuple = (True, ("foo", (3.14, ())))
|
||||
|
||||
example2 :: HList '[Bool, String , Double , ()]
|
||||
example2 = True ::: "foo" ::: 3.14 ::: () ::: Nil
|
||||
hlist :: HList '[Bool, String , Double , ()]
|
||||
hlist = True ::: "foo" ::: 3.14 ::: () ::: Nil
|
||||
|
||||
@ -21,7 +21,7 @@ eval (App e1 e2) = (eval e1) (eval e2)
|
||||
|
||||
|
||||
skk :: Expr (a -> a)
|
||||
skk = (App (App s k) k)
|
||||
skk = App (App s k) k
|
||||
|
||||
example :: Integer
|
||||
example = eval skk 1
|
||||
|
||||
30
src/http.hs
Normal file
30
src/http.hs
Normal file
@ -0,0 +1,30 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
import Network.HTTP.Types
|
||||
import Network.HTTP.Client
|
||||
import Control.Applicative
|
||||
import Control.Concurrent.Async
|
||||
|
||||
type URL = String
|
||||
|
||||
get :: Manager -> URL -> IO Int
|
||||
get m url = do
|
||||
req <- parseUrl url
|
||||
statusCode <$> responseStatus <$> httpNoBody req m
|
||||
|
||||
single :: IO Int
|
||||
single = do
|
||||
withManager defaultManagerSettings $ \m -> do
|
||||
get m "http://haskell.org"
|
||||
|
||||
parallel :: IO [Int]
|
||||
parallel = do
|
||||
withManager defaultManagerSettings $ \m -> do
|
||||
-- Fetch w3.org 10 times concurrently
|
||||
let urls = replicate 10 "http://www.w3.org"
|
||||
mapConcurrently (get m) urls
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
print =<< single
|
||||
print =<< parallel
|
||||
8
src/impredicative.hs
Normal file
8
src/impredicative.hs
Normal file
@ -0,0 +1,8 @@
|
||||
{-# LANGUAGE ImpredicativeTypes #-}
|
||||
|
||||
f :: (forall a. [a] -> a) -> (Int, Char)
|
||||
f get = (get [1,2], get ['a', 'b', 'c'])
|
||||
|
||||
g :: Maybe (forall a. [a] -> a) -> (Int, Char)
|
||||
g Nothing = (0, '0')
|
||||
g (Just get) = (get [1,2], get ['a','b','c'])
|
||||
96
src/indexed.hs
Normal file
96
src/indexed.hs
Normal file
@ -0,0 +1,96 @@
|
||||
{-# LANGUAGE RebindableSyntax #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE NoMonomorphismRestriction #-}
|
||||
|
||||
import Data.IORef
|
||||
import Data.Char
|
||||
import Prelude hiding (fmap, (>>=), (>>), return)
|
||||
import Control.Applicative
|
||||
|
||||
newtype IState i o a = IState { runIState :: i -> (a, o) }
|
||||
|
||||
evalIState :: IState i o a -> i -> a
|
||||
evalIState st i = fst $ runIState st i
|
||||
|
||||
execIState :: IState i o a -> i -> o
|
||||
execIState st i = snd $ runIState st i
|
||||
|
||||
ifThenElse :: Bool -> a -> a -> a
|
||||
ifThenElse b i j = case b of
|
||||
True -> i
|
||||
False -> j
|
||||
|
||||
return :: a -> IState s s a
|
||||
return a = IState $ \s -> (a, s)
|
||||
|
||||
fmap :: (a -> b) -> IState i o a -> IState i o b
|
||||
fmap f v = IState $ \i -> let (a, o) = runIState v i
|
||||
in (f a, o)
|
||||
|
||||
join :: IState i m (IState m o a) -> IState i o a
|
||||
join v = IState $ \i -> let (w, m) = runIState v i
|
||||
in runIState w m
|
||||
|
||||
(>>=) :: IState i m a -> (a -> IState m o b) -> IState i o b
|
||||
v >>= f = IState $ \i -> let (a, m) = runIState v i
|
||||
in runIState (f a) m
|
||||
|
||||
(>>) :: IState i m a -> IState m o b -> IState i o b
|
||||
v >> w = v >>= \_ -> w
|
||||
|
||||
get :: IState s s s
|
||||
get = IState $ \s -> (s, s)
|
||||
|
||||
gets :: (a -> o) -> IState a o a
|
||||
gets f = IState $ \s -> (s, f s)
|
||||
|
||||
put :: o -> IState i o ()
|
||||
put o = IState $ \_ -> ((), o)
|
||||
|
||||
modify :: (i -> o) -> IState i o ()
|
||||
modify f = IState $ \i -> ((), f i)
|
||||
|
||||
|
||||
|
||||
data Locked = Locked
|
||||
data Unlocked = Unlocked
|
||||
|
||||
type Stateful a = IState a Unlocked a
|
||||
|
||||
acquire :: IState i Locked ()
|
||||
acquire = put Locked
|
||||
|
||||
-- Can only release the lock if it's held, try release the lock
|
||||
-- that's not held is a now a type error.
|
||||
release :: IState Locked Unlocked ()
|
||||
release = put Unlocked
|
||||
|
||||
-- Statically forbids improper handling of resources.
|
||||
lockExample :: Stateful a
|
||||
lockExample = do ptr <- get :: IState a a a
|
||||
acquire :: IState a Locked ()
|
||||
-- ...
|
||||
release :: IState Locked Unlocked ()
|
||||
return ptr
|
||||
|
||||
-- Couldn't match type `Locked' with `Unlocked'
|
||||
-- In a stmt of a 'do' block: return ptr
|
||||
failure1 :: Stateful a
|
||||
failure1 = do ptr <- get
|
||||
acquire
|
||||
return ptr -- didn't release
|
||||
|
||||
-- Couldn't match type `a' with `Locked'
|
||||
-- In a stmt of a 'do' block: release
|
||||
failure2 :: Stateful a
|
||||
failure2 = do ptr <- get
|
||||
release -- didn't acquire
|
||||
return ptr
|
||||
|
||||
-- Evaluate the resulting state, statically ensuring that the
|
||||
-- lock is released when finished.
|
||||
evalReleased :: IState i Unlocked a -> i -> a
|
||||
evalReleased f st = evalIState f st
|
||||
|
||||
example :: IO (IORef Integer)
|
||||
example = evalReleased <$> pure lockExample <*> newIORef 0
|
||||
@ -9,12 +9,15 @@ type Coalgebra f a = a -> f a
|
||||
|
||||
newtype Fix f = Fix { unFix :: f (Fix f) }
|
||||
|
||||
-- catamorphism
|
||||
cata :: Functor f => Algebra f a -> Fix f -> a
|
||||
cata alg = alg . fmap (cata alg) . unFix
|
||||
|
||||
-- anamorphism
|
||||
ana :: Functor f => Coalgebra f a -> a -> Fix f
|
||||
ana coalg = Fix . fmap (ana coalg) . coalg
|
||||
|
||||
-- hylomorphism
|
||||
hylo :: Functor f => Algebra f b -> Coalgebra f a -> a -> b
|
||||
hylo f g = cata f . ana g
|
||||
|
||||
|
||||
19
src/iso.hs
Normal file
19
src/iso.hs
Normal file
@ -0,0 +1,19 @@
|
||||
{-# LANGUAGE ExplicitForAll #-}
|
||||
|
||||
data Iso a b = Iso { to :: a -> b, from :: b -> a }
|
||||
|
||||
f :: forall a. Maybe a -> Either () a
|
||||
f (Just a) = Right a
|
||||
f Nothing = Left ()
|
||||
|
||||
f' :: forall a. Either () a -> Maybe a
|
||||
f' (Left _) = Nothing
|
||||
f' (Right a) = Just a
|
||||
|
||||
iso :: Iso (Maybe a) (Either () a)
|
||||
iso = Iso f f'
|
||||
|
||||
data V = V deriving Eq
|
||||
|
||||
ex1 = f (f' (Right V)) == Right V
|
||||
ex2 = f' (f (Just V)) == Just V
|
||||
12
src/lazyio.hs
Normal file
12
src/lazyio.hs
Normal file
@ -0,0 +1,12 @@
|
||||
import System.IO
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
withFile "foo.txt" ReadMode $ \fd -> do
|
||||
contents <- hGetContents fd
|
||||
print contents
|
||||
-- "foo\n"
|
||||
|
||||
contents <- withFile "foo.txt" ReadMode hGetContents
|
||||
print contents
|
||||
-- ""
|
||||
30
src/lens.hs
30
src/lens.hs
@ -1,12 +1,14 @@
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE NoMonomorphismRestriction #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
|
||||
import Control.Lens
|
||||
import Control.Lens.TH
|
||||
|
||||
data Record1 a = Record1
|
||||
data Record1 = Record1
|
||||
{ _a :: Int
|
||||
, _b :: Maybe a
|
||||
, _b :: Maybe Record2
|
||||
} deriving Show
|
||||
|
||||
data Record2 = Record2
|
||||
@ -14,9 +16,10 @@ data Record2 = Record2
|
||||
, _d :: [Int]
|
||||
} deriving Show
|
||||
|
||||
$(makeLenses ''Record1)
|
||||
$(makeLenses ''Record2)
|
||||
makeLenses ''Record1
|
||||
makeLenses ''Record2
|
||||
|
||||
records :: [Record1]
|
||||
records = [
|
||||
Record1 {
|
||||
_a = 1,
|
||||
@ -45,28 +48,31 @@ records = [
|
||||
}
|
||||
]
|
||||
|
||||
-- Some abstract traversals.
|
||||
ids = traverse.a
|
||||
names = traverse.b._Just.c
|
||||
nums = traverse.b._Just.d
|
||||
list2 = traverse.b._Just.d.ix 2
|
||||
|
||||
-- Modify/read/extract in terms of generic traversals.
|
||||
-- Lens targets
|
||||
ids = traverse.a
|
||||
names = traverse.b._Just.c
|
||||
nums = traverse.b._Just.d
|
||||
listn n = traverse.b._Just.d.ix n
|
||||
|
||||
-- Modify to set all 'id' fields to 0
|
||||
ex1 :: [Record1]
|
||||
ex1 = set ids 0 records
|
||||
|
||||
-- Return a view of the concatenated 'd' fields for all nested records.
|
||||
ex2 :: [Int]
|
||||
ex2 = view nums records
|
||||
-- [1,2,3,4,5,6,7,8,9]
|
||||
|
||||
-- Increment all 'id' fields by 1
|
||||
ex3 :: [Record1]
|
||||
ex3 = over ids (+1) records
|
||||
|
||||
-- Return a list of all 'c' fields.
|
||||
ex4 :: [String]
|
||||
ex4 = toListOf names records
|
||||
-- ["Picard","Riker","Data"]
|
||||
|
||||
-- Return the the second element of all 'd' fields.
|
||||
ex5 = toListOf list2 records
|
||||
ex5 :: [Int]
|
||||
ex5 = toListOf (listn 2) records
|
||||
-- [3,6,9]
|
||||
|
||||
@ -6,9 +6,9 @@ import Lens.Family.TH
|
||||
import Lens.Family.Stock
|
||||
import Data.Traversable
|
||||
|
||||
data Record1 a = Record1
|
||||
data Record1 = Record1
|
||||
{ _a :: Int
|
||||
, _b :: Maybe a
|
||||
, _b :: Maybe Record2
|
||||
} deriving Show
|
||||
|
||||
data Record2 = Record2
|
||||
@ -16,9 +16,10 @@ data Record2 = Record2
|
||||
, _d :: [Int]
|
||||
} deriving Show
|
||||
|
||||
$(mkLenses ''Record1)
|
||||
$(mkLenses ''Record2)
|
||||
mkLenses ''Record1
|
||||
mkLenses ''Record2
|
||||
|
||||
records :: [Record1]
|
||||
records = [
|
||||
Record1 {
|
||||
_a = 1,
|
||||
|
||||
85
src/lens_impl.hs
Normal file
85
src/lens_impl.hs
Normal file
@ -0,0 +1,85 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE NoMonomorphismRestriction #-}
|
||||
|
||||
import Data.Functor
|
||||
|
||||
type Lens' a b = forall f. Functor f => (b -> f b) -> (a -> f a)
|
||||
|
||||
newtype Const x a = Const { runConst :: x } deriving Functor
|
||||
newtype Identity a = Identity { runIdentity :: a } deriving Functor
|
||||
|
||||
lens :: (s -> a) -> (s -> a -> s) -> Lens' s a
|
||||
lens getter setter f a = fmap (setter a) (f (getter a))
|
||||
|
||||
set :: Lens' a b -> b -> a -> a
|
||||
set l b = runIdentity . l (const (Identity b))
|
||||
|
||||
view :: Lens' a b -> a -> b
|
||||
view l = runConst . l Const
|
||||
|
||||
over :: Lens' a b -> (b -> b) -> a -> a
|
||||
over l f a = set l (f (view l a)) a
|
||||
|
||||
compose :: Lens' a b -> Lens' b c -> Lens' a c
|
||||
compose l s = l . s
|
||||
|
||||
id' :: Lens' a a
|
||||
id' = id
|
||||
|
||||
infixl 1 &
|
||||
infixr 4 .~
|
||||
infixr 4 %~
|
||||
infixr 8 ^.
|
||||
|
||||
(^.) = flip view
|
||||
(.~) = set
|
||||
(%~) = over
|
||||
|
||||
(&) :: a -> (a -> b) -> b
|
||||
(&) = flip ($)
|
||||
|
||||
(+~), (-~), (*~) :: Num b => Lens' a b -> b -> a -> a
|
||||
f +~ b = f %~ (+b)
|
||||
f -~ b = f %~ (subtract b)
|
||||
f *~ b = f %~ (*b)
|
||||
|
||||
-- Usage
|
||||
|
||||
data Foo = Foo { _a :: Int } deriving Show
|
||||
data Bar = Bar { _b :: Foo } deriving Show
|
||||
|
||||
a :: Lens' Foo Int
|
||||
a = lens getter setter
|
||||
where
|
||||
getter :: Foo -> Int
|
||||
getter = _a
|
||||
|
||||
setter :: Foo -> Int -> Foo
|
||||
setter = (\f new -> f { _a = new })
|
||||
|
||||
|
||||
b :: Lens' Bar Foo
|
||||
b = lens getter setter
|
||||
where
|
||||
getter :: Bar -> Foo
|
||||
getter = _b
|
||||
|
||||
setter :: Bar -> Foo -> Bar
|
||||
setter = (\f new -> f { _b = new })
|
||||
|
||||
foo :: Foo
|
||||
foo = Foo 3
|
||||
|
||||
bar :: Bar
|
||||
bar = Bar foo
|
||||
|
||||
example1 = view a foo
|
||||
example2 = set a 1 foo
|
||||
example3 = over a (+1) foo
|
||||
example4 = view (b `compose` a) bar
|
||||
|
||||
example1' = foo ^. a
|
||||
example2' = foo & a .~ 1
|
||||
example3' = foo & a %~ (+1)
|
||||
example4' = bar ^. b . a
|
||||
86
src/lenspoly_impl.hs
Normal file
86
src/lenspoly_impl.hs
Normal file
@ -0,0 +1,86 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE NoMonomorphismRestriction #-}
|
||||
|
||||
import Data.Functor
|
||||
|
||||
type Lens a a' b b' = forall f. Functor f => (b -> f b') -> (a -> f a')
|
||||
type Lens' a b = Lens a a b b
|
||||
|
||||
newtype Const x a = Const { runConst :: x } deriving Functor
|
||||
newtype Identity a = Identity { runIdentity :: a } deriving Functor
|
||||
|
||||
lens :: (a -> b) -> (a -> b' -> a') -> Lens a a' b b'
|
||||
lens getter setter f a = fmap (setter a) (f (getter a))
|
||||
|
||||
set :: Lens a a' b b' -> b' -> a -> a'
|
||||
set l b = runIdentity . l (const (Identity b))
|
||||
|
||||
get :: Lens a a' b b' -> a -> b
|
||||
get l = runConst . l Const
|
||||
|
||||
over :: Lens a a' b b' -> (b -> b') -> a -> a'
|
||||
over l f a = set l (f (get l a)) a
|
||||
|
||||
compose :: Lens a a' b b' -> Lens b b' c c' -> Lens a a' c c'
|
||||
compose l s = l . s
|
||||
|
||||
id' :: Lens a a a a
|
||||
id' = id
|
||||
|
||||
infixl 1 &
|
||||
infixr 4 .~
|
||||
infixr 4 %~
|
||||
infixr 8 ^.
|
||||
|
||||
(^.) = flip get
|
||||
(.~) = set
|
||||
(%~) = over
|
||||
|
||||
(&) :: a -> (a -> b) -> b
|
||||
(&) = flip ($)
|
||||
|
||||
(+~), (-~), (*~) :: Num b => Lens a a b b -> b -> a -> a
|
||||
f +~ b = f %~ (+b)
|
||||
f -~ b = f %~ (subtract b)
|
||||
f *~ b = f %~ (*b)
|
||||
|
||||
-- Monomorphic Update
|
||||
data Foo = Foo { _a :: Int } deriving Show
|
||||
data Bar = Bar { _b :: Foo } deriving Show
|
||||
|
||||
a :: Lens' Foo Int
|
||||
a = lens getter setter
|
||||
where
|
||||
getter :: Foo -> Int
|
||||
getter = _a
|
||||
|
||||
setter :: Foo -> Int -> Foo
|
||||
setter = (\f new -> f { _a = new })
|
||||
|
||||
b :: Lens' Bar Foo
|
||||
b = lens getter setter
|
||||
where
|
||||
getter :: Bar -> Foo
|
||||
getter = _b
|
||||
|
||||
setter :: Bar -> Foo -> Bar
|
||||
setter = (\f new -> f { _b = new })
|
||||
|
||||
-- Polymorphic Update
|
||||
data Pair a b = Pair a b deriving Show
|
||||
|
||||
pair :: Pair Int Char
|
||||
pair = Pair 1 'b'
|
||||
|
||||
_1 :: Lens (Pair a b) (Pair a' b) a a'
|
||||
_1 f (Pair a b) = (\x -> Pair x b) <$> f a
|
||||
|
||||
_2 :: Lens (Pair a b) (Pair a b') b b'
|
||||
_2 f (Pair a b) = (\x -> Pair a x) <$> f b
|
||||
|
||||
ex1 = pair ^. _1
|
||||
ex2 = pair ^. _2
|
||||
ex3 = pair & _1 .~ "a"
|
||||
ex4 = pair & (_1 %~ (+1))
|
||||
. (_2 .~ 1)
|
||||
43
src/lexer.hs
Normal file
43
src/lexer.hs
Normal file
@ -0,0 +1,43 @@
|
||||
import Text.Parsec
|
||||
import Text.Parsec.Expr
|
||||
import Text.Parsec.String
|
||||
import qualified Text.Parsec.Token as Token
|
||||
|
||||
lexerStyle :: Token.LanguageDef ()
|
||||
lexerStyle = Token.LanguageDef
|
||||
{ Token.commentStart = "{-"
|
||||
, Token.commentEnd = "-}"
|
||||
, Token.commentLine = "--"
|
||||
, Token.nestedComments = True
|
||||
, Token.identStart = letter
|
||||
, Token.identLetter = alphaNum <|> oneOf "_"
|
||||
, Token.opStart = Token.opLetter lexerStyle
|
||||
, Token.opLetter = oneOf "`~!@$%^&*-+=;:<>./?"
|
||||
, Token.reservedOpNames= []
|
||||
, Token.reservedNames = ["if", "then", "else", "def"]
|
||||
, Token.caseSensitive = True
|
||||
}
|
||||
|
||||
lexer :: Token.TokenParser ()
|
||||
lexer = Token.makeTokenParser lexerStyle
|
||||
|
||||
parens :: Parser a -> Parser a
|
||||
parens = Token.parens lexer
|
||||
|
||||
natural :: Parser Integer
|
||||
natural = Token.natural lexer
|
||||
|
||||
identifier :: Parser String
|
||||
identifier = Token.identifier lexer
|
||||
|
||||
reservedOp :: String -> Parser ()
|
||||
reservedOp = Token.reservedOp lexer
|
||||
|
||||
reserved :: String -> Parser ()
|
||||
reserved = Token.reserved lexer
|
||||
|
||||
whiteSpace :: Parser ()
|
||||
whiteSpace = Token.whiteSpace lexer
|
||||
|
||||
comma :: Parser String
|
||||
comma = Token.comma lexer
|
||||
26
src/logict.hs
Normal file
26
src/logict.hs
Normal file
@ -0,0 +1,26 @@
|
||||
import Control.Monad
|
||||
|
||||
range :: MonadPlus m => [a] -> m a
|
||||
range [] = mzero
|
||||
range (x:xs) = range xs `mplus` return x
|
||||
|
||||
pyth :: Integer -> [(Integer,Integer,Integer)]
|
||||
pyth n = do
|
||||
x <- range [1..n]
|
||||
y <- range [1..n]
|
||||
z <- range [1..n]
|
||||
if x*x + y*y == z*z then return (x,y,z) else mzero
|
||||
|
||||
main :: IO ()
|
||||
main = print $ pyth 15
|
||||
{-
|
||||
[ ( 12 , 9 , 15 )
|
||||
, ( 12 , 5 , 13 )
|
||||
, ( 9 , 12 , 15 )
|
||||
, ( 8 , 6 , 10 )
|
||||
, ( 6 , 8 , 10 )
|
||||
, ( 5 , 12 , 13 )
|
||||
, ( 4 , 3 , 5 )
|
||||
, ( 3 , 4 , 5 )
|
||||
]
|
||||
-}
|
||||
10
src/map.hs
Normal file
10
src/map.hs
Normal file
@ -0,0 +1,10 @@
|
||||
import qualified Data.Map as Map
|
||||
|
||||
kv :: Map.Map Integer String
|
||||
kv = Map.fromList [(1, "a"), (2, "b")]
|
||||
|
||||
lkup :: Integer -> String -> String
|
||||
lkup key def =
|
||||
case Map.lookup key kv of
|
||||
Just val -> val
|
||||
Nothing -> def
|
||||
52
src/matrix_index.hs
Normal file
52
src/matrix_index.hs
Normal file
@ -0,0 +1,52 @@
|
||||
import qualified Data.Vector as V
|
||||
|
||||
data Order = RowMajor | ColMajor
|
||||
|
||||
rowMajor :: [Int] -> [Int]
|
||||
rowMajor = scanr (*) 1 . tail
|
||||
|
||||
colMajor :: [Int] -> [Int]
|
||||
colMajor = init . scanl (*) 1
|
||||
|
||||
data Matrix a = Matrix
|
||||
{ _dims :: [Int]
|
||||
, _elts :: V.Vector a
|
||||
, _order :: Order
|
||||
}
|
||||
|
||||
fromList :: [Int] -> Order -> [a] -> Matrix a
|
||||
fromList sh order elts =
|
||||
if product sh == length elts
|
||||
then Matrix sh (V.fromList elts) order
|
||||
else error "dimensions don't match"
|
||||
|
||||
indexTo :: [Int] -> Matrix a -> a
|
||||
indexTo ix mat = boundsCheck offset
|
||||
where
|
||||
boundsCheck n =
|
||||
if 0 <= n && n < V.length (_elts mat)
|
||||
then V.unsafeIndex (_elts mat) offset
|
||||
else error "out of bounds"
|
||||
ordering = case _order mat of
|
||||
RowMajor -> rowMajor
|
||||
ColMajor -> colMajor
|
||||
offset = sum $ zipWith (*) ix (ordering (_dims mat))
|
||||
|
||||
matrix :: Order -> Matrix Int
|
||||
matrix order = fromList [4,4] order [1..16]
|
||||
|
||||
ex1 :: [Int]
|
||||
ex1 = rowMajor [1,2,3,4]
|
||||
-- [24,12,4,1]
|
||||
|
||||
ex2 :: [Int]
|
||||
ex2 = colMajor [1,2,3,4]
|
||||
-- [1,1,2,6]
|
||||
|
||||
ex3 :: Int
|
||||
ex3 = indexTo [1,3] (matrix RowMajor)
|
||||
-- 8
|
||||
|
||||
ex4 :: Int
|
||||
ex4 = indexTo [1,3] (matrix ColMajor)
|
||||
-- 14
|
||||
14
src/monadfix.hs
Normal file
14
src/monadfix.hs
Normal file
@ -0,0 +1,14 @@
|
||||
{-# LANGUAGE RecursiveDo #-}
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Monad.Fix
|
||||
|
||||
stream1 :: Maybe [Int]
|
||||
stream1 = do
|
||||
rec xs <- Just (1:xs)
|
||||
return (map negate xs)
|
||||
|
||||
stream2 :: Maybe [Int]
|
||||
stream2 = mfix $ \xs -> do
|
||||
xs' <- Just (1:xs)
|
||||
return (map negate xs')
|
||||
22
src/monadplus.hs
Normal file
22
src/monadplus.hs
Normal file
@ -0,0 +1,22 @@
|
||||
import Safe
|
||||
import Control.Monad
|
||||
|
||||
list1 :: [(Int,Int)]
|
||||
list1 = [(a,b) | a <- [1..25], b <- [1..25], a < b]
|
||||
|
||||
list2 :: [(Int,Int)]
|
||||
list2 = do
|
||||
a <- [1..25]
|
||||
b <- [1..25]
|
||||
guard (a < b)
|
||||
return $ (a,b)
|
||||
|
||||
maybe1 :: String -> String -> Maybe Double
|
||||
maybe1 a b = do
|
||||
a' <- readMay a
|
||||
b' <- readMay b
|
||||
guard (b' /= 0.0)
|
||||
return $ a'/b'
|
||||
|
||||
maybe2 :: Maybe Int
|
||||
maybe2 = msum [Nothing, Nothing, Just 3, Just 4]
|
||||
65
src/mono.hs
Normal file
65
src/mono.hs
Normal file
@ -0,0 +1,65 @@
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
import Data.Text
|
||||
import Data.Char
|
||||
import Data.Monoid
|
||||
import Data.MonoTraversable
|
||||
import Control.Applicative
|
||||
|
||||
bs :: Text
|
||||
bs = "Hello Haskell."
|
||||
|
||||
shift :: Text
|
||||
shift = omap (chr . (+1) . ord) bs
|
||||
-- "Ifmmp!Ibtlfmm/"
|
||||
|
||||
backwards :: [Char]
|
||||
backwards = ofoldl' (flip (:)) "" bs
|
||||
-- ".lleksaH olleH"
|
||||
|
||||
|
||||
data MyMonoType = MNil | MCons Int MyMonoType deriving Show
|
||||
|
||||
type instance Element MyMonoType = Int
|
||||
|
||||
instance MonoFunctor MyMonoType where
|
||||
omap f MNil = MNil
|
||||
omap f (MCons x xs) = f x `MCons` omap f xs
|
||||
|
||||
instance MonoFoldable MyMonoType where
|
||||
ofoldMap f = ofoldr (mappend . f) mempty
|
||||
ofoldr = mfoldr
|
||||
ofoldl' = mfoldl'
|
||||
ofoldr1Ex f = ofoldr1Ex f . mtoList
|
||||
ofoldl1Ex' f = ofoldl1Ex' f . mtoList
|
||||
|
||||
instance MonoTraversable MyMonoType where
|
||||
omapM f xs = mapM f (mtoList xs) >>= return . mfromList
|
||||
otraverse f = ofoldr acons (pure MNil)
|
||||
where acons x ys = MCons <$> f x <*> ys
|
||||
|
||||
mtoList :: MyMonoType -> [Int]
|
||||
mtoList (MNil) = []
|
||||
mtoList (MCons x xs) = x : (mtoList xs)
|
||||
|
||||
mfromList :: [Int] -> MyMonoType
|
||||
mfromList [] = MNil
|
||||
mfromList (x:xs) = MCons x (mfromList xs)
|
||||
|
||||
mfoldr :: (Int -> a -> a) -> a -> MyMonoType -> a
|
||||
mfoldr f z MNil = z
|
||||
mfoldr f z (MCons x xs) = f x (mfoldr f z xs)
|
||||
|
||||
mfoldl' :: (a -> Int -> a) -> a -> MyMonoType -> a
|
||||
mfoldl' f z MNil = z
|
||||
mfoldl' f z (MCons x xs) = let z' = z `f` x
|
||||
in seq z' $ mfoldl' f z' xs
|
||||
|
||||
ex1 :: Int
|
||||
ex1 = mfoldl' (+) 0 (mfromList [1..25])
|
||||
|
||||
ex2 :: MyMonoType
|
||||
ex2 = omap (+1) (mfromList [1..25])
|
||||
|
||||
main = return ()
|
||||
9
src/monomorphism.hs
Normal file
9
src/monomorphism.hs
Normal file
@ -0,0 +1,9 @@
|
||||
-- Float is inferred by type inferencer.
|
||||
example1 :: Double
|
||||
example1 = 3.14
|
||||
|
||||
-- In the presense of a lambda, a different type is inferred!
|
||||
example2 :: Fractional a => t -> a
|
||||
example2 _ = 3.14
|
||||
|
||||
default (Integer, Double)
|
||||
@ -9,4 +9,17 @@ v = Velocity 2.718
|
||||
x :: Double
|
||||
x = 6.636
|
||||
|
||||
-- Type error is caught at compile time even though they are the same value at runtime!
|
||||
err = v + x
|
||||
|
||||
newtype Quantity v a = Quantity a
|
||||
deriving (Eq, Ord, Num, Show)
|
||||
|
||||
data Haskeller
|
||||
type Haskellers = Quantity Haskeller Int
|
||||
|
||||
a = Quantity 2 :: Haskellers
|
||||
b = Quantity 6 :: Haskellers
|
||||
|
||||
totalHaskellers :: Haskellers
|
||||
totalHaskellers = a + b
|
||||
|
||||
19
src/noempty.hs
Normal file
19
src/noempty.hs
Normal file
@ -0,0 +1,19 @@
|
||||
import Data.List.NonEmpty
|
||||
import Prelude hiding (head, tail, foldl1)
|
||||
import Data.Foldable (foldl1)
|
||||
|
||||
a :: NonEmpty Integer
|
||||
a = fromList [1,2,3]
|
||||
-- 1 :| [2,3]
|
||||
|
||||
b :: NonEmpty Integer
|
||||
b = 1 :| [2,3]
|
||||
-- 1 :| [2,3]
|
||||
|
||||
c :: NonEmpty Integer
|
||||
c = fromList []
|
||||
-- *** Exception: NonEmpty.fromList: empty list
|
||||
|
||||
d :: Integer
|
||||
d = foldl1 (+) $ fromList [1..100]
|
||||
-- 5050
|
||||
@ -4,14 +4,18 @@
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
|
||||
data Size = None | Many
|
||||
data Size = Empty | NonEmpty
|
||||
|
||||
data List a b where
|
||||
Nil :: List None a
|
||||
Cons :: a -> List b a -> List Many a
|
||||
Nil :: List Empty a
|
||||
Cons :: a -> List b a -> List NonEmpty a
|
||||
|
||||
head' :: List Many a -> a
|
||||
head' :: List NonEmpty a -> a
|
||||
head' (Cons x _) = x
|
||||
|
||||
example1 :: Int
|
||||
example1 = head' (1 `Cons` (2 `Cons` Nil))
|
||||
|
||||
-- Cannot match type Empty with NonEmpty
|
||||
example2 :: Int
|
||||
example2 = head' Nil
|
||||
|
||||
13
src/overloadedlist.hs
Normal file
13
src/overloadedlist.hs
Normal file
@ -0,0 +1,13 @@
|
||||
{-# LANGUAGE OverloadedLists #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import GHC.Exts (IsList(..))
|
||||
|
||||
instance (Ord k) => IsList (Map.Map k v) where
|
||||
type Item (Map.Map k v) = (k,v)
|
||||
fromList = Map.fromList
|
||||
toList = Map.toList
|
||||
|
||||
example1 :: Map.Map String Int
|
||||
example1 = [("a", 1), ("b", 2)]
|
||||
42
src/par.hs
Normal file
42
src/par.hs
Normal file
@ -0,0 +1,42 @@
|
||||
import Control.Monad
|
||||
import Control.Monad.Par
|
||||
|
||||
f, g :: Int -> Int
|
||||
f x = x + 10
|
||||
g x = x * 10
|
||||
|
||||
-- f x g x
|
||||
-- \ /
|
||||
-- a + b
|
||||
-- / \
|
||||
-- f (a+b) g (a+b)
|
||||
-- \ /
|
||||
-- (d,e)
|
||||
|
||||
example1 :: Int -> (Int, Int)
|
||||
example1 x = runPar $ do
|
||||
[a,b,c,d,e] <- replicateM 5 new
|
||||
fork (put a (f x))
|
||||
fork (put b (g x))
|
||||
a' <- get a
|
||||
b' <- get b
|
||||
fork (put c (a' + b'))
|
||||
c' <- get c
|
||||
fork (put d (f c'))
|
||||
fork (put e (g c'))
|
||||
d' <- get d
|
||||
e' <- get e
|
||||
return (d', e')
|
||||
|
||||
example2 :: [Int]
|
||||
example2 = runPar $ do
|
||||
xs <- parMap (+1) [1..25]
|
||||
return xs
|
||||
|
||||
-- foldr (+) 0 (map (^2) [1..xs])
|
||||
example3 :: Int -> Int
|
||||
example3 n = runPar $ do
|
||||
let range = (InclusiveRange 1 n)
|
||||
let mapper x = return (x^2)
|
||||
let reducer x y = return (x+y)
|
||||
parMapReduceRangeThresh 10 range mapper reducer 0
|
||||
@ -37,9 +37,7 @@ data Decl
|
||||
| OpDecl OperatorDef
|
||||
deriving (Show)
|
||||
|
||||
|
||||
type Op x = Ex.Operator String ParseState Identity x
|
||||
|
||||
type Parser a = Parsec String ParseState a
|
||||
data ParseState = ParseState [OperatorDef] deriving Show
|
||||
|
||||
@ -47,9 +45,7 @@ data OperatorDef = OperatorDef {
|
||||
oassoc :: Assoc
|
||||
, oprec :: Integer
|
||||
, otok :: Name
|
||||
}
|
||||
deriving Show
|
||||
|
||||
} deriving Show
|
||||
|
||||
lexer :: Tok.GenTokenParser String u Identity
|
||||
lexer = Tok.makeTokenParser style
|
||||
@ -61,18 +57,18 @@ lexer = Tok.makeTokenParser style
|
||||
, Tok.commentLine = "--"
|
||||
}
|
||||
|
||||
reserved = Tok.reserved lexer
|
||||
reserved = Tok.reserved lexer
|
||||
reservedOp = Tok.reservedOp lexer
|
||||
identifier = Tok.identifier lexer
|
||||
parens = Tok.parens lexer
|
||||
brackets = Tok.brackets lexer
|
||||
braces = Tok.braces lexer
|
||||
commaSep = Tok.commaSep lexer
|
||||
semi = Tok.semi lexer
|
||||
integer = Tok.integer lexer
|
||||
chr = Tok.charLiteral lexer
|
||||
str = Tok.stringLiteral lexer
|
||||
operator = Tok.operator lexer
|
||||
parens = Tok.parens lexer
|
||||
brackets = Tok.brackets lexer
|
||||
braces = Tok.braces lexer
|
||||
commaSep = Tok.commaSep lexer
|
||||
semi = Tok.semi lexer
|
||||
integer = Tok.integer lexer
|
||||
chr = Tok.charLiteral lexer
|
||||
str = Tok.stringLiteral lexer
|
||||
operator = Tok.operator lexer
|
||||
|
||||
contents :: Parser a -> Parser a
|
||||
contents p = do
|
||||
|
||||
@ -19,8 +19,6 @@ data Expr
|
||||
|
||||
data Binop = Add | Sub | Mul deriving Show
|
||||
|
||||
--
|
||||
|
||||
lexer :: Tok.TokenParser ()
|
||||
lexer = Tok.makeTokenParser style
|
||||
where ops = ["->","\\","+","*","-","="]
|
||||
@ -42,8 +40,6 @@ contents p = do
|
||||
eof
|
||||
return r
|
||||
|
||||
--
|
||||
|
||||
natural :: Parser Integer
|
||||
natural = Tok.natural lexer
|
||||
|
||||
|
||||
35
src/patterns.hs
Normal file
35
src/patterns.hs
Normal file
@ -0,0 +1,35 @@
|
||||
{-# LANGUAGE PatternSynonyms #-}
|
||||
|
||||
import Data.List (foldl1')
|
||||
|
||||
type Name = String
|
||||
type TVar = String
|
||||
type TyCon = String
|
||||
|
||||
data Type
|
||||
= TVar TVar
|
||||
| TCon TyCon
|
||||
| TApp Type Type
|
||||
deriving (Show, Eq, Ord)
|
||||
|
||||
|
||||
pattern TArr t1 t2 = TApp (TApp (TCon "(->)") t1) t2
|
||||
|
||||
tapp :: TyCon -> [Type] -> Type
|
||||
tapp tcon args = foldl TApp (TCon tcon) args
|
||||
|
||||
arr :: [Type] -> Type
|
||||
arr ts = foldl1' (\t1 t2 -> tapp "(->)" [t1, t2]) ts
|
||||
|
||||
elimTArr :: Type -> [Type]
|
||||
elimTArr (TArr (TArr t1 t2) t3) = t1 : t2 : elimTArr t3
|
||||
elimTArr (TArr t1 t2) = t1 : elimTArr t2
|
||||
elimTArr t = [t]
|
||||
|
||||
-- (->) a ((->) b a)
|
||||
-- a -> b -> a
|
||||
to :: Type
|
||||
to = arr [TVar "a", TVar "b", TVar "a"]
|
||||
|
||||
from :: [Type]
|
||||
from = elimTArr to
|
||||
32
src/phantom.hs
Normal file
32
src/phantom.hs
Normal file
@ -0,0 +1,32 @@
|
||||
import Data.Void
|
||||
|
||||
data Foo tag a = Foo a
|
||||
|
||||
combine :: Num a => Foo tag a -> Foo tag a -> Foo tag a
|
||||
combine (Foo a) (Foo b) = Foo (a+b)
|
||||
|
||||
-- All identical at the value level, but differ at the type level.
|
||||
a :: Foo () Int
|
||||
a = Foo 1
|
||||
|
||||
b :: Foo t Int
|
||||
b = Foo 1
|
||||
|
||||
c :: Foo Void Int
|
||||
c = Foo 1
|
||||
|
||||
-- () ~ ()
|
||||
example1 :: Foo () Int
|
||||
example1 = combine a a
|
||||
|
||||
-- t ~ ()
|
||||
example2 :: Foo () Int
|
||||
example2 = combine a b
|
||||
|
||||
-- t0 ~ t1
|
||||
example3 :: Foo t Int
|
||||
example3 = combine b b
|
||||
|
||||
-- Couldn't match type `t' with `Void'
|
||||
example4 :: Foo t Int
|
||||
example4 = combine b c
|
||||
45
src/phoas.hs
Normal file
45
src/phoas.hs
Normal file
@ -0,0 +1,45 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
data ExprP a
|
||||
= VarP a
|
||||
| AppP (ExprP a) (ExprP a)
|
||||
| LamP (a -> ExprP a)
|
||||
| LitP Integer
|
||||
|
||||
data Value
|
||||
= VLit Integer
|
||||
| VFun (Value -> Value)
|
||||
|
||||
fromVFun :: Value -> (Value -> Value)
|
||||
fromVFun val = case val of
|
||||
VFun f -> f
|
||||
_ -> error "not a function"
|
||||
|
||||
fromVLit :: Value -> Integer
|
||||
fromVLit val = case val of
|
||||
VLit n -> n
|
||||
_ -> error "not a integer"
|
||||
|
||||
newtype Expr = Expr { unExpr :: forall a . ExprP a }
|
||||
|
||||
eval :: Expr -> Value
|
||||
eval e = ev (unExpr e) where
|
||||
ev (LamP f) = VFun(ev . f)
|
||||
ev (VarP v) = v
|
||||
ev (AppP e1 e2) = fromVFun (ev e1) (ev e2)
|
||||
ev (LitP n) = VLit n
|
||||
|
||||
i :: ExprP a
|
||||
i = LamP (\a -> VarP a)
|
||||
|
||||
k :: ExprP a
|
||||
k = LamP (\x -> LamP (\y -> VarP x))
|
||||
|
||||
s :: ExprP a
|
||||
s = LamP (\x -> LamP (\y -> LamP (\z -> AppP (AppP (VarP x) (VarP z)) (AppP (VarP y) (VarP z)))))
|
||||
|
||||
skk :: ExprP a
|
||||
skk = AppP (AppP s k) k
|
||||
|
||||
example :: Integer
|
||||
example = fromVLit $ eval $ Expr (AppP skk (LitP 3))
|
||||
@ -1,19 +1,24 @@
|
||||
import Pipes
|
||||
import Pipes.Prelude
|
||||
import Pipes.Prelude as P
|
||||
import Control.Monad
|
||||
import Control.Monad.Identity
|
||||
|
||||
a :: Producer Int Identity ()
|
||||
a = forM_ [1..10] yield
|
||||
|
||||
b :: Pipe Int Int Identity ()
|
||||
b = forever $ do
|
||||
x <- await
|
||||
yield (x*2)
|
||||
yield (x*3)
|
||||
yield (x*4)
|
||||
|
||||
c :: Pipe Int Int Identity ()
|
||||
c = forever $ do
|
||||
x <- await
|
||||
if (x `mod` 2) == 0
|
||||
then yield x
|
||||
else return ()
|
||||
|
||||
result = toList $ a >-> b >-> c
|
||||
result :: [Int]
|
||||
result = P.toList $ a >-> b >-> c
|
||||
|
||||
14
src/pipes_file.hs
Normal file
14
src/pipes_file.hs
Normal file
@ -0,0 +1,14 @@
|
||||
import Pipes
|
||||
import Pipes.Prelude as P
|
||||
import System.IO
|
||||
|
||||
readF :: FilePath -> Producer String IO ()
|
||||
readF file = do
|
||||
lift $ putStrLn $ "Opened" ++ file
|
||||
h <- lift $ openFile file ReadMode
|
||||
fromHandle h
|
||||
lift $ putStrLn $ "Closed" ++ file
|
||||
lift $ hClose h
|
||||
|
||||
main :: IO ()
|
||||
main = runEffect $ readF "foo.txt" >-> P.take 3 >-> stdoutLn
|
||||
50
src/pipes_safe.hs
Normal file
50
src/pipes_safe.hs
Normal file
@ -0,0 +1,50 @@
|
||||
import Pipes
|
||||
import Pipes.Safe
|
||||
import qualified Pipes.Prelude as P
|
||||
|
||||
import System.Timeout (timeout)
|
||||
import Data.ByteString.Char8
|
||||
import qualified System.ZMQ as ZMQ
|
||||
|
||||
data Opts = Opts
|
||||
{ _addr :: String -- ^ ZMQ socket address
|
||||
, _timeout :: Int -- ^ Time in milliseconds for socket timeout
|
||||
}
|
||||
|
||||
recvTimeout :: Opts -> ZMQ.Socket a -> Producer ByteString (SafeT IO) ()
|
||||
recvTimeout opts sock = do
|
||||
body <- liftIO $ timeout (_timeout opts) (ZMQ.receive sock [])
|
||||
case body of
|
||||
Just msg -> do
|
||||
liftIO $ ZMQ.send sock msg []
|
||||
yield msg
|
||||
recvTimeout opts sock
|
||||
Nothing -> liftIO $ print "socket timed out"
|
||||
|
||||
collect :: ZMQ.Context
|
||||
-> Opts
|
||||
-> Producer ByteString (SafeT IO) ()
|
||||
collect ctx opts = bracket zinit zclose (recvTimeout opts)
|
||||
where
|
||||
-- Initialize the socket
|
||||
zinit = do
|
||||
liftIO $ print "waiting for messages"
|
||||
sock <- ZMQ.socket ctx ZMQ.Rep
|
||||
ZMQ.bind sock (_addr opts)
|
||||
return sock
|
||||
|
||||
-- On timeout or completion guarantee the socket get closed.
|
||||
zclose sock = do
|
||||
liftIO $ print "finalizing"
|
||||
ZMQ.close sock
|
||||
|
||||
runZmq :: ZMQ.Context -> Opts -> IO ()
|
||||
runZmq ctx opts = runSafeT $ runEffect $
|
||||
collect ctx opts >-> P.take 10 >-> P.print
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
ctx <- ZMQ.init 1
|
||||
let opts = Opts {_addr = "tcp://127.0.0.1:8000", _timeout = 1000000 }
|
||||
runZmq ctx opts
|
||||
ZMQ.term ctx
|
||||
22
src/prim.hs
Normal file
22
src/prim.hs
Normal file
@ -0,0 +1,22 @@
|
||||
{-# LANGUAGE BangPatterns, MagicHash, UnboxedTuples #-}
|
||||
|
||||
import GHC.Exts
|
||||
import GHC.Prim
|
||||
|
||||
ex1 :: Bool
|
||||
ex1 = gtChar# a# b#
|
||||
where
|
||||
!(C# a#) = 'a'
|
||||
!(C# b#) = 'b'
|
||||
|
||||
ex2 :: Int
|
||||
ex2 = I# (a# +# b#)
|
||||
where
|
||||
!(I# a#) = 1
|
||||
!(I# b#) = 2
|
||||
|
||||
ex3 :: Int
|
||||
ex3 = (I# (1# +# 2# *# 3# +# 4#))
|
||||
|
||||
ex4 :: (Int, Int)
|
||||
ex4 = (I# (dataToTag# False), I# (dataToTag# True))
|
||||
41
src/prism.hs
Normal file
41
src/prism.hs
Normal file
@ -0,0 +1,41 @@
|
||||
import Control.Lens
|
||||
|
||||
main = return ()
|
||||
|
||||
|
||||
data Value = I Int
|
||||
| D Double
|
||||
deriving Show
|
||||
|
||||
_I :: Prism' Value Int
|
||||
_I = prism remit review
|
||||
where
|
||||
remit :: Int -> Value
|
||||
remit a = I a
|
||||
|
||||
review :: Value -> Either Value Int
|
||||
review (I a) = Right a
|
||||
review a = Left a
|
||||
|
||||
_D :: Prism' Value Double
|
||||
_D = prism remit review
|
||||
where
|
||||
remit :: Double -> Value
|
||||
remit a = D a
|
||||
|
||||
review :: Value -> Either Value Double
|
||||
review (D a) = Right a
|
||||
review a = Left a
|
||||
|
||||
|
||||
test1 :: Maybe Int
|
||||
test1 = (I 42) ^? _I
|
||||
|
||||
test2 :: Value
|
||||
test2 = 42 ^. re _I
|
||||
|
||||
test3 :: Value
|
||||
test3 = over _I succ (I 2)
|
||||
|
||||
test4 :: Value
|
||||
test4 = over _I succ (D 2.71)
|
||||
183
src/prism_impl.hs
Normal file
183
src/prism_impl.hs
Normal file
@ -0,0 +1,183 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE NoMonomorphismRestriction #-}
|
||||
|
||||
import Data.Functor
|
||||
import Data.Monoid
|
||||
|
||||
import Control.Applicative
|
||||
import Data.Traversable
|
||||
|
||||
newtype Getting c a = Getting { unGetting :: c }
|
||||
newtype Setting a = Setting { unSetting :: a }
|
||||
|
||||
type LensLike f s t a b = (a -> f b) -> s -> f t
|
||||
|
||||
type Lens a a' b b' = forall f. Functor f => LensLike f a a' b b'
|
||||
type Lens' a b = Lens a a b b
|
||||
|
||||
type Prism a a' b b' = forall f. Applicative f => (b -> f b') -> (a -> f a')
|
||||
type Prism' a b = Prism a a b b
|
||||
|
||||
type Setter a a' b b' = LensLike Setting a a' b b'
|
||||
type Setter' a b = Setter a a b b
|
||||
|
||||
type Getter a c = forall r d b. (c -> Getting r d) -> a -> Getting r b
|
||||
|
||||
type FoldLike r a a' b b' = LensLike (Getting r) a a' b b'
|
||||
|
||||
instance Functor (Getting c) where
|
||||
fmap _ (Getting c) = Getting c
|
||||
|
||||
instance Monoid c => Applicative (Getting c) where
|
||||
pure _ = Getting mempty
|
||||
Getting a <*> Getting b = Getting (a `mappend` b)
|
||||
|
||||
class Functor f => Phantom f where
|
||||
coerce :: f a -> f b
|
||||
|
||||
instance Phantom (Getting c) where
|
||||
coerce (Getting c) = Getting c
|
||||
|
||||
instance Functor Setting where
|
||||
fmap f (Setting a) = Setting (f a)
|
||||
|
||||
instance Applicative Setting where
|
||||
pure = Setting
|
||||
Setting f <*> Setting a = Setting (f a)
|
||||
|
||||
|
||||
lens :: (a -> b) -> (a -> b' -> a') -> Lens a a' b b'
|
||||
lens getter setter f a = fmap (setter a) (f (getter a))
|
||||
|
||||
(.~) :: Setter a a' b b' -> b' -> a -> a'
|
||||
l .~ b = l %~ const b
|
||||
|
||||
view :: FoldLike b a a' b b' -> a -> b
|
||||
view l = unGetting . l Getting
|
||||
|
||||
over :: Setter a a' b b' -> (b -> b') -> a -> a'
|
||||
over l = (l %~)
|
||||
|
||||
set :: Setter a a' b b' -> b' -> a -> a'
|
||||
set = (.~)
|
||||
|
||||
(%~) :: Setter a a' b b' -> (b -> b') -> a -> a'
|
||||
l %~ f = unSetting . l (Setting . f)
|
||||
|
||||
compose :: Lens a a' b b' -> Lens b b' c c' -> Lens a a' c c'
|
||||
compose l s = l . s
|
||||
|
||||
id' :: Lens' a a
|
||||
id' = id
|
||||
|
||||
infixl 1 &
|
||||
infixr 4 .~
|
||||
infixr 4 %~
|
||||
infixr 8 ^.
|
||||
|
||||
(^.) :: a -> FoldLike b a a' b b' -> b
|
||||
(^.) = flip view
|
||||
|
||||
(&) :: a -> (a -> b) -> b
|
||||
(&) = flip ($)
|
||||
|
||||
(+~), (-~), (*~) :: Num b => Setter' a b -> b -> a -> a
|
||||
f +~ b = f %~ (+b)
|
||||
f -~ b = f %~ (subtract b)
|
||||
f *~ b = f %~ (*b)
|
||||
|
||||
|
||||
infixr 8 ^?
|
||||
infixr 8 ^..
|
||||
|
||||
views :: FoldLike r a a' b b' -> (b -> r) -> a -> r
|
||||
views l f = unGetting . l (Getting . f)
|
||||
|
||||
(^?) :: a -> FoldLike (First b) a a' b b' -> Maybe b
|
||||
x ^? l = firstOf l x
|
||||
|
||||
(^..) :: a -> FoldLike [b] a a' b b' -> [b]
|
||||
x ^.. l = toListOf l x
|
||||
|
||||
toListOf :: FoldLike [b] a a' b b' -> a -> [b]
|
||||
toListOf l = views l (:[])
|
||||
|
||||
firstOf :: FoldLike (First b) a a' b b' -> a -> Maybe b
|
||||
firstOf l = getFirst . views l (First . Just)
|
||||
|
||||
prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b
|
||||
prism rm rv f a =
|
||||
case rv a of
|
||||
Right x -> fmap rm (f x)
|
||||
Left x -> pure x
|
||||
|
||||
prism' :: (b -> s) -> (s -> Maybe a) -> Prism s s a b
|
||||
prism' rm rv f a =
|
||||
case rv a of
|
||||
Just x -> fmap rm (f x)
|
||||
Nothing -> pure a
|
||||
|
||||
_just :: Prism (Maybe a) (Maybe b) a b
|
||||
_just = prism Just $ maybe (Left Nothing) Right
|
||||
|
||||
_nothing :: Prism' (Maybe a) ()
|
||||
_nothing = prism' (const Nothing) $ maybe (Just ()) (const Nothing)
|
||||
|
||||
_right :: Prism (Either c a) (Either c b) a b
|
||||
_right = prism Right $ either (Left . Left) Right
|
||||
|
||||
_left :: Prism (Either a c) (Either b c) a b
|
||||
_left = prism Left $ either Right (Left . Right)
|
||||
|
||||
to :: (s -> a) -> Getter s a
|
||||
to p f = coerce . f . p
|
||||
|
||||
|
||||
|
||||
pair :: (Int, Char)
|
||||
pair = (1, 'b')
|
||||
|
||||
_1 :: Lens (a, b) (a', b) a a'
|
||||
_1 f (a, b) = (\x -> (x, b)) <$> f a
|
||||
|
||||
_2 :: Lens (a, b) (a, b') b b'
|
||||
_2 f (a, b) = (\x -> (a, x)) <$> f b
|
||||
|
||||
both :: Prism (a, a) (b, b) a b
|
||||
both f (a, b) = (,) <$> f a <*> f b
|
||||
|
||||
ex1 = pair ^. _1
|
||||
ex2 = pair ^. _2
|
||||
ex3 = pair & _1 .~ "a"
|
||||
ex4 = pair & (_1 %~ (+1))
|
||||
. (_2 .~ 1)
|
||||
|
||||
ex5 = (1, 2) & both .~ 1
|
||||
ex6 = Just 3 & _just +~ 1
|
||||
ex7 = (Left 3) ^? _left
|
||||
ex8 = over traverse (+1) [1..25]
|
||||
|
||||
data Value
|
||||
= I Int
|
||||
| D Double
|
||||
deriving Show
|
||||
|
||||
_I :: Prism' Value Int
|
||||
_I = prism remit review
|
||||
where
|
||||
remit :: Int -> Value
|
||||
remit a = I a
|
||||
|
||||
review :: Value -> Either Value Int
|
||||
review (I a) = Right a
|
||||
review a = Left a
|
||||
|
||||
ex9 :: Maybe Int
|
||||
ex9 = (I 42) ^? _I
|
||||
|
||||
ex10 :: Value
|
||||
ex10 = over _I succ (I 2)
|
||||
|
||||
ex11 :: Value
|
||||
ex11 = over _I succ (D 2.71)
|
||||
@ -6,9 +6,9 @@
|
||||
data Z
|
||||
data S n
|
||||
|
||||
data Nat n where
|
||||
Zero :: Nat Z
|
||||
Succ :: Nat n -> Nat (S n)
|
||||
data SNat n where
|
||||
Zero :: SNat Z
|
||||
Succ :: SNat n -> SNat (S n)
|
||||
|
||||
data Eql a b where
|
||||
Refl :: Eql a a
|
||||
@ -17,17 +17,23 @@ type family Add m n
|
||||
type instance Add Z n = n
|
||||
type instance Add (S m) n = S (Add m n)
|
||||
|
||||
type family Pred n
|
||||
type instance Pred Z = Z
|
||||
type instance Pred (S n) = n
|
||||
|
||||
add :: Nat n -> Nat m -> Nat (Add n m)
|
||||
add :: SNat n -> SNat m -> SNat (Add n m)
|
||||
add Zero m = m
|
||||
add (Succ n) m = Succ (add n m)
|
||||
|
||||
cong :: Eql a b -> Eql (f a) (f b)
|
||||
cong Refl = Refl
|
||||
|
||||
plus_zero :: forall n. Nat n -> Eql (Add n Z) n
|
||||
-- ∀n. 0 + suc n = suc n
|
||||
plus_suc :: forall n. SNat n
|
||||
-> Eql (Add Z (S n)) (S n)
|
||||
plus_suc Zero = Refl
|
||||
plus_suc (Succ n) = cong (plus_suc n)
|
||||
|
||||
-- ∀n. 0 + n = n
|
||||
plus_zero :: forall n. SNat n
|
||||
-> Eql (Add Z n) n
|
||||
plus_zero Zero = Refl
|
||||
plus_zero (Succ n) = cong (plus_zero n)
|
||||
|
||||
main = return ()
|
||||
35
src/propositional_equal.hs
Normal file
35
src/propositional_equal.hs
Normal file
@ -0,0 +1,35 @@
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE ExplicitForAll #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
|
||||
-- a ≡ b
|
||||
data a :~: b where
|
||||
Refl :: a :~: a
|
||||
|
||||
-- (f : A → B) {x y} → x ≡ y → f x ≡ f y
|
||||
cong :: a :~: b -> (f a) :~: (f b)
|
||||
cong Refl = Refl
|
||||
|
||||
-- {a b : A} → a ≡ b → a ≡ b
|
||||
sym :: a :~: b -> b :~: a
|
||||
sym Refl = Refl
|
||||
|
||||
-- {a b c : A} → a ≡ b → b ≡ c → a ≡ c
|
||||
trans :: a :~: b -> b :~: c -> a :~: c
|
||||
trans Refl Refl = Refl
|
||||
|
||||
-- {a b : A} → a ≡ b → a → b
|
||||
cast :: a :~: b -> a -> b
|
||||
cast Refl = id
|
||||
|
||||
|
||||
a :: forall n. n :~: n
|
||||
a = Refl
|
||||
|
||||
b :: forall n. (Maybe n) :~: (Maybe n)
|
||||
b = Refl
|
||||
|
||||
c :: forall. Eql () :~: ()
|
||||
c = Refl
|
||||
15
src/quasiquote_use.hs
Normal file
15
src/quasiquote_use.hs
Normal file
@ -0,0 +1,15 @@
|
||||
{-# LANGUAGE QuasiQuotes #-}
|
||||
|
||||
import Quasiquote
|
||||
|
||||
a :: Expr
|
||||
a = [calc|true|]
|
||||
-- Tr
|
||||
|
||||
b :: Expr
|
||||
b = [calc|succ (succ 0)|]
|
||||
-- Succ (Succ Zero)
|
||||
|
||||
c :: Expr
|
||||
c = [calc|pred (succ 0)|]
|
||||
-- Pred (Succ Zero)
|
||||
51
src/quickspec.hs
Normal file
51
src/quickspec.hs
Normal file
@ -0,0 +1,51 @@
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
|
||||
import Data.List
|
||||
import Data.Typeable
|
||||
|
||||
import Test.QuickSpec hiding (lists, bools, arith)
|
||||
import Test.QuickCheck
|
||||
|
||||
type Var k a = (Typeable a, Arbitrary a, CoArbitrary a, k a)
|
||||
|
||||
listCons :: forall a. Var Ord a => a -> Sig
|
||||
listCons a = background
|
||||
[
|
||||
"[]" `fun0` ([] :: [a]),
|
||||
":" `fun2` ((:) :: a -> [a] -> [a])
|
||||
]
|
||||
|
||||
lists :: forall a. Var Ord a => a -> [Sig]
|
||||
lists a =
|
||||
[
|
||||
-- Names to print arbitrary variables
|
||||
funs',
|
||||
funvars',
|
||||
vars',
|
||||
|
||||
-- Ambient definitions
|
||||
listCons a,
|
||||
|
||||
-- Expressions to deduce properties of
|
||||
"sort" `fun1` (sort :: [a] -> [a]),
|
||||
"map" `fun2` (map :: (a -> a) -> [a] -> [a]),
|
||||
"id" `fun1` (id :: [a] -> [a]),
|
||||
"reverse" `fun1` (reverse :: [a] -> [a]),
|
||||
"minimum" `fun1` (minimum :: [a] -> a),
|
||||
"length" `fun1` (length :: [a] -> Int),
|
||||
"++" `fun2` ((++) :: [a] -> [a] -> [a])
|
||||
]
|
||||
|
||||
where
|
||||
funs' = funs (undefined :: a)
|
||||
funvars' = vars ["f", "g", "h"] (undefined :: a -> a)
|
||||
vars' = ["xs", "ys", "zs"] `vars` (undefined :: [a])
|
||||
|
||||
|
||||
tvar :: A
|
||||
tvar = undefined
|
||||
|
||||
main :: IO ()
|
||||
main = quickSpec (lists tvar)
|
||||
14
src/rankn.hs
Normal file
14
src/rankn.hs
Normal file
@ -0,0 +1,14 @@
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
-- Can't unify ( Bool ~ Char )
|
||||
rank1 :: forall a. (a -> a) -> (Bool, Char)
|
||||
rank1 f = (f True, f 'a')
|
||||
|
||||
rank2 :: (forall a. a -> a) -> (Bool, Char)
|
||||
rank2 f = (f True, f 'a')
|
||||
|
||||
auto :: (forall a. a -> a) -> (forall b. b -> b)
|
||||
auto x = x
|
||||
|
||||
xauto :: forall a. (forall b. b -> b) -> a -> a
|
||||
xauto f = f
|
||||
@ -1,11 +1,11 @@
|
||||
import Control.Monad.Reader
|
||||
|
||||
data MyState = MyState
|
||||
data MyContext = MyContext
|
||||
{ foo :: String
|
||||
, bar :: Int
|
||||
} deriving (Show)
|
||||
|
||||
computation :: Reader MyState (Maybe String)
|
||||
computation :: Reader MyContext (Maybe String)
|
||||
computation = do
|
||||
n <- asks bar
|
||||
x <- asks foo
|
||||
@ -13,8 +13,8 @@ computation = do
|
||||
then return (Just x)
|
||||
else return Nothing
|
||||
|
||||
example1 :: Maybe String
|
||||
example1 = runReader computation $ MyState "hello!" 1
|
||||
ex1 :: Maybe String
|
||||
ex1 = runReader computation $ MyContext "hello" 1
|
||||
|
||||
example2 :: Maybe String
|
||||
example2 = runReader computation $ MyState "example!" 0
|
||||
ex2 :: Maybe String
|
||||
ex2 = runReader computation $ MyContext "haskell" 0
|
||||
|
||||
64
src/reverse.hs
Normal file
64
src/reverse.hs
Normal file
@ -0,0 +1,64 @@
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE ExplicitForAll #-}
|
||||
|
||||
import Data.Type.Equality
|
||||
|
||||
data Nat = Z | S Nat
|
||||
|
||||
data SNat n where
|
||||
Zero :: SNat Z
|
||||
Succ :: SNat n -> SNat (S n)
|
||||
|
||||
data Vec :: * -> Nat -> * where
|
||||
Nil :: Vec a Z
|
||||
Cons :: a -> Vec a n -> Vec a (S n)
|
||||
|
||||
instance Show a => Show (Vec a n) where
|
||||
show Nil = "Nil"
|
||||
show (Cons x xs) = "Cons " ++ show x ++ " (" ++ show xs ++ ")"
|
||||
|
||||
type family (m :: Nat) :+ (n :: Nat) :: Nat where
|
||||
Z :+ n = n
|
||||
S m :+ n = S (m :+ n)
|
||||
|
||||
-- (a ~ b) implies (f a ~ f b)
|
||||
cong :: a :~: b -> f a :~: f b
|
||||
cong Refl = Refl
|
||||
|
||||
-- (a ~ b) implies (f a) implies (f b)
|
||||
subst :: a :~: b -> f a -> f b
|
||||
subst Refl = id
|
||||
|
||||
plus_zero :: forall n. SNat n -> (n :+ Z) :~: n
|
||||
plus_zero Zero = Refl
|
||||
plus_zero (Succ n) = cong (plus_zero n)
|
||||
|
||||
plus_suc :: forall n m. SNat n -> SNat m -> (n :+ (S m)) :~: (S (n :+ m))
|
||||
plus_suc Zero m = Refl
|
||||
plus_suc (Succ n) m = cong (plus_suc n m)
|
||||
|
||||
size :: Vec a n -> SNat n
|
||||
size Nil = Zero
|
||||
size (Cons _ xs) = Succ $ size xs
|
||||
|
||||
reverse :: forall n a. Vec a n -> Vec a n
|
||||
reverse xs = subst (plus_zero (size xs)) $ go Nil xs
|
||||
where
|
||||
go :: Vec a m -> Vec a k -> Vec a (k :+ m)
|
||||
go acc Nil = acc
|
||||
go acc (Cons x xs) = subst (plus_suc (size xs) (size acc)) $ go (Cons x acc) xs
|
||||
|
||||
append :: Vec a n -> Vec a m -> Vec a (n :+ m)
|
||||
append (Cons x xs) ys = Cons x (append xs ys)
|
||||
append Nil ys = ys
|
||||
|
||||
vec :: Vec Int (S (S (S Z)))
|
||||
vec = 1 `Cons` (2 `Cons` (3 `Cons` Nil))
|
||||
|
||||
test :: Vec Int (S (S (S Z)))
|
||||
test = Main.reverse vec
|
||||
47
src/reverse_nat.hs
Normal file
47
src/reverse_nat.hs
Normal file
@ -0,0 +1,47 @@
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE ExplicitForAll #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
import Data.Proxy
|
||||
import GHC.TypeLits
|
||||
import Data.Type.Equality
|
||||
|
||||
type family Z :: Nat where
|
||||
Z = 0
|
||||
|
||||
type family S (n :: Nat) :: Nat where
|
||||
S n = n + 1
|
||||
|
||||
eq_one :: 1 :~: 1
|
||||
eq_one = Refl
|
||||
|
||||
eq_one_one :: 1 + 1 :~: 2
|
||||
eq_one_one = Refl
|
||||
|
||||
cong :: a :~: b -> f a :~: f b
|
||||
cong Refl = Refl
|
||||
|
||||
subst :: a :~: b -> f a -> f b
|
||||
subst Refl = id
|
||||
|
||||
plus_zero :: forall n. (n + Z) :~: n
|
||||
plus_zero = Refl
|
||||
|
||||
plus_one :: forall n. (n + S Z) :~: S n
|
||||
plus_one = Refl
|
||||
|
||||
-- No.
|
||||
-- plus_comm :: forall n m. (n + m) :~: (m + n)
|
||||
-- plus_comm = Refl
|
||||
|
||||
-- No.
|
||||
-- plus_suc :: forall n m. (n + (S m)) :~: (S (n + m))
|
||||
-- plus_suc = Refl
|
||||
|
||||
-- No.
|
||||
-- nontrivial :: forall n. (n + 1) :~: (1 + n)
|
||||
-- nontrivial = Refl
|
||||
23
src/role.hs
Normal file
23
src/role.hs
Normal file
@ -0,0 +1,23 @@
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
|
||||
newtype Age = MkAge { unAge :: Int }
|
||||
|
||||
type family Inspect x
|
||||
type instance Inspect Age = Int
|
||||
type instance Inspect Int = Bool
|
||||
|
||||
class Boom a where
|
||||
boom :: a -> Inspect a
|
||||
|
||||
instance Boom Int where
|
||||
boom = (== 0)
|
||||
|
||||
deriving instance Boom Age
|
||||
|
||||
-- GHC 7.6.3 exhibits undefined behavior
|
||||
failure = boom (MkAge 3)
|
||||
-- -6341068275333450897
|
||||
|
||||
main = return ()
|
||||
@ -3,8 +3,8 @@
|
||||
import Unsafe.Coerce
|
||||
import System.IO.Unsafe
|
||||
|
||||
sin :: String
|
||||
sin = unsafePerformIO $ getLine
|
||||
bad1 :: String
|
||||
bad1 = unsafePerformIO getLine
|
||||
|
||||
mortalsin :: a
|
||||
mortalsin = unsafeCoerce 3.14 ()
|
||||
bad2 :: a
|
||||
bad2 = unsafeCoerce 3.14 ()
|
||||
|
||||
19
src/scientific.hs
Normal file
19
src/scientific.hs
Normal file
@ -0,0 +1,19 @@
|
||||
import Data.Scientific
|
||||
|
||||
c, h, g, a, k :: Scientific
|
||||
c = scientific 299792458 (0) -- Speed of light
|
||||
h = scientific 662606957 (-42) -- Planck's constant
|
||||
g = scientific 667384 (-16) -- Gravitational constant
|
||||
a = scientific 729735257 (-11) -- Fine structure constant
|
||||
k = scientific 268545200 (-9) -- Khinchin Constant
|
||||
|
||||
tau :: Scientific
|
||||
tau = fromFloatDigits (2*pi)
|
||||
|
||||
maxDouble64 :: Double
|
||||
maxDouble64 = read "1.7976931348623159e308"
|
||||
-- Infinity
|
||||
|
||||
maxScientific :: Scientific
|
||||
maxScientific = read "1.7976931348623159e308"
|
||||
-- 1.7976931348623159e308
|
||||
21
src/scopedtvars.hs
Normal file
21
src/scopedtvars.hs
Normal file
@ -0,0 +1,21 @@
|
||||
{-# LANGUAGE ExplicitForAll #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
|
||||
poly :: forall a b c. a -> b -> c -> (a, a)
|
||||
poly x y z = (f x y, f x z)
|
||||
where
|
||||
-- second argument is universally quantified from inference
|
||||
-- f :: forall t0 t1. t0 -> t1 -> t0
|
||||
f x' _ = x'
|
||||
|
||||
mono :: forall a b c. a -> b -> c -> (a, a)
|
||||
mono x y z = (f x y, f x z)
|
||||
where
|
||||
-- b is not implictly universally quantified because it is in scope
|
||||
f :: a -> b -> a
|
||||
f x' _ = x'
|
||||
|
||||
example :: IO ()
|
||||
example = do
|
||||
x :: [Int] <- readLn
|
||||
print x
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user