A bunch of old stuff I hadn't commited

bug/.gitignore

@@ -0,0 +1,10 @@
+/bower_components/
+/node_modules/
+/.pulp-cache/
+/output/
+/generated-docs/
+/.psc-package/
+/.psc*
+/.purs*
+/.psa*
+/.spago

bug/packages.dhall

@@ -0,0 +1,6 @@
+let upstream =
+      https://github.com/purescript/package-sets/releases/download/psc-0.14.2-20210623/packages.dhall sha256:b3dcd9b0a1f6bffa4b5e61dc80e9f3fec2fca9405d591397a5076c8fe3aed1bc
+
+let packages = upstream with other = ./src/other/spago.dhall as Location
+
+in  packages

bug/spago.dhall

@@ -0,0 +1,5 @@
+{ name = "my-project"
+, dependencies = [ "console", "effect", "prelude", "psci-support", "other" ]
+, packages = ./packages.dhall
+, sources = [ "src/Maain.purs" ]
+}

bug/src/Main.purs

@@ -0,0 +1,11 @@
+module Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class (liftEffect)
+import Effect.Class.Console (logShow)
+import Foo (foo)
+
+main :: Effect Unit
+main = liftEffect $ logShow 12

bug/src/other/spago.dhall

@@ -0,0 +1,5 @@
+{ name = "my-other-project"
+, dependencies = [ "console", "effect", "prelude", "psci-support" ]
+, packages = ../../packages.dhall
+, sources = [ "./src/Foo.purs" ]
+}

bug/src/other/src/Foo.purs

@@ -0,0 +1,9 @@
+module Foo where
+
+import Prelude 
+
+class Foo a where
+    foo :: a -> a -> a
+
+instance Foo Int where
+    foo a b = a - b

bug/test/Main.purs

@@ -0,0 +1,11 @@
+module Test.Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"
+  log "You should add some tests."

compose/.gitignore

@@ -0,0 +1,10 @@
+/bower_components/
+/node_modules/
+/.pulp-cache/
+/output/
+/generated-docs/
+/.psc-package/
+/.psc*
+/.purs*
+/.psa*
+/.spago

compose/packages.dhall

@@ -0,0 +1,104 @@
+{-
+Welcome to your new Dhall package-set!
+
+Below are instructions for how to edit this file for most use
+cases, so that you don't need to know Dhall to use it.
+
+## Use Cases
+
+Most will want to do one or both of these options:
+1. Override/Patch a package's dependency
+2. Add a package not already in the default package set
+
+This file will continue to work whether you use one or both options.
+Instructions for each option are explained below.
+
+### Overriding/Patching a package
+
+Purpose:
+- Change a package's dependency to a newer/older release than the
+    default package set's release
+- Use your own modified version of some dependency that may
+    include new API, changed API, removed API by
+    using your custom git repo of the library rather than
+    the package set's repo
+
+Syntax:
+where `entityName` is one of the following:
+- dependencies
+- repo
+- version
+-------------------------------
+let upstream = --
+in  upstream
+  with packageName.entityName = "new value"
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with halogen.version = "master"
+  with halogen.repo = "https://example.com/path/to/git/repo.git"
+
+  with halogen-vdom.version = "v4.0.0"
+  with halogen-vdom.dependencies = [ "extra-dependency" ] # halogen-vdom.dependencies
+-------------------------------
+
+### Additions
+
+Purpose:
+- Add packages that aren't already included in the default package set
+
+Syntax:
+where `<version>` is:
+- a tag (i.e. "v4.0.0")
+- a branch (i.e. "master")
+- commit hash (i.e. "701f3e44aafb1a6459281714858fadf2c4c2a977")
+-------------------------------
+let upstream = --
+in  upstream
+  with new-package-name =
+    { dependencies =
+       [ "dependency1"
+       , "dependency2"
+       ]
+    , repo =
+       "https://example.com/path/to/git/repo.git"
+    , version =
+        "<version>"
+    }
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with benchotron =
+      { dependencies =
+          [ "arrays"
+          , "exists"
+          , "profunctor"
+          , "strings"
+          , "quickcheck"
+          , "lcg"
+          , "transformers"
+          , "foldable-traversable"
+          , "exceptions"
+          , "node-fs"
+          , "node-buffer"
+          , "node-readline"
+          , "datetime"
+          , "now"
+          ]
+      , repo =
+          "https://github.com/hdgarrood/purescript-benchotron.git"
+      , version =
+          "v7.0.0"
+      }
+-------------------------------
+-}
+let upstream =
+      https://github.com/purescript/package-sets/releases/download/psc-0.14.2-20210713/packages.dhall sha256:654c3148cb995f642c73b4508d987d9896e2ad3ea1d325a1e826c034c0d3cd7b
+
+in  upstream

compose/spago.dhall

@@ -0,0 +1,17 @@
+{-
+Welcome to a Spago project!
+You can edit this file as you like.
+
+Need help? See the following resources:
+- Spago documentation: https://github.com/purescript/spago
+- Dhall language tour: https://docs.dhall-lang.org/tutorials/Language-Tour.html
+
+When creating a new Spago project, you can use
+`spago init --no-comments` or `spago init -C`
+to generate this file without the comments in this block.
+-}
+{ name = "my-project"
+, dependencies = [ "console", "effect", "exists", "prelude", "psci-support" ]
+, packages = ./packages.dhall
+, sources = [ "src/**/*.purs", "test/**/*.purs" ]
+}

compose/src/Compose.purs

@@ -0,0 +1,10 @@
+module Compose where
+
+import Prelude hiding (bind, discard)
+
+
+bind :: forall a b c. (a -> b) -> (b -> c) -> (a -> c)
+bind = (>>>)
+
+discard :: forall a b c. (a -> b) -> (Unit -> b -> c) -> (a -> c)
+discard f g = f >>> g unit

compose/src/Main.purs

@@ -0,0 +1,44 @@
+module Main where
+
+import Prelude
+
+import Compose as Compose
+import Data.Exists (Exists)
+import Effect (Effect)
+import Effect.Class.Console (logShow)
+import Unsafe.Coerce (unsafeCoerce)
+
+
+c :: Int -> Int
+c = Compose.do
+    add2
+    double
+
+add2 :: Int -> Int
+add2 = (+) 2
+
+double :: Int -> Int
+double = (*) 2
+
+newtype I a = I a
+type EI = Exists I
+
+type Showable f = forall result. (forall r. Show r => f r -> result) -> result
+
+mkShowable :: forall a f. Show a => f a -> Showable f
+mkShowable a f = f a
+
+test :: String
+test = do
+  I something <- mkShowable $ I 0
+  show something
+  where
+  bind :: forall f result. Showable f -> (forall r. Show r => f r -> result) -> result 
+  bind e f = e f
+
+  magicShow :: forall r. r -> String
+  magicShow = unsafeCoerce
+
+main :: Effect Unit
+main = do
+  logShow $ c 3

compose/test/Main.purs

@@ -0,0 +1,11 @@
+module Test.Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"
+  log "You should add some tests."

existentials-blog/.gitignore

@@ -0,0 +1,10 @@
+/bower_components/
+/node_modules/
+/.pulp-cache/
+/output/
+/generated-docs/
+/.psc-package/
+/.psc*
+/.purs*
+/.psa*
+/.spago

existentials-blog/packages.dhall

