Given any container type we can form the (element-focused) Zipper and know that this structure is a Comonad. This was recently explored in wonderful detail in another Stack Overflow question for the following type:
data Bin a = Branch (Bin a) a (Bin a) | Leaf a deriving Functor
with the following zipper
data Dir = L | R
data Step a = Step a Dir (Bin a) deriving Functor
data Zip a = Zip [Step a] (Bin a) deriving Functor
instance Comonad Zip where ...
It is the case that Zip
is a Comonad
though the construction of its instance is a little hairy. That said, Zip
can be completely mechanically derived from Tree
and (I believe) any type derived this way is automatically a Comonad
, so I feel it ought to be the case that we can construct these types and their comonads generically and automatically.
One method for achieving generality for zipper construction is the use the following class and type family
data Zipper t a = Zipper { diff :: D t a, here :: a }
deriving instance Diff t => Functor (Zipper t)
class (Functor t, Functor (D t)) => Diff t where
data D t :: * -> *
inTo :: t a -> t (Zipper t a)
outOf :: Zipper t a -> t a
which has (more or less) shown up in Haskell Cafe threads and on Conal Elliott's blog. This class can be instantiated for the various core algebraic types and thus provides a general framework for talking about the derivatives of ADTs.
So, ultimately, my question is whether or not we can write
instance Diff t => Comonad (Zipper t) where ...
which could be used to subsume the specific Comonad instance described above:
instance Diff Bin where
data D Bin a = DBin { context :: [Step a], descend :: Maybe (Bin a, Bin a) }
...
Unfortunately, I've had no luck writing such an instance. Is the inTo
/outOf
signature sufficient? Is there something else needed to constrain the types? Is this instance even possible?
Like the childcatcher in Chitty-Chitty-Bang-Bang luring kids into captivity with sweets and toys, recruiters to undergraduate Physics like to fool about with soap bubbles and boomerangs, but when the door clangs shut, it's "Right, children, time to learn about partial differentiation!". Me too. Don't say I didn't warn you.
Here's another warning: the following code needs
{-# LANGUAGE KitchenSink #-}
, or ratherin no particular order.
Differentiable functors give comonadic zippers
What is a differentiable functor, anyway?
It's a functor which has a derivative, which is also a functor. The derivative represents a one-hole context for an element. The zipper type
ZF f x
represents the pair of a one-hole context and the element in the hole.The operations for
Diff1
describe the kinds of navigation we can do on zippers (without any notion of "leftward" and "rightward", for which see my Clowns and Jokers paper). We can go "upward", reassembling the structure by plugging the element in its hole. We can go "downward", finding every way to visit an element in a give structure: we decorate every element with its context. We can go "around", taking an existing zipper and decorating each element with its context, so we find all the ways to refocus (and how to keep our current focus).Now, the type of
aroundF
might remind some of you ofand you're right to be reminded! We have, with a hop and a skip,
and we insist that
We also need that
Polynomial functors are differentiable
Constant functors are differentiable.
There's nowhere to put an element, so it's impossible to form a context. There's nowhere to go
upF
ordownF
from, and we easily find all none of the ways to godownF
.The identity functor is differentiable.
There's one element in a trivial context,
downF
finds it,upF
repacks it, andaroundF
can only stay put.Sum preserves differentiability.
The other bits and pieces are a bit more of a handful. To go
downF
, we must godownF
inside the tagged component, then fix up the resulting zippers to show the tag in the context.To go
aroundF
, we strip the tag, figure out how to go around the untagged thing, then restore the tag in all the resulting zippers. The element in focus,x
, is replaced by its entire zipper,z
.Note that I had to use
ScopedTypeVariables
to disambiguate the recursive calls toaroundF
. As a type function,DF
is not injective, so the fact thatf' :: D f x
is not enough to forcef' :<-: x :: Z f x
.Product preserves differentiability.
To focus on an element in a pair, you either focus on the left and leave the right alone, or vice versa. Leibniz's famous product rule corresponds to a simple spatial intuition!
Now,
downF
works similarly to the way it did for sums, except that we have to fix up the zipper context not only with a tag (to show which way we went) but also with the untouched other component.But
aroundF
is a massive bag of laughs. Whichever side we are currently visiting, we have two choices:aroundF
on that side.upF
out of that side anddownF
into the other side.Each case requires us to make use of the operations for the substructure, then fix up contexts.
Phew! The polynomials are all differentiable, and thus give us comonads.
Hmm. It's all a bit abstract. So I added
deriving Show
everywhere I could, and threw inwhich allowed the following interaction (tidied up by hand)
Exercise Show that the composition of differentiable functors is differentiable, using the chain rule.
Sweet! Can we go home now? Of course not. We haven't differentiated any recursive structures yet.
Making recursive functors from bifunctors
A
Bifunctor
, as the existing literature on datatype generic programming (see work by Patrik Jansson and Johan Jeuring, or excellent lecture notes by Jeremy Gibbons) explains at length is a type constructor with two parameters, corresponding to two sorts of substructure. We should be able to "map" both.We can use
Bifunctor
s to give the node structure of recursive containers. Each node has subnodes and elements. These can just be the two sorts of substructure.See? We "tie the recursive knot" in
b
's first argument, and keep the parametery
in its second. Accordingly, we obtain once for allTo use this, we'll need a kit of
Bifunctor
instances.The Bifunctor Kit
Constants are bifunctorial.
You can tell I wrote this bit first, because the identifiers are shorter, but that's good because the code is longer.
Variables are bifunctorial.
We need the bifunctors corresponding to one parameter or the other, so I made a datatype to distinguish them, then defined a suitable GADT.
That makes
V X x y
a copy ofx
andV Y x y
a copy ofy
. AccordinglySums and Products of bifunctors are bifunctors
So far, so boilerplate, but now we can define things like
If you want to use these types for actual data and not go blind in the pointilliste tradition of Georges Seurat, use pattern synonyms.
But what of zippers? How shall we show that
Mu b
is differentiable? We shall need to show thatb
is differentiable in both variables. Clang! It's time to learn about partial differentiation.Partial derivatives of bifunctors
Because we have two variables, we shall need to be able to talk about them collectively sometimes and individually at other times. We shall need the singleton family:
Now we can say what it means for a Bifunctor to have partial derivatives at each variable, and give the corresponding notion of zipper.
This
D
operation needs to know which variable to target. The corresponding zipperZ b v
tells us which variablev
must be in focus. When we "decorate with context", we have to decoratex
-elements withX
-contexts andy
-elements withY
-contexts. But otherwise, it's the same story.We have two remaining tasks: firstly, to show that our bifunctor kit is differentiable; secondly, to show that
Diff2 b
allows us to establishDiff1 (Mu b)
.Differentiating the Bifunctor kit
I'm afraid this bit is fiddly rather than edifying. Feel free to skip along.
The constants are as before.
On this occasion, life is too short to develop the theory of the type level Kronecker-delta, so I just treated the variables separately.
For the structural cases, I found it useful to introduce a helper allowing me to treat variables uniformly.
I then built gadgets to facilitate the kind of "retagging" we need for
down
andaround
. (Of course, I saw which gadgets I needed as I was working.)And with that lot ready to go, we can grind out the details. Sums are easy.
Products are hard work, which is why I'm a mathematician rather than an engineer.
Conceptually, it's just as before, but with more bureaucracy. I built these using pre-type-hole technology, using
undefined
as a stub in places I wasn't ready to work, and introducing a deliberate type error in the one place (at any given time) where I wanted a useful hint from the typechecker. You too can have the typechecking as videogame experience, even in Haskell.Subnode zippers for recursive containers
The partial derivative of
b
with respect toX
tells us how to find a subnode one step inside a node, so we get the conventional notion of zipper.We can zoom all the way up to the root by repeated plugging in
X
positions.But we need element-zippers.
Element-zippers for fixpoints of bifunctors
Each element is somewhere inside a node. That node is sitting under a stack of
X
-derivatives. But the position of the element in that node is given by aY
-derivative. We getBoldly, I claim
but before I develop the operations, I'll need some bits and pieces.
I can trade data between functor-zippers and bifunctor-zippers as follows:
That's enough to let me define:
That is, we go up by first reassembling the node where the element is, turning an element-zipper into a subnode-zipper, then zooming all the way out, as above.
Next, I say
to go down starting with the empty stack, and define the helper function which goes
down
repeatedly from below any stack:Now,
down b
only takes us inside the node. The zippers we need must also carry the node's context. That's whatcontextualise
does:For every
Y
-position, we must give an element-zipper, so it is good we know the whole contextdXs
back to the root, as well as thedY
which describes how the element sits in its node. For everyX
-position, there is a further subtree to explore, so we grow the stack and keep going!That leaves only the business of shifting focus. We might stay put, or go down from where we are, or go up, or go up and then down some other path. Here goes.
As ever, the existing element is replaced by its entire zipper. For the
belowY
part, we look where else we can go in the existing node: we will find either alternative elementY
-positions or furtherX
-subnodes to explore, so wecontextualise
them. For theaboveY
part, we must work our way back up the stack ofX
-derivatives after reassembling the node we were visiting.At each step of the way, we can either turn somewhere else that's
around
, or keep going up.And that's it! I haven't given a formal proof of the laws, but it looks to me as if the operations carefully maintain the context correctly as they crawl the structure.
What have we learned?
Differentiability induces notions of thing-in-its-context, inducing a comonadic structure where
extract
gives you the thing andduplicate
explores the context looking for other things to contextualise. If we have the appropriate differential structure for nodes, we can develop differential structure for whole trees.Oh, and treating each individual arity of type constructor separately is blatantly horrendous. The better way is to work with functors between indexed sets
where we make
o
different sorts of structure storingi
different sorts of element. These are closed under the Jacobian constructionwhere each of the resulting
(o, i)
-structures is a partial derivative, telling you how to make ani
-element-hole in ano
-structure. But that's dependently typed fun, for another time.