We ended up discussing the Scott encoding of lists, and of natural numbers. The Scott encoding works for any algebraic data type. The predecessor function is much easier to define than for the Church encoding:
I also showed how Church numerals can be written as Haskell functions, and readily decoded into Haskell Ints. However, writing type signatures for them got a little tricky. In some cases, it's better to let Haskell infer the type for you. In other cases, it won't work unless you specify the type. The central problem is that the lambda calculus is untyped, but we are being forced to specify types in Haskell.
We can define
type Church t = (t -> t) -> (t -> t)
but sometimes the same Church numeral must be used at different instances of t. It may help to define it with a polymorphic data type:
newtype Church = Church (forall t. (t -> t) -> (t -> t))
Yep... I tried that, and I stopped getting inscrutable types for my functions. Even the predecessor function is very simple, just
churchPredAux :: Church -> (Church, Church)
churchPredAux (Church n) = n (\x -> (snd x, churchSucc (snd x))) (churchZero, churchZero)
churchPred :: Church -> Church
churchPred = snd . churchPredAux
Ed came up with a solution [to the "length" function in Exercise 1] which seems equivalent, but we didn't quite prove that equivalence.