After first being introduced to the concept of Church numerals in Structure and Interpretation of Computer Programs, I decided to learn more about them and the more general topic, Church encoding. For those who don’t know, Church encoding defines a way to represent common data types and structures in the Lambda calculus using only functions, since functions are the only terms available.

I eventually stumbled upon a pretty neat intuition for how Church encodings work, which enables you to create encodings for arbitrary data types very easily. But first, a little on how I got there…

I started with the Wikipedia entry, which has a decent amount of examples but is lacking in providing any real intuition into how they work. As an example, the Church encoding for booleans are listed as follows.

true = λa. λb. a false = λa. λb. b

These two functions are the simplest possible two distinct terms, ignoring the identity function so that there can at least be some symmetry (same number of arguments), so in that sense it may seem intuitive to use them. And I can accept that it’s convention in the Lambda calculus to use single letter identifiers, but still I can’t help but wonder what more meaningful identifiers I would use—what do they actually mean?

The Church encoding for natural numbers is a little better.

zero = λf. λx. x succ = λn. λf. λx. f (n f x)

The common intuition for this encoding is that the encoded
`n`

represents a function that takes another function
`f`

as an argument and returns a new function which
applies `f`

to its argument `n`

times. This is
backed up by observing that `zero`

takes any function
`f`

and simply returns the identity function—application
of `f`

zero times does nothing. That’s more satisfying,
but I do wonder if it’s a coincidence that zero is alpha equivalent
to false.

Next up, lists—and this time, an even better standard intuition.

nil = λc. λn. n cons = λh. λt. λc. λn. c h (t c n)

The intuition is that a list is encoded as a fold function, although it might be difficult to see from these
terms. And now I’m really starting to doubt that it’s mere
coincidence that yet again we have an alpha equivalence with
`false`

, this time in the encoding of `nil`

.

## Implementation in Haskell

It was about this time that I decided to try implementing them in Haskell. There are a few implementations out there on the internet already but I wanted to try it from scratch. To start with, I figured I’d just bash in the definitions without type signatures and see what I get.

### Church booleans

λ let true' = \a b -> a λ :t true' true' :: t1 -> t -> t1 λ let false' = \a b -> b λ :t false' false' :: t -> t1 -> t1

Defining a type that works in all the ways I would like is a little trickier than I expected, but not too difficult.

{-# LANGUAGE RankNTypes #-} newtype Bool' = Bool' { runBool' :: forall a. a -> a -> a } true' :: Bool' true' = Bool' $ \a b -> a false' :: Bool' false' = Bool' $ \a b -> b

### Church numerals

λ let zero' = \f x -> x λ :t zero' zero' :: t -> t1 -> t1 λ let succ' = \n f x -> f (n f x) λ :t succ' succ' :: ((t1 -> t) -> t2 -> t1) -> (t1 -> t) -> t2 -> t

The trick for this one is in recognising that the first argument to
`succ’`

is supposed to be a numeral, so its type signature
in `succ’`

should give us a good place to start.

newtype Nat' = Nat' { runNat' :: forall a. (a -> a) -> a -> a } zero' :: Nat' zero' = Nat' $ \f x -> x succ' :: Nat' -> Nat' succ' n = Nat' $ \f x -> f (runNat' n f x)

### Church lists

λ let nil' = \c n -> n λ :t nil' nil' :: t -> t1 -> t1 λ let cons' = \h t c n -> c h (t c n) λ :t cons' cons' :: t1 -> ((t1 -> t2 -> t) -> t3 -> t2) -> (t1 -> t2 -> t) -> t3 -> t

Again, the trick here was in recognising that the return type after two arguments is a list.

newtype List' a = List' { runList' :: forall b. (a -> b -> b) -> b -> b } nil' :: List' a nil' = List' $ \c n -> n cons' :: a -> List' a -> List' a cons x xs = List' $ \c n -> c x (runList' xs c n)

## Comparison with standard definitions

At this point I thought it would be interesting to compare these types with the standard type definitions in the Prelude for the actual types. I decided to list out the standard data definitions in generalised algebraic datatype format.

data Bool = True :: Bool | False :: Bool newtype Bool' = Bool' { runBool' :: forall a. a -> a -> a } data Nat = Succ :: Nat -> Nat | Zero :: Nat newtype Nat' = Nat' { runNat' :: forall a. (a -> a) -> a -> a } data List a = Cons :: a -> List a -> List a | Nil :: List a newtype List' a = List' { runList' :: forall b. (a -> b -> b) -> b -> b }

And as I did this, I noticed a pattern! If you take the type
signature of the `run`

function and replace the quantified
type with the type being declared, you get something very
interesting.

Bool' -> Bool' -> Bool' (Nat' -> Nat') -> Nat' -> Nat' (a -> List' a -> List' a) -> List' a -> List' a

In all three cases, the final term is the type itself, and the other terms are the types of the data constructors! Go back up and check for yourself.

## The revelation

What does this mean? It means that the Church encodings are simply abstractions over data constructors! The arguments to the functions of the Church encodings should be data constructors! Let’s go back and try it for ourself.

λ runBool' true' True False True λ runBool' false' True False False λ runNat' zero' (+1) 0 0 λ runNat' (succ' (succ' zero')) (+1) 0 2 λ runList' nil' (:) [] [] λ runList' (cons' 1 (cons' 2 nil')) (:) [] [1,2]

And just like all good revelations, now that I see it it seems so obvious.

So with this knowledge in hand, we can go on to define Church
encodings for any data type we can think of. Let’s try Haskell’s
`Maybe`

and `Either`

types, and while we’re at
it we can use more meaningful identifiers for the lambda terms.

data Maybe a = Just :: a -> Maybe a | Nothing :: Maybe a newtype Maybe' a = Maybe' { runMaybe' :: forall b. (a -> b) -> b -> b } nothing' :: Maybe' a nothing' = Maybe' $ \just nothing -> nothing just' :: a -> Maybe' a just' a = Maybe' $ \just nothing -> just a data Either a b = Left :: a -> Either a b | Right :: b -> Either a b newtype Either' a b = Either' { runEither' :: forall c. (a -> c) -> (b -> c) -> c } left' :: a -> Either' a b left' a = Either' $ \left right -> left a right' :: b -> Either' a b right' b = Either' $ \left right -> right b

You can find these type definitions and related function definitions in my GitHub repository.