Church Representations

A project I’ve been playing with lately is generalizing maybe. Now on the surface that sounds well.. boring. But there’s actually some interesting concepts buried in here.

Lambda The Almighty

Let’s start by specifying what I mean when I say “generalize”. When we look at maybe, the type gives us a pretty strong clue on how to implement it

    maybe :: b -> (a -> b) -> Maybe a -> b
    maybe nothingCase justCase Nothing  = nothingCase
    maybe nothingCase justCase (Just a) = justCase a

Each argument of corresponds to a different case of the sum type Maybe.

There’s actually a name for this idea, it’s encoding a data type within functions: Church Encoding.

Let’s rattle of some examples:

Tuples

    {-# LANGUAGE RankNTypes #-}
    -- We'll call a tuple a Product because it
    -- looks like the cartesion *product* of two types
    type Product a b = forall c. (a -> b -> c) -> c
    pair :: a -> b -> Product a b
    pair a b = \destruct -> destruct a b

    -- We can easily make fst and snd
    fst :: Product a b -> a
    fst p = p $ \a b -> a
    snd :: Product a b -> b
    snd p = p $ \a b -> b

We can do Either as well

    -- We'll call Either a "sum" because it
    -- looks like the disjoint union (sum) of two types
    type Sum a b = forall c. (a -> c) -> (b -> c) -> c
    inl :: a -> Sum a b
    inl a = \l r -> l a

    inr :: b -> Sum a b
    inr b = \l r -> r b

Look familiar? That’s just Data.Either.either! Now if we squint at these we can imagine building up more complex types from these building blocks

    data AFew = NoVal | OneVal Int | ThrVal Int Bool String

    type ChurchAFew =
      Sum () (Sum Int (Prod Int (Prod Bool String)))

    noVal :: ChurchAFew
    noVal = inl ()

    oneVal :: Int -> ChurchAFew
    oneVal i = inr (inl i)

    thrVal :: Int -> Bool -> String -> ChurchAFew
    thrVal i b s = inr . inr . pair i $ pair b s

And now pattern matching more or less falls out for free from ChurchAFew. Since it’s a function we transform

    case foo of
      NoVal        -> ...
      OneVal i     -> ...
      ThrVal i b s -> ...
    -- becomes
    foo (\() -> ...) (\p -> p (\i -> ...) (\p1 -> p1 (\i p2 -> ...)))

Such is the power of lambda! And there are all sorts of fun side effects of pattern matching being a function, most of it to do with nicer composition with point-free functions.

But It’s Boring!

There’s a drawback here, boilerplate! We have to essentially duplicate all our data declarations, extra boilerplate for generating accessors, and then two functions to map back and forth between our representations.

As a programmer I’m far too lazy to write all that!

Whenever we start to think of terms of sum and product types it’s time to turn to GHC.Generics. It’s a library that provides a type class to reify our normal types into explicit sums and products and back again.

The first thing we have to do is write a type level function to reify a GHC.Generics representation to the appropriate type.

For example Maybe Int has the following representation

    M1
        D
        GHC.Generics.D1Maybe
        (M1 C GHC.Generics.C1_0Maybe U1
         :+: M1 C GHC.Generics.C1_1Maybe (M1 S NoSelector (K1 R Int)))

We can strip out all the M1 meta information since we don’t really care leaving

    U1 :+: K1 R Int

Not so bad! Let’s start by writing a type level function (type family) to get rid the M1 constructors

    {-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances, RankNTypes #-}

    import GHC.Generics

    -- | Remove the extra `p` parameter that GHC.Generics
    -- lugs through every constructor
    type family WithoutParam v :: * -> *
    type instance WithoutParam ((:+:) l r p) = l :+: r
    type instance WithoutParam ((:*:) l r p) = l :*: r
    type instance WithoutParam (U1 p)        = U1
    type instance WithoutParam (K1 a t p)    = K1 a t

    -- | Strip out `M1` tags
    type family StripMeta v :: *
    type instance StripMeta (M1 a b f p)  = StripMeta (f p)
    type instance StripMeta (K1 a t p)    = K1 a t p
    type instance StripMeta ((:+:) l r p) =
      (:+:) (WithoutParam (StripMeta (l p))) (WithoutParam (StripMeta (r p))) p
    type instance StripMeta ((:*:) l r p) =
      (:*:) (WithoutParam (StripMeta (l p))) (WithoutParam (StripMeta (r p))) p
    type instance StripMeta (U1 p)        = U1 p

As we can see these type families are well.. pretty terrible. But they work! Next we can actually do some real work. We need to take a product type with one or more members and turn it into a function.

    type family ChurchProd v c :: *
    type instance ChurchProd (K1 a t p) c    = t -> c
    type instance ChurchProd (U1 p)     c    = () -> c
    type instance ChurchProd ((:*:) l r p) c =
      ChurchProd (l p) (ChurchProd (r p) c)

So here we have a type family with two parameters, the term and the “out” type. These take a :*: b :*: c to a -> b -> c -> .... This is important because GHC.Generics represents things like a list where the (:) equivalent is :+: and the each leaf is product or unit type.

Now at least we can run

> :kind! ChurchProd (StripMeta (Rep (Int, Bool) ())) Char
ChurchProd (StripMeta (Rep (Int, Bool) ())) Char :: *
= Int -> Bool -> Char

As it happens, I told a small fib, GHC.Generics doesn’t make quite a list. In fact it makes a tree! We can rejigger things to a list though

    data ListTerm p -- The list terminator

    type family ToList v rest :: *
    type instance ToList ((:+:) l r' p) r = ToList (l p) (ToList (r' p) r)
    type instance ToList (K1 a t p)     r = (K1 a t     :+: WithoutParam r) p
    type instance ToList ((:*:) l r' p) r = ((l :*: r') :+: WithoutParam r) p
    type instance ToList (U1 p)         r = (U1         :+: WithoutParam r) p

Now the final piece, we need to write a function which “folds” over a tree of :+: and produces a function (a -> c) -> (b -> c) -> ... -> c

    type family ChurchSum v c :: *
    type instance ChurchSum ((:+:) l r p) c = ChurchProd (l p) c -> ChurchSum (r p) c
    type instance ChurchSum (ListTerm p) c = c


    -- A driver type for the whole thing
    type Church t = forall c. ChurchSum (ToList (StripMeta (Rep t ())) (ListTerm ())) c

And there we go! As a quick test

    {-# LANGUAGE DeriveGeneric #-}
    data AFew = S1 Int Int Int | S2 Bool Char | S3 String | S4
              deriving Generic

And now

> kind! Church AFew
(Int -> Int -> Int -> c)
  -> (Bool -> Char -> c)
  -> ([Char] -> c)
  -> (() -> c)
  -> c

Tada! Now we’ve automated the generation of types for church representations. In the next post we’ll actually go about populating them.