Journal de Chaource

I just realized that there is a snag in the construction of Church encoding for type constructors in System Fω.

The ordinary Church encoding works at the level of types: If a type T is defined recursively as the least fixpoint of T = F T (where F is some endofunctor) then the Church encoding of T is:

T = ∀(r : Type) → (F r → r) → r

Passing from simple types to type constructors: If an endofunctor ("type constructor") C is defined recursively as C = F C with some F being an endofunctor on endofunctors, then we write the Church encoding as:

C a = ∀(r : Type → Type) → (∀(t : Type) → F r t → r t) → r a

We can define List in this way if we choose F as `F C a = 1 + a × C a`.
Then, after some currying, we obtain the following definition of List:

List a = ∀(r : Type → Type) → (∀(t : Type) → r t) → (∀(t : Type) → t → r t → r t) → r a

Then we can define helper functions for creating values of type `List a`, or to do foldRight, to concatenate lists, and so on. Iteration over the Church-encoded list will be non-recursive.

This is the Church encoding "at the level of type constructors" (or, you might say, "in the category of endofunctors" if you want to be brazen about it, because actually I don't know how to formulate the Church encoding categorically even in the simple case).

I used to think that this kind of Church encoding works just fine and is perhaps an overkill for List but has its uses to encode more complicates types such as GADTs or perfect trees:

PerfectTree a = a + PerfectTree (a × a)

The curried Church encoding of PerfectTree looks like this:

PerfectTree a = ∀(r : Type → Type) → (∀(t : Type) → t → r t) → (∀(t : Type) → r (t, t) → r t) → r a

However, that thinking was just too glib. There is a heavy price to be paid if you want to use this kind of encoding.

The price is that you can't easily extract data from a List encoded in this way when your computations are not type-generic.

The Church encoding "in the category of endofunctors" works well as long as you just want to write natural transformations on endofunctors.
It is straightforward to write natural transformations such as List a → Option a or List a → List a.

But to compute the sum of all numbers in a list of type `List Int` is far from obvious. You need to specify arguments of types `∀(t : Type) → r t` and `∀(t : Type) → t → r t → r t`, for some appropriately chosen `r`. The final result must be an `Int`, so we could define `r` as a constant functor returning `Int`. The function of type `∀(t : Type) → r t` must compute a result for empty lists; this can be done as `λ(t : Type) → 0`. But we won't be able to implement a function of type `∀(t : Type) → t → r t → r t`, which is `∀(t : Type) → t → Int → Int`, because we can't add integers to values of an unknown type `t`. Of course, in practice this `t` will be `Int` when we create values of Church-encoded type `List Int`. But the fact that `t = Int` is hidden and we are required to produce a type-generic function of type `∀(t : Type) → t → Int → Int`.

In a language where type information is available at run time, like Scala, we could write something like:

def update[T](x : t, prev: Int) : Int = x match {
   case i : Int => i + prev
   case _ => throw new Exception("this will never happen but we have to throw")
}

This is ugly, and in any case this is not possible to do in System Fω. Why do we have to jump through hoops just to be able to compute the sum of a list of integers?

Right now I'm thinking in the direction of setting `r` not to a constant functor always returning Int, but to a special GADT, denoted R, such that `R a` is void unless `a = Int`, while `R Int = Int`. This kind of GADT can be Church-encoded in System Fω:

R a = ∀(s : Type → Type) → (Int → s Int) → s a

I haven't yet had time to figure out if this helps when computing the sum of integers in a list. We would need to implement a function of this type:

∀(t : type) → ∀(s : Type → Type) → (Int → s Int) → t → s t

It is not clear to me that one could write such a function in pure System Fω.