Skip to content

Instantly share code, notes, and snippets.

@LSLeary
Last active February 18, 2025 22:19
Show Gist options
  • Save LSLeary/c25f39dff9ebcc726ba2ef1c7efbddb2 to your computer and use it in GitHub Desktop.
Save LSLeary/c25f39dff9ebcc726ba2ef1c7efbddb2 to your computer and use it in GitHub Desktop.
Scott & Church Encodings

Scott & Church Encodings

Algebraic Data Types

It suffices to describe sums, products and their identities to obtain the full wealth of ADTs:

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.

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.

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.

-- AKA Mu
newtype LFP f = LFP{ fold :: forall r. (f r -> 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.

-- AKA Nu
data GFP f = forall s. GFP{ grow :: s -> f s, seed :: s }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment