LSLeary · February 18, 2025 22:19 · Feb 18, 2025 · Feb 18, 2025 · Feb 18, 2025
diff --git a/LambdaEncodings.md b/LambdaEncodings.md
@@ -55,7 +55,7 @@ Somewhat miraculously, absent any actual recursion, we can also define the least
 
 ```haskell
 -- AKA Mu
-newtype LFP f = LFP (forall r. (f r -> r) -> r)
+newtype LFP f = LFP{ fold :: forall r. (f r -> r) -> r }
 
 type ChurchList a
     = LFP (ListF a)
@@ -73,5 +73,5 @@ There's another (miraculously non-recursive) fixpoint operator, but it's not rea
 
 ```haskell
 -- AKA Nu
-data GFP f = forall s. GFP (s -> f s) s
+data GFP f = forall s. GFP{ grow :: s -> f s, seed :: s }
 ```
diff --git a/LambdaEncodings.md b/LambdaEncodings.md
@@ -55,7 +55,7 @@ Somewhat miraculously, absent any actual recursion, we can also define the least
 
 ```haskell
 -- AKA Mu
-newtype LFP f = LFP (forall r. f r -> r)
+newtype LFP f = LFP (forall r. (f r -> r) -> r)
 
 type ChurchList a
     = LFP (ListF a)

diff --git a/LambdaEncodings.md b/LambdaEncodings.md
@@ -0,0 +1,77 @@
+# Scott & Church Encodings
+
+## Algebraic Data Types
+
+It suffices to describe sums, products and their identities to obtain the full wealth of ADTs:
+
+```haskell
+newtype a + b = Sum{ matchSum :: forall r. (a -> r) -> (b -> r) -> r) }
+
+left :: a -> a + b
+left x = Sum \l _ -> l x
+
+right :: b -> a + b
+right y = Sum \_ r -> r y
+
+newtype Void = Void{ absurd :: forall r. r }
+
+newtype a * b = Product{ matchPair :: forall r. (a -> b -> r) -> r }
+
+pair :: a -> b -> a * b
+pair x y = Product \f -> f x y
+
+newtype Unit = Unit (forall r. r -> r)
+
+unit :: Unit
+unit = Unit \r -> r
+```
+
+## Recursive Data Types
+
+Recursion is where it gets a bit more interesting.
+Luckily, we can factor this consideration out: write a base functor with the above, E.g.
+
+```haskell
+newtype ListF a s = ListF (Unit + a * s)
+```
+
+Then transform it with a suitable fixpoint operator.
+Using Haskell's direct type-level recursion, we obtain `Fix`, corresponding to the Scott encoding.
+
+```haskell
+newtype Fix f = In{ out :: f (Fix f) }
+
+type ScottList a
+    = Fix (ListF a)
+--  ~ ListF a (ScottList a)
+--  ~ Unit + a * ScottList a
+--  ~ forall r. (Unit -> r) -> (a * ScottList a -> r) -> r
+--  ~ forall r. r -> (a -> ScottList a -> r) -> r
+```
+
+The resulting "destructor" corresponds to shallow pattern matching.
+
+Somewhat miraculously, absent any actual recursion, we can also define the least fixed-point operator, corresponding to the Church (or Boehm-Berarducci) encoding.
+
+```haskell
+-- AKA Mu
+newtype LFP f = LFP (forall r. f r -> r)
+
+type ChurchList a
+    = LFP (ListF a)
+--  ~ forall r. (ListF a r -> r) -> r
+--  ~ forall r. ((Unit + a * r) -> r) -> r
+--  ~ forall r. (Unit -> r) -> (a * r -> r) -> r
+--  ~ forall r. r -> (a -> r -> r) -> r
+```
+
+The type of the resulting "destructor" might just be familiar.
+Indeed, it should be—it corresponds to `foldr`, or a catamorphism in general.
+The fact that `foldr` (rearranged a little) transforms lists into into this (more fusile) alternative representation is what underpins `foldr/build` fusion.
+
+There's another (miraculously non-recursive) fixpoint operator, but it's not really used in this context.
+
+```haskell
+-- AKA Nu
+data GFP f = forall s. GFP (s -> f s) s
+```