Zap as the Machinery of Program Reduction

Last time around, we discussed duality and cofree comonads towards our quest in generating rich stories. I promised that comonads were the abstraction and machinery behind interpreters, but I have yet to prove that. Let’s do it today.

My Kingdom for a Functor🔗

Two posts ago, we created a “command functor” whose job it was to specify the specific commands possible in our DSL:

data StoryF a = Change Character ChangeType (ChangeResult -> a)
              | Interrupt (Story ()) (Story ()) a

type Story a = Free StoryF a

Recall, this should be understood as “a story is built out of primitives where characters can change, or where one story interrupted by another.” The polymorphic a is “the type of the next piece of the computation,” and so the conspicuous (ChangeResult -> a) argument to the Change data constructor is “the remainder of the computation will be given a ChangeResult” or perhaps more naturally, “the Change command returns a ChangeResult.”

So that’s one half of the puzzle. We can create programs in our DSL, but we can’t yet interpret them. We’ve derived Cofree from first principles, and I’ve promised you that once we have an appropriate cofree comonad, we can use it as an interpreter for our DSL. In the same way that we created StoryF to exist as a Functor over which Free would give us a Monad, we’re going to need to find a meaningful CoStoryF to act as a carrier over Cofree to give us a Comonad.

It’s tempting to dive right in and try our same old tried-and-true approach: dualize everything and go from there. Unfortunately, that doesn’t work (I tried it), so instead of leading ourselves down a path of madness, let’s slow down and think about what we’re actually trying to accomplish.

The function we’re actually trying to write is this:

interpret :: Story a -> CoStory b -> (a, b)

which is to say, a function that runs Story a programs through an interpreter with internal state b. While the program itself computes an a, in the case of our interpreter, it’s this internal state b that we’re actually interested in. When we get closer to actually using this machinery to generate stories, this b is going to be instantiated as necessary locations, interesting character quirks, and other things we’re trying to compute about our story.

While a carries information between program segments (on the DSL side of things), b carries information about program segments (on the interpretation side).

When Zap’s in Charge, Every Mission’s a Suicide Mission🔗

Due to free theorems from parametricity, it’s often easier to find implementations of general functions than it is for more specific ones. In light of this, we can view this desired interpret function as the special case of a more general one:

zap :: (a -> b -> c) -> f a -> g b -> c

Here, zap is understood to be a function where somehow the functors f and g “annihilate” one another, and allow us to run pure functions over top of them. Obviously this depends on our choice of f and g, so we will make a typeclass:

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
class Zap f g | f -> g, g -> f where
    zap :: (a -> b -> c) -> f a -> g b -> c

It’s safe to ignore the LANGUAGE pragmas and the | f -> g, g -> f syntax if you don’t know what’s going on with them; they’re just there to convince Haskell that the gnarly things we’re doing with the type are kosher. Things won’t compile without them, but the type signature of zap is really what we care about here.

If you’ve forgotten what we’re trying to do by this point, we’re still looking for a meaningful CoStoryF functor. Once we get that, we can make a Cofree CoStoryF, which will necessarily form a Comonad and we’ll finally be able to evaluate our programs. Carrying on.

As is usually the case with typeclasses, we can probably derive Zap f g inductively, by which I mean this: if we have a Zap StoryF CoStoryF, we can likely use it to derive Zap (Free StoryF) (Cofree CoStoryF). Following this line of reasoning, we’ll try to work backwards to see what CoStoryF might look like.

But where do we start? Well, in the same line of reasoning, we can probably get a Zap StoryF CoStoryF from a Zap over the constituent functors of StoryF. Recall its definition:

data StoryF a = Change Character ChangeType (ChangeResult -> a)
              | Interrupt (Story ()) (Story ()) a

The constituent functors here are kind of hidden, but if you stare at it, you’ll see we have a sum (between Change and Interrupt), a product (the parameters in each branch), and a function.

In functor form, we know these as Either x, (,) x and (->) x. This suggests we should start looking for instances of Zap between these functors. Since pairs make up most of StoryF, we’ll start there. With the wisdom of having done it already, I’ll suggest we look for a Zap ((,) x) ((->) x) instance¹.

If we expand this out, it means we’re looking for a function of type (a -> b -> c) -> (x, a) -> (x -> b) -> c. Given the signature, it’s actually pretty easy to work out:

instance Zap ((,) x) ((->) x) where
 -- zap :: (a -> b -> c) -> (x, a) -> (x -> b) -> c
    zap f (x, a) xtob = f a (xtob x)

