Type Systems #15: A Church Encoding of Lists

(This is part 15 in a series on type systems. You can find part 14 here .)

We’ve seen a lot of lambda calucli so far, haven’t we! Each one builds upon the last, adding new features and new concepts. We saw the untyped lambda calculus, then the simply typed lambda calculus, then System F, and then System F<:.

Quite an impressive repertoire — we’ve built that up from nothing, and you know all the nitty-gritty details now!

But believe me when I say that we are far from done. To get to more of the juicy bits however, we will need a more complicated data structure we can use for examples.

All the way back in post #1 we saw how we can encode booleans in the untyped lambda calculus using so-called Church encodings… and while it’s a fun party trick, and Church encodings are very prevalent in every post or paper about type theory, I purposefully avoided giving them too much attention, because in regular programming languages you never use them. Like yes you can encode true as λt. λf. t — but in the real world we just use a single bit instead.

Anyhow, the type of a Church-encoded list of integers is IntList = ∀R. R → (Int → R → R) → R, which looks scary at first, but it will turn out that you knew it all along.

I will rush through this a bit, because there is no way not to rush through this — Church encodings really deserve a series of their own. For the purposes of this series I just want to give some justification for when I will say things like “the type of a list is ∀R. R → (Int → R → R) → R” in the future. If you are interested in constructing lists ex nihilo, I recommend you to program along in typescript as we go through this. That way you can see how data flows through the functions, and in which order things are called, which is really helpful to build intuition. It’s also a fun exercise!

Lists in pure lambda calculus

As programmers, we sometimes get to ask questions like, “what even is an AbstractDtoFactory? What is it’s essence?”, and then we spend hours delineating what does and what doesn’t constitute the essence of an AbstractDtoFactory, what to put into that class and what to put somewhere else. It really makes me feel like a philosopher at times.

What would you say is the essence of a list? Can we single out a single core property that all lists have? Like a single thing you can do with a list, that you cannot do to non-lists?

We could argue that lists are mappable, and that map is the essence of lists. Or perhaps filter is more fundamental? Are lists collections you can filter? Maybe what defines lists is that you can concatenate two of them to make a larger one.

Well, these are all good candidates, but there is one operation that is more fundamental than all of them: A fold, or what we could call reduce in typescript. Folds allow you to merge a list into a single value, for example to take a list of integers and sum them. The “single value” you are returning can be of any type though, and that includes lists themselves, which makes folds powerful enough to express map, and filter, and concatenate as well.

It’s a fun exercise so give it a try! Implement the other three functions in terms of just list.reduce(fn, initialValue) — in typescript!

Implement const map = <A, B>(list: A[], fn: (a: A) => B): B[] => ...

const map = <A, B>(list: A[], fn: (a: A) => B): B[] => {
  return list.reduce((acc, a) => {
    acc.push(fn(a));
    return acc;
  }, [] as B[]);
};

Implement const filter = <A>(list: A[], predicate: (a: A) => boolean): A[] => ...

const filter = <A>(list: A[], predicate: (a: A) => boolean): A[] => {
  return list.reduce((acc, a) => {
    if (predicate(a)) { 
      acc.push(a);
    }
    return acc;
  }, [] as A[]);
};

Implement const concatenate = <A>(list1: A[], list2: A[]): A[] => ...

const concatenate = <A>(list1: A[], list2: A[]): A[] => {
  return list1.reduce((acc, a) => {
    acc.push(a);
    return acc;
  }, list2);
};

Folds are powerful!

What would the type of a fold be? It takes an initial value, and a function merging a value with an accumulator, and returning the next accumulator. If the list contains Ints, and the accumulator is of any type R, then the type of fold would be:

fold :: ∀R. R → (Int → R → R) → R

Wait. What was the type of our Church encoded list again?

IntList = ∀R. R → (Int → R → R) → R

Oh yeah. It’s the same.

A List is literally just it’s own fold function. Mind = blown!

For completeness

Let’s write out the full Church encoding of lists of integers for completeness. We use a linked-list kind of construction here, where nil is the empty list, and cons head tail constructs a new list with head as the first element, and tail as the rest of the list.

When we define nil and cons constructors that return IntLists, that are just folds, we are essentially defining how a fold should behave for those two cases. Folding a nil returns the initial value, and folding a cons head tail recursively applies a 2-parameter function to head, and the result of folding the tail.

nil : IntList
nil = ΛR.
  λinitialValue: R.
  λx: Int → R → R.
    initialValue

cons : Int → IntList → IntList
cons = λhead: Int. λtail: IntList.
    ΛR.
      λinitialValue: R.
      λaggregate: Int → R → R.
        aggregate head (tail [R] initialValue aggregate)

With these helper functions we can now construct a list like so:

myList : IntList
myList = cons 1 (cons 2 (cons 3 nil))

This is the list containing the integers 1, 2, and 3. And, well, folding a list is pretty easy, since a list is just it’s own fold function:

sum = myList 0 (λx. λacc. add x acc) // sum == 6

And once we have folds, we can do any other list operation, meaning we have successfully defined lists in terms of just pure lambda calculus! It’s functions all the way down.

Church encodings can be a bit rough if you are not used to them. It took me a long long time until I was able to shake the feeling of “what do you mean everything is a function, at some point you must hit atomic values”, or “what do you mean a list is a fold, the list is the thing you fold, where does a fold function even store data”. Pure lambda calculus can be a mind twister for sure and it takes a while to really grok it.

For this reason, for the purposes of this series, I try to avoid Church encodings and just assume “Integers are given” and “Lists are given” wherever possible. I mean, even the integers in this examples I took as given, but you could Church-encode those as well if you wanted to go full lambda.

I do hope I gave enough intuition and context for you to understand that lists are just folds, and what the type ∀R. R → (Int → R → R) → R means when I say “this is the type of a list of integers” — we’ll need this later.

(This is part 15 in a series on type systems. You can find part 16 here .)