Conor McBride conor at strictlypositive.org
Tue May 22 15:52:09 CEST 2012

```Hi Mathijs

On 22 May 2012, at 07:42, Mathijs Kwik wrote:

> Hi all,
>
> After using zippers for a while, I wanted to dig a bit deeper into them.
> I found there is some relation between Zipper and Comonad, but this
> confuses me somewhat.
>
> understand them somewhat, and I see how they too are useful for
> navigating a data structures and giving functions the ability to "look
> around".
>
> What confuses me though, is the relation between these 2.
> This source [3] mentions all zippers can be made instances of Comonad,
> and demonstrates how to do this for simple, 1-dimensional (list)
> zippers.
> But a comment on [4] says a Zipper by itself is already an application
> I want to find out which is the case. Looking at the types does not
> yield me a solution yet.

[..]

Once upon a time, I wrote this message:

which may serve as grist to your mill.

The key points

(1) Inductive datatypes can usually be seen as instances of

data Mu f = In (f (Mu f))

where f is a Functor explaining the structure of one node, with the
parameter of f standing for the node's children. See how Mu f
instantiates f's parameter with Mu f, meaning that the children are
recursive subobjects?

(2) The derivative f' of such an f characterizes "f-structures with
one element missing", so a one-hole context in a Mu f is given by
the type [f' (Mu f)], being a series of nodes, each of which has
one child missing, but whose other children are still intact. The
whole zipper is given by ([f' (Mu f)], Mu f)

(3) The construction Focusf x = (f' x, x), representing an f-node
with one child held separately, is always comonadic. The counit
gives the separated child, discarding the context. The cojoin
decorates each element with its own context, showing the decompositions
you could get by "moving the cursor".

Sorry to be so brief and example-free -- terrible hurry

Conor

```