# 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:

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:

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:

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^{1}.

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:

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

Until next time.

Deriving the other two instances is informative for how this machinery actually works, and is left as an exercise to the reader.↩︎