Intuition of Church Encoding

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.