It’s worth noticing that Zap f g is symmetric about f and g. We had to pick one to go first, but there is no semantic distinction between the positions. We can exploit this fact to derive Zap g f automatically: we can just flip our incoming function:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
instance {-# OVERLAPPABLE #-} Zap f g => Zap g f where
    zap f a b = zap (flip f) b a

Again, more magic syntax to convince Haskell that this is kosher. UndecidableInstances certainly sounds scary, but I promise that this is an OK use of it.

Searching for a Functor Clarity🔗

The construction of this Zap instance between pairs and functions is promising. If you’re curious about what sorcery is actually going on here, this magic comes directly from the adjunction between curry and uncurry. Since every term in our sum-type StoryF is made up of nothing but pairs and functions, and functions and pairs can annihilate one another, this suggests our CoStoryF should be a product-type where we swap all of our products with functions and vice-versa:

data CoStoryF b = CoStoryF
                { changeH    :: Character -> ChangeType -> (ChangeResult, b)
                , interruptH :: Story () -> Story () -> b
                }
type CoStory b = Cofree CoStoryF b

This actually makes a great deal of sense if you look at it for a minute or two. If a StoryF is one of any possible commands, a CoStoryF should be a collection of functions to handle any action that a StoryF is capable of throwing at it. A StoryF is a sum of arguments, while a CoStoryF is a product of functions taking those arguments.

Convinced that we’ve found the right data structure, we’ll write a Functor instance for it:

instance Functor CoStoryF where
    fmap f (CoStoryF c i) = CoStoryF
        (fmap (fmap (fmap f)) c)
        (fmap (fmap f) i)

Your first thought might be “what a disgusting mess of fmap”. And you’d be right. You can convince yourself that it’s right by remembering that each application of fmap moves you inside a function, or into the second piece of a pair. Alternatively, you can try compiling it, see that it type-checks, and move on with your life thinking no more about it.

Armed with the right data structure and a Functor instance it, we’ll go on to build our Zap StoryF CoStoryF. Remember that the pieces of our CoStoryF product are “handlers” of particular actions from our StoryF, and thus we’ll call these pieces h in the following snippet:

instance Zap StoryF CoStoryF where
    zap f (Change c ct k) (CoStoryF h _) =
        let (cr, b) = h c ct
            a       = k cr
         in f a b
    zap f (Interrupt x x' a) (CoStoryF _ h) = f a (h x x')

Gross and ugly, I know. What are we writing here, C? Instead, we can exploit our Zap instance from earlier to perform the computation in that let block for us:

-- much nicer version of our previous snippet
instance Zap StoryF CoStoryF where
    zap f (Change    c ct k) (CoStoryF h _) = zap f k (h c ct)
    zap f (Interrupt x x' k) (CoStoryF _ h) =     f k (h x x')

Much better.

I claim that this does what we want. But why does this work? Well we’re using the sum constructor from our StoryF type as an index into the related handler from the product of our CoStoryF.

To interpret a Change, for example, we compute a ChangeResult from our handler given the arguments from Change. We then take this resulting ChangeResult and pass it into the continuation (ChangeResult -> a) returned by Change. In effect, this instance of Zap has performed a single stage of reduction between our DSL and our interpreter.

The Cogs in the Machine🔗

Maybe you’re starting to see now why this Zap machinery is useful for running our program: it automatically interleaves the results from our interpretation into the bound values in our DSL. What we’ve built so far automatically connects a single step of the program with a single step of the interpretation; as you might expect, the Zap over Free and Cofree will take care of running the individual reductions sequentially until we’ve fully evaluated our program.

And so we need to find a derivation of Zap (Free f) (Cofree g). If you followed the last derivation, this one should be a piece of cake. If not, it’s worth staring at for a little while – grokking it definitely helped solidify in my mind how Free and Cofree are related.

instance Zap f g => Zap (Cofree f) (Free g) where
    zap f (Pure a)  (Cofree b _ ) = f a b
    zap f (Bind as) (Cofree _ bs) = zap (zap f) as bs

Notice that we’re doing the same trick here: using the sum constructor of our Free type to pick a particular piece out of the product of our Cofree type.

All that’s left now is to construct a particular interpreter : CoStory b, which we can zap against any story : Story a. That will be our focus for the next post, but in the meantime, we’ll convince ourselves that we’ve done something worthwhile here by implementing our desired interpret function from earlier:

interpret :: Story a -> CoStory b -> (a, b)
interpret = zap (,)

Oh. That was easy. Definitely a sign that we’re onto something here.

Until next time.