Church encoding? #

Church encoding is a way to talk about datatypes in a simply typed lambda calculus, or in an STLC + polymorphism (preferable).

If you know what an eliminator is, values eliminate themselves. In STLCs, everything is a function. So first of all, I'll show a couple very simple types (Haskell notation):

 1{-# LANGUAGE MagicHash #-}
 2
 3data Zero
 4absurd :: Zero -> a
 5absurd _ = error "value of type zero"
 6type Zero# = ∀ a. a
 7
 8data One = One
 9one :: One -> a -> a
10one One x = x
11type One# = ∀ a. a -> a
12
13data Two = A | B
14two :: Two -> a -> a -> a
15two A a b = a
16two B a b = b
17type Two# = ∀ a. a -> a -> a

My GHC is angry at me about the inaccessible pattern in absurd, but it's also angry if I don't give a definition. So be it.

You can see, now, why Church encodings work in the λ-calculus: they're just functions. They even can be used in the untyped λ-calculus.

This doesn't really seem usable... #

Au contraire! They're fairly ergonomical, if you can remember the order of arguments:

 1type Bool# = ∀ a. a -> a -> a
 2
 3true :: Bool#
 4true = \x y -> x
 5false :: Bool#
 6false = \x y -> y
 7
 8-- | if-then-else: ite True x y = x, ite False x y = y
 9ite :: Bool# -> a -> a -> a
10ite b = b
11
12not :: Bool# -> Bool#
13not b = ite b false true
14-- also `flip b`, or `b false true`
15
16and, or :: Bool# -> Bool# -> Bool#
17and a b = a b false
18or a b = a true b

And of course, they also handle infinite types:

 1type N = ∀ a. (a -> a) -> a -> a
 2
 3z :: N
 4z f x = x
 5s :: N -> N
 6s n = (.) <*> n
 7
 8add :: N -> N -> N
 9add a b = \f x -> a f (b f x)
10mul :: N -> N -> N
11mul a b = \f -> a (b f)
12pow :: N -> N -> N
13pow a b = b a

Now that I've (hopefully) won you over, let's get into the problem.

Dependent Types #

I'm going to assume you know what dependent types are. The dependent eliminator for natural numbers is elim: (t: N -> Type) -> t 0 -> ((n: N) -> t n -> t (n+1)) -> (n:N) -> t n. The intuition here is just induction: if you have t 0, and you can turn a t n into a t (n+1), you can get any t n. The trouble is, a term can't be its own eliminator in this way, because its type would depend on itself. Also because this eliminator is sorta based on the constructors, which DNE for the Church encoding.

Simpler, the eliminator for Bool is elim: (t: Bool -> Type) -> t False -> t True -> (b: Bool) -> t b. To Church encode this, we would need b: (t: (∀ a. a -> a -> a) -> Type) -> t (λx y. y) -> t (λx y. x) -> t b. This is problematic because it boils down in some way to b: T(b), which is an unacceptable form of recursion in most type theories and programming languages.

Oh well.