How do I use the Church encoding for Free Monads?
Let me describe the difference for a simpler scenario - lists. Let's focus on how one can consume lists:
By a catamorphism, which essentially means that we can express it using
foldr :: (a -> r -> r) -> r -> [a] -> rAs we can see, the folding functions never get hold of the list tail, only its processed value.
By pattern matching we can do somewhat more, in particular we can construct a generalized fold of type
foldrGen :: (a -> [a] -> r) -> r -> [a] -> rIt's easy to see that one can express
foldrusingfoldrGen. However, asfoldrGenisn't recursive, this expression involves recursion.To generalize both concepts, we can introduce
foldrPara :: (a -> ([a], r) -> r) -> r -> [a] -> rwhich gives the consuming function even more power: Both the reduced value of the tail, as well as the tail itself. Clearly this is more generic than both previous ones. This corresponds to a paramorphism which “eats its argument and keeps it too”.
But it's also possible to do it the other way round. Even though paramorphisms are more general, they can be expressed using catamorphisms (at some overhead cost) by re-creating the original structure on the way:
foldrPara :: (a -> ([a], r) -> r) -> r -> [a] -> r
foldrPara f z = snd . foldr f' ([], z)
where
f' x t@(xs, r) = (x : xs, f x t)
Now Church-encoded data structures encode the catamorphism pattern, for lists it's everything that can be constructed using foldr:
newtype List a = L (forall r . r -> (a -> r -> r) -> r)
nil :: List a
nil = L $ \n _ -> n
cons :: a -> List a -> List a
cons x (L xs) = L $ \n c -> c x (xs n c)
fromL :: List a -> [a]
fromL (L f) = f [] (:)
toL :: [a] -> List a
toL xs = L (\n c -> foldr c n xs)
In order to see the sub-lists, we have take the same approach: re-create them on the way:
foldrParaL :: (a -> (List a, r) -> r) -> r -> List a -> r
foldrParaL f z (L l) = snd $ l (nil, z) f'
where
f' x t@(xs, r) = (x `cons` xs, f x t)
This applies generally to Church-encoded data structures, like to the encoded free monad. They express catamorphisms, that is folding without seeing the parts of the structure, only with the recursive results. To get hold of sub-structures during the process, we need to recreate them on the way.
You asked for the "general pattern you are missing". Let me give my own attempt at explaining it, though Petr Pudlák's answer is also pretty good. As user3237465 says, there are two encodings that we can use, Church and Scott, and you're using Scott rather than Church. So here's the general review.
How encodings work
By continuation passing, we can describe any value of type x by some unique function of type
data Identity x = Id { runId :: x }
{- ~ - equivalent to - ~ -}
newtype IdentityFn x = IdFn { runIdFn :: forall z. (x -> z) -> z }
The "forall" here is very important, it says that this type leaves z as an unspecified parameter. The bijection is that Id . ($ id) . runIdFn goes from IdentityFn to Identity while IdFn . flip ($) . runId goes the other way. The equivalence comes because there is essentially nothing one can do with the type forall z. z, no manipulations are sufficiently universal. We can equivalently state that newtype UnitFn = UnitFn { runUnitFn :: forall z. z -> z } has only one element, namely UnitFn id, which means that it corresponds to the unit type data Unit = Unit in a similar way.
Now the currying observation that (x, y) -> z is isomorphic to x -> y -> z is the tip of a continuation-passing iceberg which allows us to represent data structures in terms of pure functions, with no data structures, because clearly the type Identity (x, y) is equivalent therefore to forall z. (x -> y -> z) -> z. So "gluing" together two items is the same as creating a value of this type, which just uses pure functions as "glue".
To see this equivalence, we have to just handle two other properties.
The first is sum-type constructors, in the form of Either x y -> z. See, Either x y -> z is isomorphic to
newtype EitherFn x y = EitherFn { runEitherFn :: forall z. (x -> z) -> (y -> z) -> z }
from which we get the basic idea of the pattern:
- Take a fresh type variable
zthat does not appear in the body of the expression. - For each constructor of the data type, create a function-type which takes all of its type-arguments as parameters, and returns a
z. Call these "handlers" corresponding to the constructors. So the handler for(x, y)is(x, y) -> zwhich we curry tox -> y -> z, and the handlers forLeft x | Right yarex -> zandy -> z. If there are no parameters, you can just take a valuezas your function rather than the more cumbersome() -> z. - Take all of those handlers as parameters to an expression
forall z. Handler1 -> Handler2 -> ... -> HandlerN -> z. - One half of the isomorphism is basically just to hand the constructors in as the desired handlers; the other pattern-matches on the constructors and applies the correponding handlers.
Subtle missing things
Again, it's fun to apply these rules to various things; for example as I noted above, if you apply this to data Unit = Unit you find that any unit type is the identity function forall z. z -> z, and if you apply this to data Bool = False | True you find the logic functions forall z. z -> z -> z where false = const while true = const id. But if you do play with it you will notice that something's missing still. Hint: if we look at
data List x = Nil | Cons x (List x)
we see that the pattern should look like:
data ListFn x = ListFn { runListFn :: forall z. z -> (x -> ??? -> z) -> z }
for some ???. The above rules don't pin down what goes there.
There are two good options: either we use the power of the newtype to its fullest to put ListFn x there (the "Scott" encoding), or we can preemptively reduce it with the functions we've been given, in which case it becomes a z using the functions that we already have (the "Church" encoding). Now since the recursion is already being performed for us up-front, the Church encoding is only perfectly equivalent for finite data structures; the Scott encoding can handle infinite lists and such. It can also be hard to understand how to encode mutual recursion in the Church form whereas the Scott form is usually a little more straightforward.
Anyway, the Church encoding is a little harder to think about, but a little more magical because we get to approach it with wishful thinking: "assume that this z is already whatever you're trying to accomplish with tail list, then combine it with head list in the appropriate way." And this wishful thinking is precisely why people have trouble understanding foldr, as the one side of this bijection is precisely the foldr of the list.
There are some other problems like "what if, like Int or Integer, the number of constructors is big or infinite?". The answer to this particular question is to use the functions
data IntFn = IntFn { runIntFn :: forall z. (z -> z) -> z -> z }
What is this, you ask? Well, a smart person (Church) has worked out that this is a way to represent integers as the repetition of composition:
zero f x = x
one f x = f x
two f x = f (f x)
{- ~ - increment an `n` to `n + 1` - ~ -}
succ n f = f . n f
Actually on this account m . n is the product of the two. But I mention this because it is not too hard to insert a () and flip arguments around to find that this is actually forall z. z -> (() -> z -> z) -> z which is the list type [()], with values given by length and addition given by ++ and multiplication given by >>.
For greater efficiency, you might Church-encode data PosNeg x = Neg x | Zero | Pos x and use the Church encoding (keeping it finite!) of [Bool] to form the Church encoding of PosNeg [Bool] where each [Bool] implicitly ends with an unstated True at its most-significant bit at the end, so that [Bool] represents the numbers from +1 to infinity.
An extended example: BinLeaf / BL
One more nontrivial example, we might think about the binary tree which stores all of its information in leaves, but also contains annotations on the internal nodes: data BinLeaf a x = Leaf x | Bin a (BinLeaf a x) (BinLeaf a x). Following the recipe for Church encoding we do:
newtype BL a x = BL { runBL :: forall z. (x -> z) -> (a -> z -> z -> z) -> z}
Now instead of Bin "Hello" (Leaf 3) (Bin "What's up?" (Leaf 4) (Leaf 5) we construct instances in lowercase:
BL $ \leaf bin -> bin "Hello" (leaf 3) (bin "What's up?" (leaf 4) (leaf 5)
The isomorphism is thus very easy one way: binleafFromBL f = runBL f Leaf Bin. The other side has a case dispatch, but is not too bad.
What about recursive algorithms on the recursive data? This is where it gets magical: foldr and runBL of Church encoding have both run whatever our functions were on the subtrees before we get to the trees themselves. Suppose for example that we want to emulate this function:
sumAnnotate :: (Num n) => BinLeaf a n -> BinLeaf (n, a) n
sumAnnotate (Leaf n) = Leaf n
sumAnnotate (Bin a x y) = Bin (getn x' + getn y', a) x' y'
where x' = sumAnnotate x
y' = sumAnnotate y
getn (Leaf n) = n
getn (Bin (n, _) _ _) = n
What do we have to do?
-- pseudo-constructors for BL a x.
makeLeaf :: x -> BL a x
makeLeaf x = BL $ \leaf _ -> leaf x
makeBin :: a -> BL a x -> BL a x -> BL a x
makeBin a l r = BL $ \leaf bin -> bin a (runBL l leaf bin) (runBL r leaf bin)
-- actual function
sumAnnotate' :: (Num n) => BL a n -> BL n n
sumAnnotate' f = runBL f makeLeaf (\a x y -> makeBin (getn x + getn y, a) x y) where
getn t = runBL t id (\n _ _ -> n)
We pass in a function \a x y -> ... :: (Num n) => a -> BL (n, a) n -> BL (n, a) n -> BL (n, a) n. Notice that the two "arguments" are of the same type as the "output" here. With Church encoding, we have to program as if we've already succeeded -- a discipline called "wishful thinking".
The Church encoding for the Free monad
The Free monad has normal form
data Free f x = Pure x | Roll f (Free f x)
and our Church encoding procedure says that this becomes:
newtype Fr f x = Fr {runFr :: forall z. (x -> z) -> (f z -> z) -> z}
Your function
matchFree p _ (Pure x) = p x
matchFree _ f (Free x) = f x
becomes simply
matchFree' p f fr = runFr fr p f
Your
matchF
:: Functor f
=> (a -> r)
-> (f (F f a) -> r)
-> F f a
-> r
looks like the Scott-encoded Free monad. The Church-encoded version is just
matchF
:: Functor f
=> (a -> r)
-> (f r -> r)
-> F f a
-> r
matchF kp kf f = runF f kp kf
Here are Church- and Scott-encoded lists for comparison:
newtype Church a = Church { runChurch :: forall r. (a -> r -> r) -> r -> r }
newtype Scott a = Scott { runScott :: forall r. (a -> Scott a -> r) -> r -> r }