It’s possible to represent data types purely as functions. For example, consider the following type:
data What = Foo | Bar | Baz
What has three inhabitants given by the three nullary value constructors. This can be represented via the Church encoding as follows:
type What1 = forall b. b -> b -> b -> b
What1 also has 3 inhabitants, due to parametricity of b: a function of type
What1 must evaluate to one of its three arguments. The mapping between these two types is given by the following two functions:
to :: What -> What1 to Foo = \x y z -> x to Bar = \x y z -> y to Baz = \x y z -> z from :: What1 -> What from f = f Foo Bar Baz
Note that to extract a value of type
What back out, all you have to do is pass in the value constructors.
What happens when the data constructor is not nullary?
data Where = Location String | Nowhere
It seems plausible to take all the instances of the type in the signature and just replace them with
b. Then, to construct the encoded version, we use
String -> b for Location and
b for Nowhere. Thus:
type Where1 = forall b. (String -> b) -> b -> b to :: Where -> Where1 to (Location s) = \f x -> f s to Nowhere = \f x -> x from :: Where1 -> Where from f = f Location Nowhere
What about a unary type constructor? Modulo newtypes, everything is more of the same:
type Maybe1 a = forall b. (a -> b) -> b -> b to :: Maybe a -> Maybe1 a to (Just s) = \f x -> f s to Nothing = \f x -> x from :: Maybe1 a -> Maybe a from f = f Just Nothing
The situation becomes a little more illuminating when recursive types are considered. Consider the following encoded version of the list type:
type List1 a = forall b. (a -> b -> b) -> b -> b
But this is just a fold on a specific list! It turns out that the encoding of any data type corresponds to its fold.
Exercise: What do
from look like for