@@ -0,0 +1,104 @@
+{-
+Welcome to your new Dhall package-set!
+
+Below are instructions for how to edit this file for most use
+cases, so that you don't need to know Dhall to use it.
+
+## Use Cases
+
+Most will want to do one or both of these options:
+1. Override/Patch a package's dependency
+2. Add a package not already in the default package set
+
+This file will continue to work whether you use one or both options.
+Instructions for each option are explained below.
+
+### Overriding/Patching a package
+
+Purpose:
+- Change a package's dependency to a newer/older release than the
+    default package set's release
+- Use your own modified version of some dependency that may
+    include new API, changed API, removed API by
+    using your custom git repo of the library rather than
+    the package set's repo
+
+Syntax:
+where `entityName` is one of the following:
+- dependencies
+- repo
+- version
+-------------------------------
+let upstream = --
+in  upstream
+  with packageName.entityName = "new value"
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with halogen.version = "master"
+  with halogen.repo = "https://example.com/path/to/git/repo.git"
+
+  with halogen-vdom.version = "v4.0.0"
+  with halogen-vdom.dependencies = [ "extra-dependency" ] # halogen-vdom.dependencies
+-------------------------------
+
+### Additions
+
+Purpose:
+- Add packages that aren't already included in the default package set
+
+Syntax:
+where `<version>` is:
+- a tag (i.e. "v4.0.0")
+- a branch (i.e. "master")
+- commit hash (i.e. "701f3e44aafb1a6459281714858fadf2c4c2a977")
+-------------------------------
+let upstream = --
+in  upstream
+  with new-package-name =
+    { dependencies =
+       [ "dependency1"
+       , "dependency2"
+       ]
+    , repo =
+       "https://example.com/path/to/git/repo.git"
+    , version =
+        "<version>"
+    }
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with benchotron =
+      { dependencies =
+          [ "arrays"
+          , "exists"
+          , "profunctor"
+          , "strings"
+          , "quickcheck"
+          , "lcg"
+          , "transformers"
+          , "foldable-traversable"
+          , "exceptions"
+          , "node-fs"
+          , "node-buffer"
+          , "node-readline"
+          , "datetime"
+          , "now"
+          ]
+      , repo =
+          "https://github.com/hdgarrood/purescript-benchotron.git"
+      , version =
+          "v7.0.0"
+      }
+-------------------------------
+-}
+let upstream =
+      https://github.com/purescript/package-sets/releases/download/psc-0.14.2-20210713/packages.dhall sha256:654c3148cb995f642c73b4508d987d9896e2ad3ea1d325a1e826c034c0d3cd7b
+
+in  upstream

existentials-blog/spago.dhall

@@ -0,0 +1,17 @@
+{-
+Welcome to a Spago project!
+You can edit this file as you like.
+
+Need help? See the following resources:
+- Spago documentation: https://github.com/purescript/spago
+- Dhall language tour: https://docs.dhall-lang.org/tutorials/Language-Tour.html
+
+When creating a new Spago project, you can use
+`spago init --no-comments` or `spago init -C`
+to generate this file without the comments in this block.
+-}
+{ name = "my-project"
+, dependencies = [ "console", "effect", "exists", "prelude", "psci-support" ]
+, packages = ./packages.dhall
+, sources = [ "src/**/*.purs", "test/**/*.purs" ]
+}

existentials-blog/src/Exists.purs

@@ -0,0 +1,17 @@
+module Exists where
+
+
+import Prelude
+
+import Data.Exists (Exists, mkExists)
+
+-- type Exists f = forall result. (forall a. f a (a -> result)) -> result
+
+type Forall :: forall k. (k -> Type) -> Type -> Type
+type Forall f r = forall a. f a -> r
+
+{- type Showable a f = Show a => f
+type EConstructor f = forall a. f a (a -> Exists f)
+
+mkShowable :: EConstructor Showable
+mkShowable a f = f a  -}

existentials-blog/src/Main.purs

@@ -0,0 +1,10 @@
+module Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"

existentials-blog/test/Main.purs

@@ -0,0 +1,11 @@
+module Test.Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"
+  log "You should add some tests."

existentials/packages.dhall

@@ -0,0 +1,104 @@
+{-
+Welcome to your new Dhall package-set!
+
+Below are instructions for how to edit this file for most use
+cases, so that you don't need to know Dhall to use it.
+
+## Use Cases
+
+Most will want to do one or both of these options:
+1. Override/Patch a package's dependency
+2. Add a package not already in the default package set
+
+This file will continue to work whether you use one or both options.
+Instructions for each option are explained below.
+
+### Overriding/Patching a package
+
+Purpose:
+- Change a package's dependency to a newer/older release than the
+    default package set's release
+- Use your own modified version of some dependency that may
+    include new API, changed API, removed API by
+    using your custom git repo of the library rather than
+    the package set's repo
+
+Syntax:
+where `entityName` is one of the following:
+- dependencies
+- repo
+- version
+-------------------------------
+let upstream = --
+in  upstream
+  with packageName.entityName = "new value"
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with halogen.version = "master"
+  with halogen.repo = "https://example.com/path/to/git/repo.git"
+
+  with halogen-vdom.version = "v4.0.0"
+  with halogen-vdom.dependencies = [ "extra-dependency" ] # halogen-vdom.dependencies
+-------------------------------
+
+### Additions
+
+Purpose:
+- Add packages that aren't already included in the default package set
+
+Syntax:
+where `<version>` is:
+- a tag (i.e. "v4.0.0")
+- a branch (i.e. "master")
+- commit hash (i.e. "701f3e44aafb1a6459281714858fadf2c4c2a977")
+-------------------------------
+let upstream = --
+in  upstream
+  with new-package-name =
+    { dependencies =
+       [ "dependency1"
+       , "dependency2"
+       ]
+    , repo =
+       "https://example.com/path/to/git/repo.git"
+    , version =
+        "<version>"
+    }
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with benchotron =
+      { dependencies =
+          [ "arrays"
+          , "exists"
+          , "profunctor"
+          , "strings"
+          , "quickcheck"
+          , "lcg"
+          , "transformers"
+          , "foldable-traversable"
+          , "exceptions"
+          , "node-fs"
+          , "node-buffer"
+          , "node-readline"
+          , "datetime"
+          , "now"
+          ]
+      , repo =
+          "https://github.com/hdgarrood/purescript-benchotron.git"
+      , version =
+          "v7.0.0"
+      }
+-------------------------------
+-}
+let upstream =
+      https://github.com/purescript/package-sets/releases/download/psc-0.14.1-20210419/packages.dhall sha256:d9a082ffb5c0fabf689574f0680e901ca6f924e01acdbece5eeedd951731375a
+
+in  upstream

existentials/spago.dhall

@@ -0,0 +1,17 @@
+{-
+Welcome to a Spago project!
+You can edit this file as you like.
+
+Need help? See the following resources:
+- Spago documentation: https://github.com/purescript/spago
+- Dhall language tour: https://docs.dhall-lang.org/tutorials/Language-Tour.html
+
+When creating a new Spago project, you can use
+`spago init --no-comments` or `spago init -C`
+to generate this file without the comments in this block.
+-}
+{ name = "my-project"
+, dependencies = [ "console", "effect", "prelude", "psci-support" ]
+, packages = ./packages.dhall
+, sources = [ "src/**/*.purs", "test/**/*.purs" ]
+}

existentials/src/Main.purs

