The Wikipedia page on Scott encoding has some useful insights. The short version is, what you're referring to is the Church encoding, and your "hypothetical pattern-match encoding" is the Scott encoding. Both are sensible ways of doing things, but the Church encoding requires lighter type machinery to use (in particular, it does not require recursive types).
The proof that the two are equivalent uses the following idea:
churchfold :: (a -> b -> b) -> b -> [a] -> b
churchfold _ z [] = z
churchfold f z (x:xs) = f x (churchfold f z xs)
scottfold :: (a -> [a] -> b) -> b -> [a] -> b
scottfold _ z [] = z
scottfold f _ (x:xs) = f x xs
scottFromChurch :: (a -> [a] -> b) -> b -> [a] -> b
scottFromChurch f z xs = fst (churchfold g (z, []) xs)
where
g x ~(_, xs) = (f x xs, x : xs)
The idea is that since churchfold (:) []
is the identity on lists, we can use a Church fold that produces the list argument it is given as well as the result it is supposed to produce. Then in the chain x1 `f` (x2 `f` (... `f` xn) ... )
the outermost f
receives a pair (y, x2 : ... : xn : [])
(for some y
we don't care about), so returns f x1 (x2 : ... : xn : [])
. Of course, it also has to return x1 : ... : xn : []
so that any more applications of f
could also work.
(This is actually a little similar to the proof of the mathematical principle of strong (or complete) induction, from the "weak" or usual principle of induction).
By the way, your Bool r
type is a bit too big for real Church booleans – e.g. (+) :: Bool Integer
, but (+)
isn't really a Church boolean. If you enable RankNTypes
then you can use a more precise type: type Bool = forall r. r -> r -> r
. Now it is forced to be polymorphic, so genuinely only contains two (ignoring seq
and bottom) inhabitants – \t _ -> t
and \_ f -> f
. Similar ideas apply to your other Church types, too.