Church Representations: Part 3
To conclude my recent spat of posts on church representations I’d like to write one more.
My last two posts have focused on taking a random value and turning it into a nifty function that we can use in place of the value. In this post I’ll show to invert the process and given a function, return a value.
This requires a lot more intricate type level programming, so let’s start by turning on our slew of language extensions and importing a few libraries.
{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables, PolyKinds, DataKinds #-}
import Data.Proxy
import GHC.GenericsWe’ll start by defining a few useful type families across type level lists (-XDataKinds has promoted [] for us).
type family Head (xs :: [k]) :: k
type instance Head (x ': xs) = x
type family Tail (xs :: [k]) :: [k]
type instance Tail (x ': xs) = xs
pHead :: Proxy xs -> Proxy (Head xs)
pHead = reproxy
pTail :: Proxy xs -> Proxy (Tail xs)
pTail = reproxy
type family Append (xs :: [k]) (ys :: [k]) :: [k]
type instance Append '[] ys = ys
type instance Append (x ': xs) ys = x ': Append xs ys
type family Reverse (xs :: [k]) :: [k]
type instance Reverse '[] = '[]
type instance Reverse (x ': xs) = Append (Reverse xs) (x ': '[])There’s not too much of interest here, but it’s worth noting the syntax for type level lists '[] and ':. Additionally, I’ve made these functions polykinded for reasons that will become apparent momentarily.
A High Level Outline
Since the actual procedure for this is much more complex than going to a Church, it’s useful to have a high level overview of how we plan on doing this.
The 10,000 foot idea is something like this
- Take in the church representation which has the form
(a -> r) -> (b -> c -> r) -> r -> ror similar - Apply the constructors of the type we’re interested in to the church representation
- Let the representation do the actual work of constructing the value
Our first major hiccup is that we don’t actually have access to the constructors. Instead we’ll traverse the generic representation of our type, and produce a type level list of “breadcrumbs” (I’ll explain more shortly) that can be fed to a typeclass to yield a function which takes either a U1 p, K1 a t p, or some large combination of :*:’s and returns our value. This serves as our makeshift constructor.
However, this alone isn’t enough since we need to provide a function of type a -> b -> r not M1 foo bar (K1 baz a) :*: M1 foo bar (K1 quux a) -> r. We need something akin to the ultimate “uncurry” that’ll take in a large product type component by component and build it up. In order to do this, we’ll introduce a “shell” of a product type where each node is undefined, then as we get each new argument, we’ll fill in the corresponding undefined in the product type.
This isn’t the nicest solution, since we’re playing with fire by tossing around undefined, but it’s much simpler than the alternatives which is to either somehow convert a tree of product types into a flat constructor or make each field of the product type maybe and step by step fill in each field and change the type of the product type.
The Gory Details
Without further delay, let’s dive in! First let’s create our type level representation of the “bread-crumbs” we’ll use to represent the type’s structure
In our use case, we’ll specialize a to be *, the kind of simple haskell types.
Now the way to think about this is as a series of directions, each element of the list a specific instruction on how to navigate the type.
Metarepresents a type wrapped in anM1constructor so thatM1 a b f pcorresponds toMeta a b pInLandInRrepresent going left or right in a:+:or:*:. Going left at(l :*: r) pisInL (r p) pTermis the endpoint of our directions, it holds some leaf in the “tree” we’re considering
Now with this in mind, here’s how we can construct all possible paths in our types
type family MakePaths v (m :: [Traverse *]) (r :: [ [Traverse *] ]) :: [[Traverse *] ]
type instance MakePaths ((:+:) l r p) s all =
Append (MakePaths (l p) (InL (r p) p ': s) '[])
(Append (MakePaths (r p) (InR (l p) p ': s) '[]) all)
type instance MakePaths (M1 a b f p) s all =
MakePaths (f p) (Meta a b p ': s) all
type instance MakePaths (K1 a t p) s all = Reverse (Term (K1 a t p) ': s) ': all
type instance MakePaths (U1 p) s all = Reverse (Term (U1 p) ': s) ': all
type instance MakePaths ((:*:) l r p) s all = Reverse (Term ((:*:) l r p) ': s) ': allThis traverse each path, maintaining a stack of all the current stuff seen as s previous paths as all. Similarly, we can also reconstruct the original type given a path
type family ReconstructPath (t :: [Traverse *])
type instance ReconstructPath (InL r p ': rest) =
(WithoutParam (ReconstructPath rest) :+: WithoutParam r) p
type instance ReconstructPath (InR l p ': rest) =
(WithoutParam l :+: WithoutParam (ReconstructPath rest)) p
type instance ReconstructPath (Meta a b p ': rest) =
M1 a b (WithoutParam (ReconstructPath rest)) p
type instance ReconstructPath (Term a ': '[]) = aNow it should be clear why we need to store the p and the other side of :*:s and :+:s, without them we couldn’t possible reconstruct the type.
We need one final type family before we can start doing real work, this needs to take a path and return the type that the path leads to, in other words the Term a at the end of our list.
Extracting this is pretty mechanical
type family PathArg (t :: [Traverse *])
type instance PathArg (Term a ': '[] ) = a
type instance PathArg (Meta a b p ': rest) = PathArg rest
type instance PathArg (InR l p ': rest) = PathArg rest
type instance PathArg (InL r p ': rest) = PathArg restWe only need to explicitly pattern match on Meta’s and others because type families don’t have the same convenient “fall through” semantics as normal Haskell functions.
Notice that we expect our list to be terminated by a Term a ': '[], if they aren’t it represents a bug in MakePaths and will fail at compile time.
Now we can actually start writing some transformations, first let’s define a function that takes a [Traverse *] and the corresponding PathArg and returns our type
class GPath (p :: [Traverse *]) where
path :: Proxy p -> PathArg p -> ReconstructPath p
instance GPath (Term a ': '[]) where
path _ = id
instance ((WithoutParam (ReconstructPath rest)) p ~ ReconstructPath rest, GPath rest)
=> GPath (InR r p ': rest) where
path p a = R1 $ path (pTail p) a
instance ((WithoutParam (ReconstructPath rest)) p ~ ReconstructPath rest, GPath rest)
=> GPath (InL l p ': rest) where
path p a = L1 $ path (pTail p) a
instance ((WithoutParam (ReconstructPath rest)) p ~ ReconstructPath rest, GPath rest)
=> GPath (Meta a b p ': rest) where
path p a = M1 $ path (pTail p) aThis code rolls out pretty similarly to how ReconstructPath works, the only difference is at the end of it all we stick the PathArg we’ve been lugging around with us into the appropriate “slot” in our type.
Now we just need to take a series of paths and somehow give them to the church representation with path to mimic constructors
class GBuild (paths :: [[Traverse *] ])f r where
build :: Proxy paths -> f -> r
-- | Unit case. This represents constructors with no arguments
instance (ReconstructPath x ~ r, GPath x, GBuild xs f' r, PathArg x ~ U1 p)
=> GBuild (x ': xs) (r -> f') r where
build p f = build (pTail p) $ f (path (pHead p) U1)
instance (???) => GBuild (x ': xs) ((f -> g) -> f') r where
build p f = build (pTail p) $ f (??? $ path (pHead p))
instance GBuild '[] r r where
build _ f = fSo build takes a list of paths by Proxy, the church representation f, and returns our result r, the last instance is the simplest, it represents once we’ve fully applied the church representation and can now just return it.
The next simplest one is the first one, where we have a constructor with no arguments so the PathArg is U1 p. Since we can trivially construct a U1 p, we just do so and give it to path ourselves, this creates an r that we can give to the church representation. Recall that for a Church a r, no argument constructors of a are simply represented with r.
Now the tricky bit, in the second instance we must fill in ??? with something that takes a product type and converts it to something that will swallow and fill in our product type step by step.
Our first step in doing this is to create a generic way of creating “empty” product types
class GEmpty a where
empty :: a
instance GEmpty (U1 p) where
empty = U1
instance GEmpty (K1 a t p) where
empty = K1 (error "Error! The impossible has happened.")
instance GEmpty (f p) => GEmpty (M1 a b f p) where
empty = M1 empty
instance (GEmpty (l p), GEmpty (r p)) => GEmpty ((:*:) l r p) where
empty = empty :*: emptyIt’s pretty clear how this works. Everything except K1’s are filled in with empty’s and K1 is filled in with something equivalent to undefined.
Now we can write a type family to give us the paths to each K1 in a product type
type family MakeProdPaths v (m :: [Traverse *]) (r :: [ [Traverse *] ]) :: [[Traverse *] ]
type instance MakeProdPaths (K1 a t p) s all = Reverse (Term (K1 a t p) ': s) ': all
type instance MakeProdPaths (M1 a b f p) s all = MakeProdPaths (f p) (Meta a b p ': s) all
type instance MakeProdPaths ((:*:) l r p) s all =
Append (MakeProdPaths (l p) (InL (r p) p ': s) '[])
(Append (MakeProdPaths (r p) (InR (l p) p ': s) '[]) all)This should strike the reader as very similar to MakePaths because it is. In fact the only real difference is that we only accept K1’s in nodes and that we’re branching on :*:’s.
Just like MakePaths, we’ll want a corresponding type class to take a path and a value and fill in the corresponding bit of our structure.
class GUpdate (path :: [Traverse *]) a where
update :: Proxy path -> a -> PathArg path -> a
instance GUpdate (Term (K1 a t p) ': '[]) (K1 a t p) where
update _ _ a = a
instance GUpdate rest (l p) => GUpdate (InL (r p) p ': rest) ((:*:) l r p) where
update p (l :*: r) a = update (pTail p) l a :*: r
instance GUpdate rest (r p) => GUpdate (InR (l p) p ': rest) ((:*:) l r p) where
update p (l :*: r) a = l :*: update (pTail p) r a
instance GUpdate rest (f p) => GUpdate (Meta a b p ': rest) (M1 a b f p) where
update p (M1 f) a = M1 (update (pTail p) f a)Unlike GPath, we take in a structure instead of updating it instead of creating an entirely new one. Notice that we’re careful to never be strict in any leaves of the structure since we intend to use this with GEmpty and all those leaves will blow up if poked.
Now for the really clever bit, we can use update to create a function which will take in an argument and the corresponding path to fill it in in the structure.
type family Fill (paths :: [[Traverse *] ]) r
type instance Fill (x ': xs) r = StripK (PathArg x) -> Fill xs r
type instance Fill '[] r = r
class GFill (paths :: [[Traverse *] ]) a where
fill :: Proxy paths -> (a -> r) -> a -> Fill paths r
instance GFill '[] a where
fill _ f a = f a
instance (PathArg x ~ K1 m t p, StripK (PathArg x) ~ t, GUpdate x a, GFill xs a) =>
GFill (x ': xs) a where
fill p f a = \x -> fill (pTail p) f $ update (pHead p) a (K1 x)Fill represents the type of these functions. While most of this code is as one would expect, notice that we take a continuation a -> r and drag it through fill and finally apply it once we’ve filled in all the leaves. There is a good reason for this, we intend to use this with path, but we can’t compose them since fill takes varying amounts of arguments. Instead, we opt for a bit of continuation passing style and through path into fill and let fill call it where appropriate.
Now we can fill in that last bit of GBuild
instance ((f -> g) ~ Fill (MakeProdPaths (PathArg x) '[] '[]) r,
ReconstructPath x ~ r, GEmpty (PathArg x), GBuild xs f' r,
(GFill (MakeProdPaths (PathArg x) '[] '[]) (PathArg x)),
GPath x)
=> GBuild (x ': xs) ((f -> g) -> f') r where
build p f = build (pTail p) $ f (fill (prod p) (path (pHead p)) empty)
where prod :: forall xs. Proxy xs -> Proxy (MakeProdPaths (PathArg (Head xs)) '[] '[])
prod _ = ProxyAnd now we’re almost done! We can wrap all of this up into one function
fromChurch :: forall a. (Generic a,
GBuild (MakePaths (Rep a ()) '[] '[])
(Church a (Rep a ()))
(Rep a ()))
=> Church a (Rep a ()) -> a
fromChurch c = to $ (build p c :: Rep a ())
where p :: Proxy (MakePaths (Rep a ()) '[] '[])
p = ProxyAnd that’s it! Automatic reconstruction of types from church representations! To demonstrate
> fromChurch (\nothing just -> just True) :: Maybe Bool
Just True
> fromChurch (\f -> f 'a' "foo") :: (Char, String)
('a', "foo")Thanks for reading through this (rather dense) series of posts! Most of the code can be found bundled into a package: generic-church.
comments powered by Disqus