This website is out of date, please refer to the site on github.

# Church Representations

Posted on March 6, 2014

A project I’ve been playing with lately is generalizing `maybe`. Now on the surface that sounds well.. boring. But there’s actually some interesting concepts buried in here.

## Lambda The Almighty

Let’s start by specifying what I mean when I say “generalize”. When we look at `maybe`, the type gives us a pretty strong clue on how to implement it

``````    maybe :: b -> (a -> b) -> Maybe a -> b
maybe nothingCase justCase Nothing  = nothingCase
maybe nothingCase justCase (Just a) = justCase a``````

Each argument of corresponds to a different case of the sum type `Maybe`.

There’s actually a name for this idea, it’s encoding a data type within functions: Church Encoding.

Let’s rattle of some examples:

Tuples

``````    {-# LANGUAGE RankNTypes #-}
-- We'll call a tuple a Product because it
-- looks like the cartesion *product* of two types
type Product a b = forall c. (a -> b -> c) -> c
pair :: a -> b -> Product a b
pair a b = \destruct -> destruct a b

-- We can easily make fst and snd
fst :: Product a b -> a
fst p = p \$ \a b -> a
snd :: Product a b -> b
snd p = p \$ \a b -> b``````

We can do `Either` as well

``````    -- We'll call Either a "sum" because it
-- looks like the disjoint union (sum) of two types
type Sum a b = forall c. (a -> c) -> (b -> c) -> c
inl :: a -> Sum a b
inl a = \l r -> l a

inr :: b -> Sum a b
inr b = \l r -> r b``````

Look familiar? That’s just `Data.Either.either`! Now if we squint at these we can imagine building up more complex types from these building blocks

``````    data AFew = NoVal | OneVal Int | ThrVal Int Bool String

type ChurchAFew =
Sum () (Sum Int (Prod Int (Prod Bool String)))

noVal :: ChurchAFew
noVal = inl ()

oneVal :: Int -> ChurchAFew
oneVal i = inr (inl i)

thrVal :: Int -> Bool -> String -> ChurchAFew
thrVal i b s = inr . inr . pair i \$ pair b s``````

And now pattern matching more or less falls out for free from `ChurchAFew`. Since it’s a function we transform

``````    case foo of
NoVal        -> ...
OneVal i     -> ...
ThrVal i b s -> ...
-- becomes
foo (\() -> ...) (\p -> p (\i -> ...) (\p1 -> p1 (\i p2 -> ...)))``````

Such is the power of lambda! And there are all sorts of fun side effects of pattern matching being a function, most of it to do with nicer composition with point-free functions.

## But It’s Boring!

There’s a drawback here, boilerplate! We have to essentially duplicate all our data declarations, extra boilerplate for generating accessors, and then two functions to map back and forth between our representations.

As a programmer I’m far too lazy to write all that!

Whenever we start to think of terms of sum and product types it’s time to turn to GHC.Generics. It’s a library that provides a type class to reify our normal types into explicit sums and products and back again.

The first thing we have to do is write a type level function to reify a GHC.Generics representation to the appropriate type.

For example `Maybe Int` has the following representation

``````    M1
D
GHC.Generics.D1Maybe
(M1 C GHC.Generics.C1_0Maybe U1
:+: M1 C GHC.Generics.C1_1Maybe (M1 S NoSelector (K1 R Int)))``````

We can strip out all the `M1` meta information since we don’t really care leaving

``    U1 :+: K1 R Int``

Not so bad! Let’s start by writing a type level function (type family) to get rid the `M1` constructors

``````    {-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances, RankNTypes #-}

import GHC.Generics

-- | Remove the extra `p` parameter that GHC.Generics
-- lugs through every constructor
type family WithoutParam v :: * -> *
type instance WithoutParam ((:+:) l r p) = l :+: r
type instance WithoutParam ((:*:) l r p) = l :*: r
type instance WithoutParam (U1 p)        = U1
type instance WithoutParam (K1 a t p)    = K1 a t

-- | Strip out `M1` tags
type family StripMeta v :: *
type instance StripMeta (M1 a b f p)  = StripMeta (f p)
type instance StripMeta (K1 a t p)    = K1 a t p
type instance StripMeta ((:+:) l r p) =
(:+:) (WithoutParam (StripMeta (l p))) (WithoutParam (StripMeta (r p))) p
type instance StripMeta ((:*:) l r p) =
(:*:) (WithoutParam (StripMeta (l p))) (WithoutParam (StripMeta (r p))) p
type instance StripMeta (U1 p)        = U1 p``````

As we can see these type families are well.. pretty terrible. But they work! Next we can actually do some real work. We need to take a product type with one or more members and turn it into a function.

``````    type family ChurchProd v c :: *
type instance ChurchProd (K1 a t p) c    = t -> c
type instance ChurchProd (U1 p)     c    = () -> c
type instance ChurchProd ((:*:) l r p) c =
ChurchProd (l p) (ChurchProd (r p) c)``````

So here we have a type family with two parameters, the term and the “out” type. These take `a :*: b :*: c` to `a -> b -> c -> ...`. This is important because GHC.Generics represents things like a list where the `(:)` equivalent is `:+:` and the each leaf is product or unit type.

Now at least we can run

``````> :kind! ChurchProd (StripMeta (Rep (Int, Bool) ())) Char
ChurchProd (StripMeta (Rep (Int, Bool) ())) Char :: *
= Int -> Bool -> Char``````

As it happens, I told a small fib, GHC.Generics doesn’t make quite a list. In fact it makes a tree! We can rejigger things to a list though

``````    data ListTerm p -- The list terminator

type family ToList v rest :: *
type instance ToList ((:+:) l r' p) r = ToList (l p) (ToList (r' p) r)
type instance ToList (K1 a t p)     r = (K1 a t     :+: WithoutParam r) p
type instance ToList ((:*:) l r' p) r = ((l :*: r') :+: WithoutParam r) p
type instance ToList (U1 p)         r = (U1         :+: WithoutParam r) p``````

Now the final piece, we need to write a function which “folds” over a tree of `:+:` and produces a function `(a -> c) -> (b -> c) -> ... -> c`

``````    type family ChurchSum v c :: *
type instance ChurchSum ((:+:) l r p) c = ChurchProd (l p) c -> ChurchSum (r p) c
type instance ChurchSum (ListTerm p) c = c

-- A driver type for the whole thing
type Church t = forall c. ChurchSum (ToList (StripMeta (Rep t ())) (ListTerm ())) c``````

And there we go! As a quick test

``````    {-# LANGUAGE DeriveGeneric #-}
data AFew = S1 Int Int Int | S2 Bool Char | S3 String | S4
deriving Generic``````

And now

``````> kind! Church AFew
(Int -> Int -> Int -> c)
-> (Bool -> Char -> c)
-> ([Char] -> c)
-> (() -> c)
-> c``````

Tada! Now we’ve automated the generation of types for church representations. In the next post we’ll actually go about populating them.