@@ -0,0 +1,31 @@
+module Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Console (log)
+
+
+main :: Effect Unit
+main = log "hello world"
+
+---------- Existentials
+type ShowConstraint a = Show a => a
+
+type Exists :: forall k. (k -> Type) -> Type
+type Exists c = forall r. (forall a. c a -> r) -> r
+
+type Showable = Exists ShowConstraint
+
+mkShowable :: forall a. Show a => a -> Showable
+mkShowable inner continue = continue inner
+
+demo1 :: Showable
+demo1 = mkShowable 1
+
+demo2:: Showable
+demo2 = mkShowable "a"
+
+demo3:: Showable
+demo3 = mkShowable true
+

gadts/.gitignore

@@ -0,0 +1,10 @@
+/bower_components/
+/node_modules/
+/.pulp-cache/
+/output/
+/generated-docs/
+/.psc-package/
+/.psc*
+/.purs*
+/.psa*
+/.spago

gadts/packages.dhall

@@ -0,0 +1,104 @@
+{-
+Welcome to your new Dhall package-set!
+
+Below are instructions for how to edit this file for most use
+cases, so that you don't need to know Dhall to use it.
+
+## Use Cases
+
+Most will want to do one or both of these options:
+1. Override/Patch a package's dependency
+2. Add a package not already in the default package set
+
+This file will continue to work whether you use one or both options.
+Instructions for each option are explained below.
+
+### Overriding/Patching a package
+
+Purpose:
+- Change a package's dependency to a newer/older release than the
+    default package set's release
+- Use your own modified version of some dependency that may
+    include new API, changed API, removed API by
+    using your custom git repo of the library rather than
+    the package set's repo
+
+Syntax:
+where `entityName` is one of the following:
+- dependencies
+- repo
+- version
+-------------------------------
+let upstream = --
+in  upstream
+  with packageName.entityName = "new value"
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with halogen.version = "master"
+  with halogen.repo = "https://example.com/path/to/git/repo.git"
+
+  with halogen-vdom.version = "v4.0.0"
+  with halogen-vdom.dependencies = [ "extra-dependency" ] # halogen-vdom.dependencies
+-------------------------------
+
+### Additions
+
+Purpose:
+- Add packages that aren't already included in the default package set
+
+Syntax:
+where `<version>` is:
+- a tag (i.e. "v4.0.0")
+- a branch (i.e. "master")
+- commit hash (i.e. "701f3e44aafb1a6459281714858fadf2c4c2a977")
+-------------------------------
+let upstream = --
+in  upstream
+  with new-package-name =
+    { dependencies =
+       [ "dependency1"
+       , "dependency2"
+       ]
+    , repo =
+       "https://example.com/path/to/git/repo.git"
+    , version =
+        "<version>"
+    }
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with benchotron =
+      { dependencies =
+          [ "arrays"
+          , "exists"
+          , "profunctor"
+          , "strings"
+          , "quickcheck"
+          , "lcg"
+          , "transformers"
+          , "foldable-traversable"
+          , "exceptions"
+          , "node-fs"
+          , "node-buffer"
+          , "node-readline"
+          , "datetime"
+          , "now"
+          ]
+      , repo =
+          "https://github.com/hdgarrood/purescript-benchotron.git"
+      , version =
+          "v7.0.0"
+      }
+-------------------------------
+-}
+let upstream =
+      https://github.com/purescript/package-sets/releases/download/psc-0.14.1-20210516/packages.dhall sha256:f5e978371d4cdc4b916add9011021509c8d869f4c3f6d0d2694c0e03a85046c8
+
+in  upstream

gadts/spago.dhall

@@ -0,0 +1,18 @@
+{-
+Welcome to a Spago project!
+You can edit this file as you like.
+
+Need help? See the following resources:
+- Spago documentation: https://github.com/purescript/spago
+- Dhall language tour: https://docs.dhall-lang.org/tutorials/Language-Tour.html
+
+When creating a new Spago project, you can use
+`spago init --no-comments` or `spago init -C`
+to generate this file without the comments in this block.
+-}
+{ name = "my-project"
+, dependencies =
+  [ "console", "effect", "prelude", "psci-support", "run", "tuples" ]
+, packages = ./packages.dhall
+, sources = [ "src/**/*.purs", "test/**/*.purs" ]
+}

gadts/src/Ast.purs

@@ -0,0 +1,32 @@
+module Ast where
+
+import Prelude
+import Data.Tuple.Nested (type (/\), (/\))
+
+
+newtype OutputNumber :: forall k. Type -> k -> Type
+newtype OutputNumber number boolean = OutputNumber number
+
+newtype OutputBoolean :: forall k. k -> Type -> Type
+newtype OutputBoolean number boolean = OutputBoolean boolean
+
+data Ast output
+    = Number (output Number Void)
+    | Boolean (output Void Number)
+    | Add (output (Ast output /\ Ast output) Void)
+    | And (output Void (Ast output /\ Ast output))
+
+addition :: Ast OutputNumber
+addition = Add $ OutputNumber ((Number $ OutputNumber 0.0) /\ (Number $ OutputNumber 1.1))
+
+class ExtractFromOutput output where
+    extractLeft :: forall left. output left Void -> left
+    wrapLeft :: forall left right. left -> output left right
+
+
+interpret :: forall output. Semiring (output Number Boolean) => ExtractFromOutput output => Ast output -> output Number Boolean
+interpret (Add inner) = interpret left + interpret right
+    where
+    left /\ right = extractLeft inner
+interpret (Number n) = wrapLeft $ extractLeft n
+interpret a = interpret a

gadts/src/Main.purs

@@ -0,0 +1,10 @@
+module Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"

gadts/src/RunLift.purs

@@ -0,0 +1,89 @@
+module RunLift where
+
+import Prelude
+
+import Data.Tuple (Tuple)
+import Data.Tuple.Nested (type (/\), (/\))
+import Prim.Boolean (False, True)
+import Type.Equality (class TypeEquals)
+import Type.Proxy (Proxy(..))
+
+{-
+Get :: forall s a. (s -> a) -> State s a
+-}
+data State a
+    = Get (Int -> a)
+    | Set Int a
+
+
+{-
+
+Take each arg.
+Notice an "a"? Replace it with Unit
+
+(!s -> a) -> State !s a
+
+=>
+
+State !s !s
+
+
+
+-}
+
+class TypeEqualsBool left right res | left right -> res
+
+instance tebT :: TypeEqualsBool l l True
+else instance tebF :: TypeEqualsBool l r False
+
+class ReturnOf :: forall k1 k2. k1 -> k2 -> Constraint
+class ReturnOf f r | f -> r
+
+instance ro :: ReturnOf b c => ReturnOf (a -> b) c
+else instance ro' :: ReturnOf a a
+
+class LiftConstructor :: (Type -> Type) -> Type -> Type -> Type -> Constraint
+class LiftConstructor f from to arg | f from -> arg to 
+
+instance lc :: (ReturnOf from (f arg), LiftConstructorImpl from to arg, ReturnOf to (f arg)) => LiftConstructor f from to arg
+
+class LiftConstructorImpl :: Type -> Type -> Type -> Constraint
+class LiftConstructorImpl from to arg | from -> to 
+
+instance lc'' :: TypeEquals d d' => LiftConstructorImpl ((d -> d') -> result) result d'
+else instance lc' :: (LiftConstructorImpl from to arg) => LiftConstructorImpl (Unit -> from) to arg
+else instance lc''' :: (TypeEqualsBool f Unit isUnit ,LiftConstructorFunc isUnit (f -> from) to arg) => LiftConstructorImpl (f -> from) to arg
+
+class LiftConstructorFunc isUnit from to arg | isUnit from -> to
+
+instance lcf :: LiftConstructorImpl from to arg => LiftConstructorFunc False (ignore -> from) (ignore -> to) arg
+else instance lct :: LiftConstructorFunc True (ignore -> result) result Unit
+
+testReturn :: forall from f a. ReturnOf from (f a) => from -> Proxy f /\ Proxy a
+testReturn _ = Proxy /\ Proxy
+
+testLift :: forall f from to arg. LiftConstructor f from to arg => Proxy f -> from -> Proxy to /\ Proxy arg
+testLift _ _ = Proxy /\ Proxy
+
+get :: forall a. Tuple (Proxy State) (Proxy a) 
+get = testReturn Get
+
+b :: Proxy (State Int) /\ Proxy Int
+b = testLift _state Get
+
+c :: Proxy _ /\ Proxy _
+c = testLift _state Set
+
+_state :: Proxy State
+_state = Proxy
+
+
+-- class Basic f arg | f -> arg
+
+-- instance basic :: Basic ((arg -> arg) -> r) arg
+
+-- testBasic :: forall f arg. Basic f arg => f -> Proxy arg 
+-- testBasic _ = Proxy
+
+-- hmm :: Proxy _
+-- hmm = testBasic (\f -> f 0 :: Int)

gadts/test/Main.purs

@@ -0,0 +1,11 @@
+module Test.Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"
+  log "You should add some tests."

lune/.gitignore

@@ -0,0 +1,10 @@
+/bower_components/
+/node_modules/
+/.pulp-cache/
+/output/
+/generated-docs/
+/.psc-package/
+/.psc*
+/.purs*
+/.psa*
+/.spago

lune/packages.dhall

@@ -0,0 +1,110 @@
+{-
+Welcome to your new Dhall package-set!
+
+Below are instructions for how to edit this file for most use
+cases, so that you don't need to know Dhall to use it.
+
+## Warning: Don't Move This Top-Level Comment!
+
+Due to how `dhall format` currently works, this comment's
+instructions cannot appear near corresponding sections below
+because `dhall format` will delete the comment. However,
+it will not delete a top-level comment like this one.
+
+## Use Cases
+
+Most will want to do one or both of these options:
+1. Override/Patch a package's dependency
+2. Add a package not already in the default package set
+
+This file will continue to work whether you use one or both options.
+Instructions for each option are explained below.
+
+### Overriding/Patching a package
+
+Purpose:
+- Change a package's dependency to a newer/older release than the
+    default package set's release
+- Use your own modified version of some dependency that may
+    include new API, changed API, removed API by
+    using your custom git repo of the library rather than
+    the package set's repo
+
+Syntax:
+where `entityName` is one of the following:
+- dependencies
+- repo
+- version
+-------------------------------
+let upstream = --
+in  upstream
+  with packageName.entityName = "new value"
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with halogen.version = "master"
+  with halogen.repo = "https://example.com/path/to/git/repo.git"
+
+  with halogen-vdom.version = "v4.0.0"
+-------------------------------
+
+### Additions
+
+Purpose:
+- Add packages that aren't already included in the default package set
+
+Syntax:
+where `<version>` is:
+- a tag (i.e. "v4.0.0")
+- a branch (i.e. "master")
+- commit hash (i.e. "701f3e44aafb1a6459281714858fadf2c4c2a977")
+-------------------------------
+let upstream = --
+in  upstream
+  with new-package-name =
+    { dependencies =
+       [ "dependency1"
+       , "dependency2"
+       ]
+    , repo =
+       "https://example.com/path/to/git/repo.git"
+    , version =
+        "<version>"
+    }
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with benchotron =
+      { dependencies =
+          [ "arrays"
+          , "exists"
+          , "profunctor"
+          , "strings"
+          , "quickcheck"
+          , "lcg"
+          , "transformers"
+          , "foldable-traversable"
+          , "exceptions"
+          , "node-fs"
+          , "node-buffer"
+          , "node-readline"
+          , "datetime"
+          , "now"
+          ]
+      , repo =
+          "https://github.com/hdgarrood/purescript-benchotron.git"
+      , version =
+          "v7.0.0"
+      }
+-------------------------------
+-}
+let upstream =
+      https://github.com/purescript/package-sets/releases/download/psc-0.13.8-20210118/packages.dhall sha256:a59c5c93a68d5d066f3815a89f398bcf00e130a51cb185b2da29b20e2d8ae115
+
+in  upstream

lune/spago.dhall

@@ -0,0 +1,20 @@
+{-
+Welcome to a Spago project!
+You can edit this file as you like.
+-}
+{ name = "my-project"
+, dependencies =
+  [ "console"
+  , "effect"
+  , "either"
+  , "foreign"
+  , "functions"
+  , "psci-support"
+  , "tuples"
+  , "typelevel-prelude"
+  , "undefined"
+  , "unsafe-coerce"
+  ]
+, packages = ./packages.dhall
+, sources = [ "src/**/*.purs", "test/**/*.purs" ]
+}

lune/src/Handle.js

@@ -0,0 +1,52 @@
+function applyMany(length, f, args) {
+  if (length === 0) return f;
+  else if (length === 1) return f(args);
+
+  return applyMany(length - 1, f(args.value0), args.value1);
+}
+
+/**
+ * Collect an arbitrary number of arguments inside an array.
+ *
+ * @param { number } count The number of arguments to collect.
+ * @param { (arguments: any[]) => T } then Callback to give the argument array to.
+ */
+const collectArguments = (count, then) => {
+  if (count === 0) return then([]);
+
+  return (argument) =>
+    collectArguments(count - 1, (arguments) => [argument, ...arguments]);
+};
+
+exports.curryImpl = (mkTuple, length, f) => {
+  if (length <= 1) return f;
+
+  return collectArguments(length, (arguments) => {
+    const tuples = arguments.reduceRight(mkTuple);
+
+    return f(tuples);
+  });
+};
+
+exports.handleImpl = (matchLune, request, casePure, matchers, target) =>
+  matchLune(target, {
+    pure: casePure,
+    request: (length, key, parameters, continuation) => {
+      console.log(length);
+      if (Reflect.has(matchers, key)) {
+        return applyMany(length, matchers[key](continuation), parameters);
+      }
+
+      return request((f) =>
+        f(key)(parameters)((result) =>
+          handleImpl(
+            matchLune,
+            request,
+            casePure,
+            matchers,
+            continuation(result)
+          )
+        )
+      );
+    },
+  });

lune/src/Handle.purs

@@ -0,0 +1,268 @@
+module Handle where
+
+import Prelude
+
+import Data.Function.Uncurried (Fn2, Fn3, Fn4, mkFn2, runFn3, runFn4)
+import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol)
+import Data.Tuple (Tuple)
+import Data.Tuple.Nested (type (/\), (/\))
+import Foreign (Foreign, unsafeToForeign)
+import Lists (class MatchArrow, TCons, TNil, kind TList)
+import Partial.Unsafe (unsafeCrashWith)
+import Prim.Row as Row
+import Prim.RowList as RowList
+import Type.Data.Row (RProxy(..))
+
+-- | Abilities for testing
+type ReaderAbility e r = ( ask :: e | r ) 
+type StreamAbility v r = ( emit :: v -> Unit | r )
+type StoreAbility s r 
+  = ( get :: s
+    , put :: s -> Unit | r )
+
+-- | Transform a list of types into a chain of nested tuples.
+class TListToTuples (i :: TList) o | i -> o
+
+instance tlistTupleConsNil :: TListToTuples (TCons head TNil) head
+else instance tlistTupleCons 
+  :: TListToTuples tail outputTail 
+  => TListToTuples (TCons head tail) (head /\ outputTail)
+else instance tlistTupleBase :: TListToTuples TNil Unit
+
+-- | Transform a chain of nested tuples into a list of types
+class TuplesToTList i (o :: TList) | i -> o
+
+instance tupleToTListTuple 
+  :: TuplesToTList b tail
+  => TuplesToTList (a /\ b) (TCons a tail)
+else instance tupleToTListUnit :: TuplesToTList Unit TNil
+else instance tupleToTListGeneral :: TuplesToTList a (TCons a TNil)
+
+-- | Measure the lenght of some nested tuples
+class TupleLength t where
+  tupleLength :: Proxy t -> Int
+
+instance tupleLengthTuple :: TupleLength b => TupleLength (a /\ b) where
+  tupleLength _ = tupleLength (Proxy :: _ b) + 1
+
+else instance tupleLengthUnit :: TupleLength Unit where
+  tupleLength _ = 0
+
+else instance tupleLengthGeneral :: TupleLength a where
+  tupleLength _ = 1
+
+{-
+get :: s 
+put :: s -> ()
+
+...becomes
+get :: (s -> Lune abilities a) -> Lune remaining result
+put :: (unit -> Lune abilities a) -> state -> Lune remaining result
+-}
+class AbilityMatchers (all :: #Type) a result (abilities :: #Type) (matchers :: #Type) 
+  | all a result abilities -> matchers
+  , all a result matchers -> abilities
+
+instance abilityMatchersGeneral :: 
+  ( RowList.RowToList abilities abilities'
+  , AbilityMatchersRL (Lune all a) result abilities' matchers
+  ) => AbilityMatchers all a result abilities ( pure :: a -> result | matchers )
+
+-- | Internal version of abilityMatchers using rowlists
+class AbilityMatchersRL next result (rowList :: RowList.RowList) (output :: #Type) 
+  | next result rowList -> output
+  , next result output -> rowList
+
+instance abilityMatchersRLNil :: AbilityMatchersRL next result RowList.Nil ()
+else instance abilityMatchersRlCons :: 
+  ( AbilityMatchersRL continuationOutput result tail tail' 
+  , MatchArrow focus parameters continuationInput
+  , MatchArrow return parameters result
+  , Row.Cons key ((continuationInput -> continuationOutput) -> return) tail' matchers
+  ) => AbilityMatchersRL
+        continuationOutput 
+        result 
+        (RowList.Cons key focus tail) 
+        matchers
+
+-- | Type for lune requests
+type Request abilities a = (forall t.
+      (forall key focus subrow arguments return tuples. 
+        Row.Cons key focus subrow abilities =>
+        MatchArrow focus arguments return =>
+        TListToTuples arguments tuples => 
+        IsSymbol key =>
+        SProxy key ->
+        Int ->
+        tuples -> 
+        (return -> Lune abilities a) -> 
+        t
+      ) -> t)
+
+-- | The actual lune monad
+data Lune (abilities :: #Type) a 
+  = Pure a
+  | Request (Request abilities a)
+
+-- TODO: ffi this
+foreign import curryImpl :: 
+  forall tuples arguments return t. 
+  MatchArrow t arguments return => 
+  TListToTuples arguments tuples => 
+  Fn3 
+    (forall a b. a -> b -> Tuple a b)
+    Int
+    (tuples -> return) 
+    t
+
+curryGeneralized :: 
+  forall tuples arguments return t.
+  MatchArrow t arguments return => 
+  TListToTuples arguments tuples => 
+  TupleLength tuples =>
+  Proxy t ->
+  (tuples -> return) ->
+  t
+curryGeneralized _ = runFn3 curryImpl (/\) (tupleLength (Proxy :: _ tuples))
+
+request :: 
+  forall abilities key focus subrow output arguments return tuples.  
+  Row.Cons key focus subrow abilities => 
+  MatchArrow focus arguments return => 
+  TListToTuples arguments tuples => 
+  MatchArrow output arguments (Lune abilities return) =>
+  IsSymbol key =>
+  RProxy abilities -> 
+  SProxy key ->
+  output
+request r s = curryGeneralized (Proxy :: _ output) $ \t -> Request \f -> f s (tupleLength (Proxy :: _ tuples)) t Pure
+
+type MatchLune abilities a t = 
+  Fn2 
+    (Lune abilities a) 
+    { pure :: a -> t
+    -- TODO: this is not that well typed, maybe try and fix it
+    , request :: 
+        Fn4 Int String Foreign Foreign t
+    } t
+
+matchLune :: forall abilities a t. MatchLune abilities a t
+matchLune = mkFn2 \lune cases -> case lune of
+  Pure a -> cases.pure a
+  Request r -> r \sproxy argumentCount t a -> 
+    runFn4 cases.request 
+      argumentCount 
+      (reflectSymbol sproxy) 
+      (unsafeToForeign t) 
+      (unsafeToForeign a)
+
+foreign import handleImpl :: 
+  forall abilities subrow remaining result a matchers.
+  Row.Union subrow remaining abilities =>
+  AbilityMatchers abilities a (Lune remaining result) subrow matchers =>
+  Fn4 
+    (MatchLune abilities a (Lune abilities result)) 
+    (forall x y. Request x y -> Lune x y) 
+    (Record matchers) 
+    (Lune abilities a) 
+    (Lune remaining result)
+
+-- | Remove some effects.
+handleWith :: 
+  forall abilities subrow remaining result a matchers.
+  Row.Union subrow remaining abilities =>
+  AbilityMatchers abilities a (Lune remaining result) subrow matchers =>
+  RProxy subrow ->
+  Record matchers ->
+  Lune abilities a -> 
+  Lune remaining result
+handleWith _ matchers monad
+  = runFn4 handleImpl 
+      matchLune 
+      Request 
+      matchers
+      monad
+
+
+-- | Why is this not a thing already?
+data Proxy t = Proxy
+
+-- Tests
+getState :: forall a. Lune (StoreAbility a ()) a
+getState = request _store _get
+  where
+  _store :: RProxy (StoreAbility a ())
+  _store = RProxy
+
+  _get :: SProxy "get"
+  _get = SProxy
+
+putState :: forall a. a -> Lune (StoreAbility a ()) Unit
+putState s = request _store _put s
+  where
+  _store :: RProxy (StoreAbility a ())
+  _store = RProxy
+
+  _put :: SProxy "put"
+  _put = SProxy
+ 
+-- Typeclass instances for Lune.
+instance functorLune :: Functor (Lune abilities) where
+  map f = case _ of
+    Pure a -> Pure (f a)
+    Request existential -> 
+      Request \runExistential -> 
+        existential \key paramCount parameters continuation -> 
+          runExistential key paramCount parameters (continuation >>> map f)
+
+instance applyLune :: Apply (Lune abilities) where
+  apply = ap
+
+instance applicativeLune :: Applicative (Lune abilities) where
+  pure = Pure
+
+instance bindLune :: Bind (Lune abilities) where
+  bind m f = case m of
+    Pure a -> f a
+    Request existential -> 
+      Request \runExistential -> 
+        existential \key paramCount parameters continuation ->
+          runExistential key paramCount parameters (continuation >=> f)
+
+instance monadLune :: Monad (Lune abilities)
+
+-- | Extract the value from an empty lune monad.
+extract :: forall a. Lune () a -> a
+extract = case _ of
+  Pure a -> a
+  -- | This should never run
+  Request _ -> unsafeCrashWith "Cannot extract values from requests"
+
+-- | Simple program for testing
+myProgram :: Lune (StoreAbility Int ()) String
+myProgram = do
+  state <- getState
+  putState (state + 3)
+  pure $ show $ state * 2
+
+-- | Handler for stores
+runStore :: forall state a r. state -> Lune (StoreAbility state r) a -> Lune r (state /\ a)
+runStore initialState = handleWith _on (handler initialState)
+  where
+  handler state = 
+    { get: \continue -> handleWith _on (handler state) (continue state)
+    , put: \continue newState -> handleWith _on (handler newState) (continue unit)
+    , pure: \a -> pure (state /\ a)
+    }
+
+  _on :: RProxy (StoreAbility state ())
+  _on = RProxy
+
+abilityMatchers :: 
+  forall all a result abilities matchers. 
+  AbilityMatchers all a result abilities matchers =>
+  Proxy (Lune all a) ->
+  Proxy result ->
+  RProxy abilities ->
+  RProxy matchers
+abilityMatchers _ _ _ = RProxy

lune/src/Lists.purs

@@ -0,0 +1,42 @@
+module Lists where
+
+
+foreign import kind TList
+foreign import data TNil :: TList
+foreign import data TCons :: Type -> TList -> TList
+
+data TLProxy (tlist :: TList) = TLProxy
+
+
+foreign import kind RList
+foreign import data RNil :: RList
+foreign import data RCons :: #Type -> RList -> RList
+
+data RLProxy (tlist :: RList) = RLProxy
+
+infixr 6 type RCons as :
+
+-- | Check if a rlist contains a row
+class InList (t :: #Type) (list :: RList)
+
+instance inListFirst :: InList t (t : rest)
+else instance inListLater :: InList t tail => InList t (head : tail)
+
+-- | Remove an element from a list
+class Without (t :: #Type) (list :: RList) (remaining :: RList) | t list -> remaining
+
+instance withoutNil :: Without a RNil RNil
+else instance withoutHead :: Without a (RCons a tail) tail
+else instance withoutCons :: Without a tail remaining => Without a (RCons head tail) (RCons head remaining)
+
+-- | Break up function into it's components
+class MatchArrow t (arguments :: TList) return 
+  | t -> arguments return
+  , arguments return -> t
+  , arguments t -> return 
+
+instance matchArrowRec 
+  :: MatchArrow to arguments return 
+  => MatchArrow (from -> to) (TCons from arguments) return
+
+else instance matchArrowGeneral :: MatchArrow t TNil t

lune/src/Main.purs

@@ -0,0 +1,9 @@
+module Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Console (log)
+
+main :: Effect Unit
+main = log "hello world"  

lune/test/Main.purs

@@ -0,0 +1,11 @@
+module Test.Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"
+  log "You should add some tests."

maps/.gitignore

@@ -0,0 +1,10 @@
+/bower_components/
+/node_modules/
+/.pulp-cache/
+/output/
+/generated-docs/
+/.psc-package/
+/.psc*
+/.purs*
+/.psa*
+/.spago

maps/packages.dhall

@@ -0,0 +1,18 @@
+let upstream =
+      https://github.com/purescript/package-sets/releases/download/psc-0.14.0-20210409/packages.dhall sha256:e81c2f2ce790c0e0d79869d22f7a37d16caeb5bd81cfda71d46c58f6199fd33f
+
+let additions =
+      { typelevel-lists =
+        { dependencies =
+          [ "prelude"
+          , "tuples"
+          , "typelevel-peano"
+          , "typelevel-prelude"
+          , "unsafe-coerce"
+          ]
+        , repo = "https://github.com/PureFunctor/purescript-typelevel-lists/"
+        , version = "main"
+        }
+      }
+
+in  upstream // additions

maps/spago.dhall

@@ -0,0 +1,15 @@
+{-
+Welcome to a Spago project!
+You can edit this file as you like.
+-}
+{ name = "my-project"
+, dependencies =
+  [ "console"
+  , "effect"
+  , "ordered-collections"
+  , "psci-support"
+  , "typelevel-lists"
+  ]
+, packages = ./packages.dhall
+, sources = [ "src/**/*.purs", "test/**/*.purs" ]
+}

maps/src/Composable.purs

@@ -0,0 +1,26 @@
+module Composable where
+
+import Prelude
+
+class Transform a b where
+    from :: a -> b
+
+instance tbi :: Transform Boolean Int where
+    from true = 1
+    from false = 0
+
+else instance tis :: Transform Int String where
+    from = show
+
+else instance ti :: Transform i i where
+    from = identity
+
+else instance tc :: (Transform a b, Transform b c) => Transform a c where
+    from = (from :: a -> b) >>> from
+
+{- This doensn't work:
+
+a :: String
+a = from true
+
+ -}

maps/src/Main.purs

@@ -0,0 +1,10 @@
+module Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"

maps/src/Map.purs

@@ -0,0 +1,38 @@
+module Oof where
+
+import Prelude
+
+import Data.Map (Map)
+import Data.Map as Map
+import Data.Maybe (fromJust)
+import Data.Tuple.Nested (type (/\), (/\))
+import Partial.Unsafe (unsafePartial)
+import Prim.Row (class Cons)
+import Safe.Coerce (coerce)
+
+data MapId
+
+newtype SafeMap :: Row MapId -> Type -> Type -> Type
+newtype SafeMap t k v = SafeMap (Map k v)
+
+newtype Key :: MapId -> Type -> Type
+newtype Key t a = Key a
+
+type AddKey :: forall k1. k1 -> Row k1 -> Row k1
+type AddKey k r = ( includes :: k | r )
+
+lookup :: forall t ts ts' k v. Cons "includes" t ts ts' => Ord k => Key t k -> SafeMap ts' k v -> v 
+lookup (Key k) (SafeMap m) = unsafePartial $ fromJust $ Map.lookup k m
+
+insert :: forall ts k v r. Ord k => k -> v -> SafeMap ts k v -> (forall t. Key t k /\ SafeMap (AddKey t ts) k v -> r) -> r  
+insert k v m next = next $ Key k /\ coerce (Map.insert k v $ coerce m)
+
+empty :: forall k v. SafeMap () k v
+empty = SafeMap Map.empty
+
+test :: String
+test = 
+    insert 0 "first" empty \(first /\ dict) -> 
+        insert 1 "second" dict \(second /\ dict') ->
+            insert 2 "third" dict' \(third /\ dict'') -> 
+                lookup first dict'

maps/test/Main.purs

@@ -0,0 +1,11 @@
+module Test.Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"
+  log "You should add some tests."

proofs/.gitignore

@@ -0,0 +1,10 @@
+/bower_components/
+/node_modules/
+/.pulp-cache/
+/output/
+/generated-docs/
+/.psc-package/
+/.psc*
+/.purs*
+/.psa*
+/.spago

proofs/packages.dhall

@@ -0,0 +1,4 @@
+let upstream =
+      https://github.com/purescript/package-sets/releases/download/psc-0.14.0-20210409/packages.dhall sha256:e81c2f2ce790c0e0d79869d22f7a37d16caeb5bd81cfda71d46c58f6199fd33f
+
+in  upstream

proofs/spago.dhall

@@ -0,0 +1,9 @@
+{-
+Welcome to a Spago project!
+You can edit this file as you like.
+-}
+{ name = "my-project"
+, dependencies = [ "console", "effect", "psci-support", "undefined" ]
+, packages = ./packages.dhall
+, sources = [ "src/**/*.purs", "test/**/*.purs" ]
+}

proofs/src/Main.purs

@@ -0,0 +1,11 @@
+module Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Console (logShow)
+import Naturals (reflectNat, two)
+
+main :: Effect Unit
+main = do
+  logShow $ reflectNat two

proofs/src/Nats.purs

@@ -0,0 +1,117 @@
+module Naturals where
+
+import Prelude
+
+import Type.Proxy (Proxy(..))
+
+class IsNatural :: Natural -> Constraint
+class IsNatural a where
+    match :: Proxy a 
+        -> forall r. (forall inner. IsNatural inner => Proxy inner -> r) 
+        -> (forall zero. IsNatural zero => Proxy zero -> r) 
+        -> r
+
+foreign import data Natural :: Type
+foreign import data Succ :: forall k. k -> Natural
+foreign import data Zero :: Natural
+
+instance isNaturalZero :: IsNatural Zero where
+    match _ caseSucc caseZero = caseZero (Proxy :: Proxy Zero)
+
+instance isNaturalSucc :: IsNatural a => IsNatural (Succ a) where
+    match _ caseSucc caseZero = caseSucc (Proxy :: Proxy a)
+
+foreign import data Add :: forall k. k -> k -> Natural
+
+instance isNaturalAdd :: (IsNatural a, IsNatural b) => IsNatural (Add a b) where
+    match _ caseSucc caseZero = match (Proxy :: _ a)     
+        handleFirstSucc
+        handleFirstZero
+        where
+        handleFirstZero _ = match (Proxy :: _ b) caseSucc caseZero
+    
+        handleFirstSucc :: forall previous. IsNatural previous => Proxy previous -> _
+        handleFirstSucc _ = match (Proxy :: _ (Succ (Add previous b))) caseSucc caseZero
+
+reflectNat :: forall n. IsNatural n => Proxy n -> Int
+reflectNat p = match p (\inner -> 1 + reflectNat inner) (const 0)
+
+{-
+--------- Equality
+foreign import data Equality :: forall k. k -> k -> Type
+foreign import data Refl :: forall a. Equality a a
+
+unsafeRefl :: forall a b. Equality a b
+unsafeRefl = undefined
+
+mapEquality :: forall a b f. Proxy f -> Equality a b -> Equality (f a) (f b)
+mapEquality _ _ = unsafeRefl
+
+zeroPlusAIsA :: forall a. Proxy a -> Equality (Add Zero a) a
+zeroPlusAIsA _ = unsafeRefl 
+
+succRule :: forall a b. Equality (Add (Succ a) b) (Succ (Add a b))
+succRule = unsafeRefl
+
+aPlusZeroIsA :: forall a. IsNatural a => Proxy a -> Equality (Add a Zero) a 
+aPlusZeroIsA p = match p 
+    caseSucc
+    caseZero
+    where
+    caseZero p = zeroPlusAIsA p 
+    caseSucc inner = mapEquality (Proxy :: _ Succ) (aPlusZeroIsA inner)
+
+type ZeroIsZero :: Equality Zero Zero
+type ZeroIsZero = Refl
+
+data Natural id
+    = Zero (TZero ~ id)
+    | Succ (forall r. (forall inner. Natural inner -> (Succ inner ~ id) -> r) -> r)
+
+zeroPlusAIsA :: forall id. Proxy id -> Equality id (Add Zero id)
+zeroPlusAIsA = ...
+
+succEquality :: forall a b. Proxy a -> Proxy b -> Equality (Succ (Add a b)) (Add (Succ a) b)
+succEquality = ...
+
+aPlusZeroIsA :: forall r id. Natural id -> Equality id (Add id Zero)
+aPlusZeroIsA (Zero proof) 
+    = zeroPlusAIsA @Zero -- Equality Zero (Add Zero Zero)
+    |> rewriteLeft proof -- Equality id (Add Zero Zero)
+    |> rewriteRight 
+        (additionEquality proof identity) -- Equlity (Add id Zero) (Add Zero Zero)
+            -- Equality id (Add id Zero)
+    
+aPlusZeroIsA (Succ existential) = existential handleExistential
+    where
+    handleExistential :: forall inner. Natural inner -> (Succ inner ~ id) -> Equality id (Add id Zero)
+    handleExistential inner proof
+        = aPlusZeroIsA inner -- Equality inner (Add inner Zero)
+        |> rewriteWithContext (Proxy :: _ Succ) -- Equality (Succ inner) (Succ (Add inner Zero))
+        |> rewriteLeft proof -- Equality id (Succ (Add inner Zero))
+        |> rewriteRight 
+            (succEquality @inner @Zero) -- Equality (Succ (Add inner Zero)) (Add (Succ inner) Zero)
+                -- Equality id (Add (Succ inner) Zero)
+        |> rewriteRight 
+            (additionEquality proof identity) -- Equality (Add (Succ inner) Zero) (Add id Zero)
+                -- Equality id (Add id Zero)
+
+
+-}
+
+---------- Helpers
+type One = Succ Zero
+type Two = Succ One
+type Three = Succ Two
+
+one :: Proxy One 
+one = Proxy 
+
+two :: Proxy Two
+two = Proxy 
+
+three :: Proxy Three
+three = Proxy 
+
+add :: forall a b. Proxy a -> Proxy b -> Proxy (Add a b)
+add _ _ = Proxy

proofs/src/ValueLevelNaturals.purs

@@ -0,0 +1,5 @@
+module ValueLevelNaturals where
+
+data Natural 
+    = Succ Natural
+    | Zero

proofs/test/Main.purs

@@ -0,0 +1,11 @@
+module Test.Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"
+  log "You should add some tests."

sprint/.gitignore

@@ -0,0 +1,10 @@
+/bower_components/
+/node_modules/
+/.pulp-cache/
+/output/
+/generated-docs/
+/.psc-package/
+/.psc*
+/.purs*
+/.psa*
+/.spago

sprint/packages.dhall

@@ -0,0 +1,18 @@
+let upstream =
+      https://github.com/purescript/package-sets/releases/download/psc-0.14.0-20210409/packages.dhall sha256:e81c2f2ce790c0e0d79869d22f7a37d16caeb5bd81cfda71d46c58f6199fd33f
+
+let additions =
+      { typelevel-lists =
+        { dependencies =
+          [ "prelude"
+          , "tuples"
+          , "typelevel-peano"
+          , "typelevel-prelude"
+          , "unsafe-coerce"
+          ]
+        , repo = "https://github.com/PureFunctor/purescript-typelevel-lists/"
+        , version = "main"
+        }
+      }
+
+in  upstream // additions

sprint/spago.dhall

@@ -0,0 +1,10 @@
+{-
+Welcome to a Spago project!
+You can edit this file as you like.
+-}
+{ name = "my-project"
+, dependencies =
+  [ "console", "effect", "psci-support", "typelevel-lists", "undefined" ]
+, packages = ./packages.dhall
+, sources = [ "src/**/*.purs", "test/**/*.purs" ]
+}

sprint/src/Main.purs

@@ -0,0 +1,15 @@
+module Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class.Console (logShow)
+import Sprint (Sprint(..), State(..), evalState, extract)
+import Type.Data.List (type (:>), Nil')
+
+myProgram :: Sprint (State Int :> Nil') Int
+myProgram = Bind \f -> f "State" $ Put 2 \_ -> Bind \f' -> f' "State" $ Get \s -> Pure s
+
+main :: Effect Unit
+main = do
+  logShow $ extract $ evalState 0 myProgram

sprint/src/Sprint.purs

@@ -0,0 +1,49 @@
+module Sprint where
+
+import Prelude
+
+import Partial.Unsafe (unsafeCrashWith)
+import Type.Data.List (type (:>), List', Nil')
+import Unsafe.Coerce (unsafeCoerce)
+
+data State s a
+    = Get (s -> a)
+    | Put s (Unit -> a)
+
+type Ability = Type -> Type
+
+data Sprint :: List' Ability -> Type -> Type
+data Sprint effects a 
+    = Pure a
+    | Bind (forall t. (forall eff. Functor eff => String -> WithContinuation eff effects a -> t) -> t)
+
+type WithContinuation :: Ability -> List' Ability -> Type -> Type
+type WithContinuation eff effects a = eff (Sprint effects a)
+
+flat :: forall a effects. Sprint effects (Sprint effects a) -> Sprint effects a
+flat = case _ of
+    Pure m -> m
+    Bind f -> f \n eff -> Bind \cont -> cont n $ map flat eff
+
+handle :: forall rest eff a t. String -> Sprint (eff :> rest) a -> (a -> t) -> (WithContinuation eff (eff :> rest) a -> t) -> Sprint rest t
+handle name m casePure caseBind = case m of
+    Pure a -> Pure $ casePure a
+    Bind f -> f go 
+        where 
+        go ::  forall eff'. Functor eff' => String -> WithContinuation eff' (eff :> rest) a -> Sprint rest t
+        go name' eff = case name == name' of
+            false -> Bind \f' -> f' name' $ map (\m' -> handle name m' casePure caseBind) eff
+            true -> Pure $ caseBind (unsafeCoerce eff)
+
+evalState :: forall rest s a. s -> Sprint (State s :> rest) a -> Sprint rest a
+evalState s m = flat $ handle "State" m Pure case _ of
+    Put s' continue -> evalState s' $ continue unit 
+    Get continue -> evalState s $ continue s
+
+extract :: forall a. Sprint Nil' a -> a
+extract = case _ of
+    Pure a -> a
+    _ -> unsafeCrashWith "can't extract :("
+
+---------- Typeclass instances
+derive instance functorState :: Functor (State s)

sprint/test/Main.purs

@@ -0,0 +1,11 @@
+module Test.Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"
+  log "You should add some tests."

streams/.gitignore

@@ -0,0 +1,10 @@
+/bower_components/
+/node_modules/
+/.pulp-cache/
+/output/
+/generated-docs/
+/.psc-package/
+/.psc*
+/.purs*
+/.psa*
+/.spago

streams/packages.dhall

@@ -0,0 +1,104 @@
+{-
+Welcome to your new Dhall package-set!
+
+Below are instructions for how to edit this file for most use
+cases, so that you don't need to know Dhall to use it.
+
+## Use Cases
+
+Most will want to do one or both of these options:
+1. Override/Patch a package's dependency
+2. Add a package not already in the default package set
+
+This file will continue to work whether you use one or both options.
+Instructions for each option are explained below.
+
+### Overriding/Patching a package
+
+Purpose:
+- Change a package's dependency to a newer/older release than the
+    default package set's release
+- Use your own modified version of some dependency that may
+    include new API, changed API, removed API by
+    using your custom git repo of the library rather than
+    the package set's repo
+
+Syntax:
+where `entityName` is one of the following:
+- dependencies
+- repo
+- version
+-------------------------------
+let upstream = --
+in  upstream
+  with packageName.entityName = "new value"
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with halogen.version = "master"
+  with halogen.repo = "https://example.com/path/to/git/repo.git"
+
+  with halogen-vdom.version = "v4.0.0"
+  with halogen-vdom.dependencies = [ "extra-dependency" ] # halogen-vdom.dependencies
+-------------------------------
+
+### Additions
+
+Purpose:
+- Add packages that aren't already included in the default package set
+
+Syntax:
+where `<version>` is:
+- a tag (i.e. "v4.0.0")
+- a branch (i.e. "master")
+- commit hash (i.e. "701f3e44aafb1a6459281714858fadf2c4c2a977")
+-------------------------------
+let upstream = --
+in  upstream
+  with new-package-name =
+    { dependencies =
+       [ "dependency1"
+       , "dependency2"
+       ]
+    , repo =
+       "https://example.com/path/to/git/repo.git"
+    , version =
+        "<version>"
+    }
+-------------------------------
+
+Example:
+-------------------------------
+let upstream = --
+in  upstream
+  with benchotron =
+      { dependencies =
+          [ "arrays"
+          , "exists"
+          , "profunctor"
+          , "strings"
+          , "quickcheck"
+          , "lcg"
+          , "transformers"
+          , "foldable-traversable"
+          , "exceptions"
+          , "node-fs"
+          , "node-buffer"
+          , "node-readline"
+          , "datetime"
+          , "now"
+          ]
+      , repo =
+          "https://github.com/hdgarrood/purescript-benchotron.git"
+      , version =
+          "v7.0.0"
+      }
+-------------------------------
+-}
+let upstream =
+      https://github.com/purescript/package-sets/releases/download/psc-0.14.1-20210613/packages.dhall sha256:5f10380b3ca7d3a32ea5c2b7535e4814a5e3f3590c70692f76e596d6ab0687b3
+
+in  upstream

streams/spago.dhall

@@ -0,0 +1,18 @@
+{-
+Welcome to a Spago project!
+You can edit this file as you like.
+
+Need help? See the following resources:
+- Spago documentation: https://github.com/purescript/spago
+- Dhall language tour: https://docs.dhall-lang.org/tutorials/Language-Tour.html
+
+When creating a new Spago project, you can use
+`spago init --no-comments` or `spago init -C`
+to generate this file without the comments in this block.
+-}
+{ name = "my-project"
+, dependencies =
+  [ "console", "effect", "pipes", "prelude", "psci-support", "tuples" ]
+, packages = ./packages.dhall
+, sources = [ "src/**/*.purs", "test/**/*.purs" ]
+}

streams/src/Main.purs

@@ -0,0 +1,38 @@
+module Main where
+
+import Prelude
+
+import Data.Tuple (Tuple(..))
+import Effect (Effect)
+import Effect.Class (class MonadEffect)
+import Effect.Class.Console (logShow)
+import Pipes (await, for, yield, (>->))
+import Pipes.Core (Consumer_, Producer_, runEffect)
+import Pipes.Prelude (take)
+import Pipes.Prelude as Pipes
+
+naturals :: forall m. Monad m => Producer_ Int m Unit
+naturals = go 0
+  where
+  go n = do
+    yield n
+    go (n + 1)
+
+logAll :: forall a m. MonadEffect m => Show a => Consumer_ a m Unit
+logAll = do
+  showable <- await
+  logShow showable
+  logAll
+
+nNaturals :: forall m. Monad m => Int -> Producer_ Int m Unit
+nNaturals n = naturals >-> take n
+
+merger :: forall m. Monad m => Producer_ (Tuple Int Int) m Unit
+merger = 
+  for (nNaturals 3) \a ->
+    for (nNaturals 3 >-> Pipes.map ((+) 4)) \b ->
+      yield $ Tuple a b
+
+
+main :: Effect Unit
+main = runEffect ((nNaturals 3 <> nNaturals 3) >-> logAll)

streams/test/Main.purs

@@ -0,0 +1,11 @@
+module Test.Main where
+
+import Prelude
+
+import Effect (Effect)
+import Effect.Class.Console (log)
+
+main :: Effect Unit
+main = do
+  log "🍝"
+  log "You should add some tests."