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

# A Tutorial on Church Representations

Posted on July 19, 2014

I’ve written a few times about church representations, but never aimed at someone who’d never heard of what a church representation is. In fact, it doesn’t really seem like too many people have!

In this post I’d like to fix that :)

## What is a Church Representation

Simply put, a church representation (CR) is a way of representing a piece of concrete data with a function. The CR can be used through an identical way to the concrete data, but it’s comprised entirely of functions.

They where originally described by Alanzo Church as a way of modeling all data in lambda calculus, where all we have is functions.

## Tuples

The simplest CR I’ve found is that of a tuples.

Let’s first look at our basic tuple API

``````    type Tuple a b = ...
mkTuple :: a -> b -> Tuple a b
fst     :: Tuple a b -> a
snd     :: Tuple a b -> b``````

Now this is trivially implemented with `(,)`

``````    type Tuple a b = (a, b)
mkTuple = (,)
fst     = Prelude.fst
snd     = Prelude.snd``````

The church representation preserves the interface, but changes all the underlying implementations.

``    type Tuple a b = forall c. (a -> b -> c) -> c``

There’s our church pair, notice that it’s only comprised of `->`. It also makes use of higher rank types. This means that a `Tuple a b` can be applied to function producing any `c` and it must return something of that type.

Let’s look at how the rest of our API is implemented

``````    mkTuple a b = \f -> f a b
fst tup     = tup (\a _ -> a)
snd tup     = tup (\_ b -> b)``````

And that’s it!

It’s helpful to step through some reductions here

``````    fst (mkTuple 1 2)
fst (\f -> f 1 2)
(\f -> f 1 2) (\a _ -> a)
(\a _ -> a) 1 2
1``````

And for `snd`

``````    snd (mkTuple True False)
fst (\f -> f True False)
(\f -> f True False) (\_ b -> b)
(\_ b -> b) True false
False``````

So we can see that these are clearly morally equivalent. The only real question here is whether, for each CR tuple there exists a normal tuple. This isn’t immediately apparent since the function type for the CR looks a lot more general. In fact, the key to this proof lies in the `forall c` part, this extra polymorphism let’s us use a powerful technique called “parametricity” to prove that they’re equivalent.

I won’t actually go into such a proof now since it’s not entirely relevant, but it’s worth noting that both `(,)` and `Tuple` are completely isomorphic.

To convert between them is pretty straightforward

``````    isoL :: Tuple a b -> (a, b)
isoL tup = tup (,)

isoR :: (a, b) -> Tuple a b
isoR (a, b) = \f -> f a b``````

Now that we have an idea of how to church representations “work” let’s go through a few more examples to start to see a pattern.

## Booleans

Booleans have the simplest API of all

``````    type Boolean = ...
true  :: Boolean
false :: Boolean
test  :: Boolean -> a -> a -> a``````

We can build all other boolean operations on `test`

``````    a && b = test a b false
a || b = test a true b
when t e = test t e (return ())``````

This API is quite simple to implement with `Bool`,

``````    type Boolean = Bool

true  = True
false = False
test b t e = if b then t else e``````

But how could we represent this with functions? The answer stems from `test`,

``    type Boolean = forall a. a -> a -> a``

Clever readers will notice this is almost identical to `test`, a boolean get’s two arguments and returns one or the other.

``````    true  = \a _ -> a
false = \_ b -> b
test b t e = b t e``````

We can write an isomorphism between `Bool` and `Boolean` as well

``````    isoL :: Bool -> Boolean
isoL b = if b then true else false

isoR :: Boolean -> Bool
isoR b = test b True False``````

## Lists

Now let’s talk about lists. One of the interesting things is lists are the first recursive data type we’ve dealt with so far.

Defining the API for lists isn’t entirely clear either. We want a small set of functions that can easily cover any conceivable operations for a list.

The simplest way to do this is to realize that we can do exactly 3 things with lists.

1. Make an empty list
2. Add a new element to the front of an existing list
3. Pattern match on them

We can represent this with 3 functions

``````    type List a = ...

nil   :: List a
cons  :: a -> List a -> List a
match :: List a -> b -> (a -> List a -> b) -> b``````

If `match` looks confusing just remember that

``    f list = match list g h``

Is really the same as

``````    f []       = g
f (x : xs) = h x xs``````

In this way `match` is just the pure functional version of pattern matching. We can actually simplify the API by realizing that rather than this awkward `match` construct, we can use something cleaner.

`foldr` forms a much more pleasant API to work with since it’s really the most primitive form of “recursing” on a list.

``````    match :: List a -> (a -> List a -> b) -> b -> b
match list f b = fst \$ foldr list worker (b, nil)
where worker x (b, xs) = (f x xs, cons x xs)``````

The especially nice thing about `foldr` is that it doesn’t mention `List a` in its two “destruction” functions, all the recursion is handled in the implementation.

We can implement CR lists trivially using `foldr`

``````    type List a = forall b. (a -> b -> b) -> b -> b

nil = \ _ nil -> nil
cons x xs = \ cons nil -> x `cons` xs cons nil
foldr list cons nil = list cons nil``````

Notice that we handle the recursion in the list type by having a `b` as an argument? This is similar to how the accumulator to `foldr` gets the processed tail of the list. This is a common technique for handling recursion in our church representations.

Last but not least, the isomorphism arises from `foldr (:) []`,

``````    isoL :: List a -> [a]
isoL l = l (:) []

isoR :: [a] -> List a
isoR l f z = foldr f z l``````

## Either

The last case that we’ll look at is `Either`. Like `Pair`, `Either` has 3 different operations.

``````    type Or a b = ...
inl :: a -> Or a b
inr :: b -> Or a b

or :: Or a b -> (a -> c) -> (b -> c)  -> c``````

This is pretty easy to implement with `Either`

``````    type Or a b = Either a b
inl = Left
inr = Right

or (Left a)  f g = f a
or (Right b) f g = g b``````

Once again, the trick to encoding this as a function falls right out of the API. In this case we use the type of `or`

``````     type Or a b = forall c. (a -> c) -> (b -> c) -> c

inl a = \f g -> f a
inr b = \f g -> g a

or x = x``````

Last but not least, let’s quickly rattle off our isomorphism.

``````    isoL :: Or a b -> Either a b
isoL o = o Left Right

isoR o :: Either a b -> Or a b
isoR o = or o``````

## The Pattern

So now we can talk about the underlying pattern in CRs. First remember that for any type `T`, we have a list of `n` distinct constructors `T1` `T2` `T3``Tn`. Each of the constructors has a `m` fields `T11`, `T12`, `T13`

Now the church representation of such a type `T` is

``````    forall c.  (T11 -> T12 -> T13 -> .. -> c)
-> (T21 -> T22 -> T23 -> .. -> c)
...
-> (Tn1 -> Tn2 -> Tn3 -> .. -> c)
-> c``````

This pattern doesn’t map quite as nicely to recursive types. Here we have to take the extra step of substituting all occurrences of `T` for `c` in our resulting church representation.

This is actually such a pleasant pattern to work with that I’ve written a library for automatically reifying a type between its church representation and concrete form.

## Wrap Up

Hopefully you now understand what a church representation is. It’s worth noting that a lot of stuff Haskellers stumble upon daily are really church representations in disguise.

My favorite example is `maybe`, this function takes a success and failure continuation with a `Maybe` and produces a value. With a little bit of imagination, one can realize that this is really just a function mapping a `Maybe` to a church representation!

If you’re thinking that CRs are pretty cool! Now might be a time to take a look at one of my previous posts on deriving them automagically.