This website is out of date, please refer to the site on github.

Church Representations: Part 2

Posted on March 7, 2014
Tags: haskell, types

In the last post, we discussed some of the type families needed to transform a type equipped with a Generic instance into a church representation.

In this post, we’ll go over the type class prolog needed to actually mechanically transform values between these types.

To start with, we’ll need a bit of boilerplate. Here’s our language extensions and imports.

    {-# LANGUAGE TypeFamilies,          TypeOperators,     UndecidableInstances #-}
    {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts     #-}
    {-# LANGUAGE ScopedTypeVariables,   RankNTypes                              #-}
    import GHC.Generics
    import Data.Proxy

Now our first order of business is to write a function to take a GHC.Generics value and transform it into the corresponding value occupying the type returned by StripMeta.

To do this we rely on type classes

    class GStripMeta a where
      stripMeta :: a -> StripMeta a
    instance GStripMeta (f p) => GStripMeta (M1 a b f p) where
      stripMeta (M1 f) = stripMeta f
    instance GStripMeta (K1 a t p) where
      stripMeta = id
    instance GStripMeta (U1 p) where
      stripMeta = id
    instance (GStripMeta (l p), GStripMeta (r p),
              (WithoutParam (StripMeta (l p))) p ~ StripMeta (l p),
              (WithoutParam (StripMeta (r p))) p ~ StripMeta (r p)) =>
             GStripMeta ((:*:) l r p) where
      stripMeta (l :*: r) = stripMeta l :*: stripMeta r
    instance (GStripMeta (l p), GStripMeta (r p),
              (WithoutParam (StripMeta (l p))) p ~ StripMeta (l p),
              (WithoutParam (StripMeta (r p))) p ~ StripMeta (r p)) =>
             GStripMeta ((:+:) l r p) where
      stripMeta (L1 l) = L1 $ stripMeta l
      stripMeta (R1 r) = R1 $ stripMeta r

This does some type class prolog to traverse a GHC.Generics value and systematically throw out the M1 annotations. An important technique that I make heavy use of is the ~ equality constraints. These let us assert that two types are equivalent and the type checker will attempt to verify this once it’s selected the appropriate instance later. Other than that there’s not too much of interest here so let’s move on to something with more substance.

Our ToList type family requires quite a bit of work to automagically do with a type family. The base cases are pretty straightforward

    class GList a r where
      toList :: Maybe a -> r -> ToList a r
    instance (WithoutParam r) p ~ r => GList (U1 p) r where
      toList Nothing  r = R1 r
      toList (Just a) _ = L1 a
    instance (WithoutParam r) p ~ r => GList (K1 a t p) r where
      toList Nothing  r = R1 r
      toList (Just a) _ = L1 a
    instance (WithoutParam r) p ~ r => GList ((l :*: r') p) r where
      toList Nothing  r = R1 r
      toList (Just a) _ = L1 a

The trick here is that if we get a Nothing, it means that somewhere in the process of choosing the list we’ve already found state our sum type is in and all we do is pass things of to R1. Otherwise, we shove the value we receive into L1.

Now the tricky bit is the :+: instance which must walk along the spine of our tree flattening things as it goes.

    instance (GList (l p) (ToList (r' p) r), GList (r' p) r) =>
             GList ((l :+: r') p) r where
      toList (Just sum@(L1 l)) r = toList (Just l) (toList (rNot sum) r)
        where rNot :: forall l r p. (l :+: r) p -> Maybe (r p)
              rNot _ = Nothing
      toList (Just sum@(R1 r')) r = toList (lNot sum) (toList (Just r') r)
        where lNot :: forall l r p. (l :+: r) p -> Maybe (l p)
              lNot _ = Nothing
      toList m r = toList (lNot m) (toList (rNot m) r)
        where lNot :: forall l r p. Maybe ((:+:) l r p) -> Maybe (l p)
              lNot _ = Nothing
              rNot :: forall l r p. Maybe ((:+:) l r p) -> Maybe (r p)
              rNot _ = Nothing

We’re just plugging in the appropriate l and r into toList l (toList r rest). if both we have Just (L1 l) then we put in Nothing for r, similarly for Just (R1 r) and if we have Nothing then both are filled in as Nothings.

Notice that we have to a few hoops using lNot and rNot. Otherwise GHC will complain that type classes aren’t injective and it’s not sure how to handle Nothing :: Maybe a. However, a bit of explicit hand holding takes care of this.

For our next type class hacking we need to actually add one type family that I forgot in our last post.

    type family ToListProd v rest
    type instance ToListProd ((:*:) l r' p) r = ToListProd (l p) (ToListProd (r' p) r)
    type instance ToListProd (K1 a t p)     r = (K1 a t     :*: WithoutParam r) p
    type instance ToListProd (U1 p)         r = U1 p -- since U1 is never in `:*:`'s.

This is isomorphic to ToList but instead of restructuring :+:’s, it moves around :*:’s. The corresponding type class for this almost identical to GList

    class GListProd a r where
      toListProd :: a -> r -> ToListProd a r
    instance (WithoutParam r) p ~ r => GListProd (U1 p) r where
      toListProd = const -- Throw away the rest which must be ListTerm
    instance (WithoutParam r) p ~ r => GListProd (K1 a t p) r where
      toListProd = (:*:)
    instance (GListProd (l p) (ToListProd (r' p) r), GListProd (r' p) r) =>
             GListProd ((:*:) l r' p) r where
      toListProd (l :*: r) rest = toListProd l (toListProd r rest)

The only notable difference here is that we don’t have a Maybe a since with products both sides our present. This makes the whole thing much simpler.

No we’re ready to proceed to the actual transformation type classes.

    class GChurchProd a where
      prod :: Proxy r -> a -> ChurchProd a r -> r -- Proxy needed for GChurchSum
    instance GChurchProd (U1 p) where
      prod _ _ f = f
    instance GChurchProd (K1 a t p) where
      prod _ (K1 r) f = f r
    instance GChurchProd (r p) => GChurchProd ((:*:) (K1 a t) r p) where
      prod p (K1 l :*: r) f = prod p r (f l)

    class Swallow a where
      swallow :: Proxy a -> c -> ChurchSum a c
    instance Swallow (ListTerm p) where
      swallow _ c = c
    instance Swallow (r p) => Swallow ((:+:) l r p) where
      swallow p c = \_ -> swallow (right p) c
        where right :: forall l r p. Proxy ((:+:) l r p) -> Proxy (r p)
              right _ = Proxy

In GChurchProd we take a value and the corresponding product eliminator and eliminate it. Believe it or not this is essentially the workhorse of this entire library. We’re threading a Proxy r through there which will come in handy when we start to use this in GChurchSum.

Swallow is a bit odd. It represents a situation where we’ve already used prod to produce our result and now need to eat the rest of the supplied arguments. Note again the use of Proxy to keep track of types, it’s a useful little library!

Now, finally, GChurchSum

    class GChurchSum a r where
      elim :: Proxy r -> a -> ChurchSum a r -- Proxy because type inference is stubborn

    instance (GListProd (l p) (ListTerm ()), GChurchProd (ToListProd (l p) (ListTerm ())),
              GChurchSum (r' p) r, Swallow (r' p)) =>
             GChurchSum ((:+:) l r' p) r where
      elim p sum@(L1 l) = \f ->
        swallow (right sum) (prod p (toListProd l (ListTerm :: ListTerm ())) f)
        where right :: forall l r p. (:+:) l r p -> Proxy (r p)
              right _ = Proxy
      elim p (R1 r) = \_ -> elim p r
    instance GChurchSum (ListTerm p) r where
      elim _ _ = error "Malformed generic instance"

Now the elim instance for ListTerm can never be called, this is guarenteed by the definition of toList since a type must occupy one state prior to ToList, we’ll never end up with ListTerm.

Otherwise if we get an L1 then we’re at the actual value our sum type is in so we produce an r and swallow the rest of our arguments, notice that this is where we actual transform a leaf into a ToListProd and this is reflected in our constraints. Otherwise we ignore the irrelevant eliminator and recurse!

To put it all together

    from' :: Generic a => a -> Rep a ()
    from' = from

    toChurch :: forall a r.
                (Generic a, GStripMeta (Rep a ()),
                 GList (StripMeta (Rep a ())) (ListTerm ()),
                 GChurchSum (ToList (StripMeta (Rep a ())) (ListTerm ())) r) =>
                a -> Church a r
    toChurch = elim p . flip toList (ListTerm :: ListTerm ()) . Just . stripMeta . from'
      where p = Proxy :: Proxy r

And we’re done! Using this we can reify a type to it’s church representation. We can mostly ignore that scary looking constraints on toChurch since they should be true by construction.

As a demo

> toChurch [1, 2, 3] True (\_ _ ->  False)
> toChurch [] True (\_ _ ->  False)

The True corresponds to the [] list case and the function represents (:). The current True (\_ _ -> False) actually computes null.

Edit, added GListProd

comments powered by Disqus