It’s possible to represent data types purely as functions. For example, consider the following type:

data What = Foo | Bar | Baz

Ignoring undefined, 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 to and from look like for List1 a?