## Another angle on zippers

The zipper is an efficient and elegant data structure for purely functional editing of tree-like data structures, first published by Gérard Huet. Zippers maintain a location of focus in a tree and support navigation operations (up, down, left, right) and editing (replace current focus).

The original zipper type and operations are customized for a single type, but it’s not hard to see how to adapt to other tree-like types, and hence to regular data types.
There have been many follow-up papers to *The Zipper*, including a polytypic version in the paper *Type-indexed data types*.

All of the zipper adaptations and generalizations I’ve seen so far maintain the original navigation interface. In this post, I propose an alternative interface that appears to significantly simplify matters. There are only two navigation functions instead of four, and each of the two is specified and implemented via a fairly simple one-liner.

I haven’t used this new zipper formulation in an application yet, so I do not know whether some usefulness has been lost in simplifying the interface.

The code in this blog post is taken from the Haskell library functor-combo and completes the `Holey`

type class introduced in *Differentiation of higher-order types*.

**Edits**:

- 2010-07-29: Removed some stray
`Just`

applications in`up`

definitions. (Thanks, illissius.) - 2010-07-29: Augmented my complicated definition of
`tweak2`

with a much simpler version from Sjoerd Visscher. - 2010-07-29: Replaced
`fmap (first (:ds'))`

with`(fmap.first) (:ds')`

in`down`

definitions. (Thanks, Sjoerd.)

### Extraction

The post *Differentiation of higher-order types* gave part of a type class for one-hole contexts (functor derivatives) and the filling of those contexts:

```
class Functor f ⇒ Holey f where
type Der f :: * → *
fillC :: Der f a → a → f a
```

The arguments of `fillC`

correspond roughly to the components of what Gérard Huet called a “location”, namely context and something to fill the context:

```
type Loc f a = (Der f a, a)
```

So an alternative hole-filling interface is

```
fill :: Holey f ⇒ Loc f a → f a
fill = uncurry fillC
```

Now consider a reverse operation, a kind of *extraction*:

```
guess1 :: f a → Loc f a
```

There’s an awkward problem here.
What if `f a`

has more than one possible hole, or has no hole at all?
If more than one, then which do we pick?
Perhaps the left-most.
If none, then we might want to have a failure representation, e.g.,

```
guess2 :: f a → Maybe (Loc f a)
```

To handle the more-than-one possibility, we could add another method for traversing the various extractions, like the `go_right`

operation in *The Zipper*, section 2.2.
I don’t know what changes we’d have to make to the `Loc`

type.

We could instead use a list of possible extractions.

```
guess3 :: f a → [Loc f a]
```

Why a *list*?
I guess because it’s in our habitual functional toolbox, and it covers any number of alternative extracted locations.
On the other hand, our toolbox is growing, and sometimes list isn’t the best functor for the job.
For instance, we might use a finger tree, which has better performance for some sequence operations.

Or we could a functor closer at hand, namely `f`

itself.

```
class Functor f ⇒ Holey f where
type Der f :: * → *
fillC :: Der f a → a → f a
extract :: f a → f (Loc f a)
```

For instance, when `f ≡ []`

, `extract`

returns a list of extractions; and when `f ≡ Id :*: Id`

, `extract`

returns a pair of extractions.

### How to extract

A constant functor has void derivative. Extraction yields another constant structure, with the same data but a different type:

```
instance Holey (Const x) where
type Der (Const x) = Void
fillC = voidF
extract (Const x) = Const x
```

The identity functor has exactly one opportunity for a hole, leaving no information behind:

```
instance Holey Id where
type Der Id = Unit
fillC (Const ()) = Id
extract (Id a) = Id (Const (), a)
```

The definitions of `Der`

and `fillC`

above and below are lifted directly from *Differentiation of higher-order types*.

For sums, there are two cases: `InL fa, InR ga :: (f :+: g) a`

.
Starting with the first case:

```
InL fa :: (f :+: g) a
fa :: f a
extract fa :: f (Loc f a)
:: f (Der f a, a)
(fmap.first) InL (extract fa) :: f ((Der f :+: Der g) a, a)
:: f ((Der (f :+: g) a), a)
```

See *Semantic editor combinators* for an explanation of `(fmap.first)`

friends.
Continuing, apply the definition of `Der`

on sums:

```
InL ((fmap.first) InL (extract fa)) :: (f :+: g) ((Der (f :+: g) a), a)
:: (f :+: g) (Loc (f :+: g) a)
```

The two steps that introduce `g`

are motivated by the required type of `extract`

.
Similarly, for the second case:

```
InR ((fmap.first) InR (extract ga)) :: (f :+: g) (Loc (f :+: g) a)
```

So,

```
instance (Holey f, Holey g) ⇒ Holey (f :+: g) where
type Der (f :+: g) = Der f :+: Der g
fillC (InL df) = InL ∘ fillC df
fillC (InR df) = InR ∘ fillC df
extract (InL fa) = InL ((fmap.first) InL (extract fa))
extract (InR ga) = InR ((fmap.first) InR (extract ga))
```

For products, recall the derivative type:

```
type Der (f :*: g) = Der f :*: g :+: f :*: Der g
```

To extract from a product, we extract from either component and then pair with the other component.
The form of an argument to `extract`

is

```
fa :*: ga :: (f :*: g) a
```

Again, start with the left part:

```
fa :: f a
extract fa :: f (Loc f a)
:: f (Der f a, a)
(fmap.first) (:*: ga) (extract fa) :: f ((Der f :*: g) a, a)
(fmap.first) (InL ∘ (:*: ga)) (extract fa)
:: f (((Der f :*: g) :+: (f :*: Der g)) a, a)
:: f ((Der (f :*: g)) a, a)
```

Similarly, for the second component,

```
(fmap.first) (InR ∘ (fa :*:)) (extract ga)
:: g ((Der (f :*: g)) a, a)
```

Combining the two extraction routes:

```
(fmap.first) (InL ∘ (:*: ga)) (extract fa) :*:
(fmap.first) (InR ∘ (fa :*:)) (extract ga)
:: (f :*: g) (Der (f :*: g) a, a)
```

So,

```
instance (Holey f, Holey g) ⇒ Holey (f :*: g) where
type Der (f :*: g) = Der f :*: g :+: f :*: Der g
fillC (InL (dfa :*: ga)) = (:*: ga) ∘ fillC dfa
fillC (InR ( fa :*: dga)) = (fa :*:) ∘ fillC dga
extract (fa :*: ga) =
(fmap.first) (InL ∘ (:*: ga)) (extract fa) :*:
(fmap.first) (InR ∘ (fa :*:)) (extract ga)
```

Finally, the chain rule, for functor composition:

```
type Der (g :. f) = Der g :. f :*: Der f
```

A value of type `(g :. f) a`

has form `O gfa`

, where `gfa :: g (f a)`

.
To extract:

- form all
`g`

-extractions, yielding values of type`fa :: f a`

and their contexts of type`Der g (f a)`

; - form all
`f`

-extractions of each such`fa`

, yielding values of type`a`

and their contexts of type`Der f a`

; and - reassemble these pieces into the shape determined by
`Der (g :. f)`

.

Let’s go:

```
gfa :: g (f a)
extract gfa :: g (Loc g (f a))
:: g (Der g (f a), f a)
fmap (second extract) (extract gfa)
:: g (Der g (f a), f (Loc f a))
```

Continuing, the following lemmas come in handy.

```
tweak2 :: Functor f ⇒
(dg (f a), f (df a, a)) → f (((dg :. f) :*: df) a, a)
tweak2 = (fmap.first) chainRule ∘ tweak1
tweak1 :: Functor f ⇒
(dg (fa), f (dfa, a)) → f ((dg (fa), dfa), a)
tweak1 = fmap lassoc ∘ squishP
squishP :: Functor f ⇒ (a, f b) → f (a,b)
squishP (a,fb) = fmap (a,) fb
chainRule :: (dg (f a), df a) → ((dg :. f) :*: df) a
chainRule (dgfa, dfa) = O dgfa :*: dfa
lassoc :: (p,(q,r)) → ((p,q),r)
lassoc (p,(q,r)) = ((p,q),r)
```

*Edit:* Sjoerd Visscher found a much simpler form to replace the previous group of definitions:

```
tweak2 (dgfa, fl) = (fmap.first) (O dgfa :*:) fl
```

More specifically,

```
tweak2 :: Functor f => (Der g (f a), f (Loc f a))
-> f (((Der g :. f) :*: Der f) a, a)
:: Functor f => (Der g (f a), f (Loc f a))
-> f (Der (g :. f) a, a)
:: Functor f => (Der g (f a), f (Loc f a))
-> f (Loc (g :. f) a)
```

This lemma gives just what we need to tweak the inner extraction:

```
fmap (tweak2 ∘ second extract) (extract gfa) :: g (f (Loc (g :. f) a))
```

So

```
extractGF :: (Holey f, Holey g) ⇒
g (f a) → g (f (Loc (g :. f) a))
extractGF = fmap (tweak2 ∘ second extract) ∘ extract
```

and

```
instance (Holey f, Holey g) ⇒ Holey (g :. f) where
type Der (g :. f) = Der g :. f :*: Der f
fillC (O dgfa :*: dfa) = O ∘ fillC dgfa ∘ fillC dfa
extract = inO extractGF
```

where `inO`

is from Control.Compose, and is defined using the ideas from *Prettier functions for wrapping and wrapping* and the notational improvement from Matt Hellige’s *Pointless fun*.

```
-- | Apply a unary function within the 'O' constructor.
inO :: (g (f a) → g' (f' a')) → ((g :. f) a → (g' :. f') a')
inO = unO ~> O
infixr 1 ~>
-- | Add pre- and post processing
(~>) :: (a' → a) → (b → b') → ((a → b) → (a' → b'))
(f ~> h) g = h ∘ g ∘ f
```

In case you’re wondering, these definitions did not come to me effortlessly.
I sweated through the derivation, guided always by my intuition and the necessary types, as determined by the shape of `Der (g :. f)`

.
The type-checker helped me get from one step to the next.

I do a lot of type-directed derivations of this style while I program in Haskell, with the type-checker checking each step for me.
I’d love to have mechanized help in *creating* these derivations, not just *checking* them.

### Zippers

How does the `Holey`

class relate to zippers?
As in a few recent blog posts, let’s use the fact that regular data types are isomorphic to fixed-points of functors.

Functor fixed-points are like function fixed points

```
fix f = f (fix f)
type Fix f = f (Fix f)
```

However, Haskell doesn’t support recursive type synonyms, so use a `newtype`

:

```
newtype Fix f = Fix { unFix :: f (Fix f) }
```

A context for a functor fixed-point is either empty, if we’re at the very top of an “`f`

-tree”, or it’s an `f`

-context for `f (Fix f)`

, and a parent context:

```
data Context f = TopC | Context (Der f (Fix f)) (Context f) -- first try
```

Hm.
On the outside, `Context f`

looks like a list, so let’s use a list instead:

```
type Context f = [Der f (Fix f)]
```

The location type we used above is

```
type Loc f a = (Der f a, a)
```

Similarly, define a type of zippers (also called “locations”) for functor fixed-points:

```
type Zipper f = (Context f, Fix f)
```

This `Zipper`

type corresponds to a zipper, and has operations `up`

and `down`

.
The `down`

motion can yield multiple results.

```
up :: Holey f ⇒ Zipper f → Zipper f
down :: Holey f ⇒ Zipper f → f (Zipper f)
```

Since `down`

yields an `f`

-collection of locations, we do not need sibling navigation functions (`left`

& `right`

).

To move up in `Zipper`

, strip off a derivative (one-hole functor context) and fill the hole with the current tree, leaving the other derivatives as the remaining fixed-point context.
Like so:

```
up :: Holey f ⇒ Zipper f → Zipper f
up (d:ds', t) = (ds', Fix (fill (d,t)))
```

To see how the typing works out:

```
(d:ds', t) :: Zipper f
(d:ds', t) :: (Context f, Fix f)
d:ds' :: [Der f (Fix f)]
t :: Fix f
d :: Der f (Fix f)
ds' :: [Der f (Fix f)]
fill :: Loc f b → f b
fill :: (Der f b, b) → f b
fill :: (Der f (Fix f), Fix f) → f (Fix f)
fill (d,t) :: f (Fix f)
Fix (fill (d,t)) :: Fix f
(ds', Fix (fill (d,t))) :: (Context f, Fix f)
:: Zipper f
```

Note that the `up`

motion fails when at the top of a zipper (empty context).
If desired, we can also provide an unfailing version (really, a version with explictly typed failure):

```
up' :: Holey f => Zipper f -> Maybe (Zipper f)
up' ([] , _) = Nothing
up' l = Just (up l)
```

To move down in an `f`

-tree `t`

, form the extractions of `t`

, each of which has a derivative and a sub-tree.
The derivative becomes part of an extended fixed-point context, and the sub-tree becomes the new sub-tree of focus.

```
down :: Holey f ⇒ Zipper f → f (Zipper f)
down (ds', t) = (fmap.first) (:ds') (extract (unFix t)) (unFix t))
```

The typing (in case you’re curious):

```
(ds',t) :: Zipper f
:: (Context f, Fix f)
:: ([Der f (Fix f)], Fix f)
ds' :: [Der f (Fix f)]
t :: Fix f
unFix t :: f (Fix f)
extract (unFix t) :: f (Der f (Fix f), Fix f)
(fmap.first) (:ds') (extract (unFix t))
:: ([Der f (Fix f)], Fix f)
:: (Context f, Fix f)
:: LocFix f
```

### Zipping back to regular data types

I like the (functor) fixed-point perspective on regular data types, for its austere formal simplicity. It shows me the naked essence of regular data types, so I can more easily see and more deeply understand patterns like memoization, derivatives, and zippers.

For convenience and friendliness of *use*, I prefer working with regular types directly, rather than through the (nearly) isomorphic form of functor fixed-points.
While the fixed-point perspective is formalism-friendly, the *pattern functor* perspective is more user-friendly, allowing us to work with our familiar regular data as they are.

As in *Elegant memoization with higher-order types*, let’s use the following class:

```
class Functor (PF t) ⇒ Regular t where
type PF t :: * → *
wrap :: PF t t → t
unwrap :: t → PF t t
```

The idea is that a type `t`

is isomorphic to `Fix (PF t)`

, although really there may be more points of undefinedness in the fixed-point representation, so rather than an isomorphism, we have an embedding/projection pair.

The notions of context and location are similar to the ones above:

```
type Context t = [Der (PF t) t]
type Zipper t = (Context t, t)
```

So are the `up`

and `down`

motions, in which `wrap`

and `unwrap`

replace `Fix`

and `unFix`

:

```
up :: (Regular t, Holey (PF t)) ⇒ Zipper t → Zipper t
down :: (Regular t, Holey (PF t)) ⇒ Zipper t → PF t (Zipper t)
up (d:ds', t) = (ds', wrap (fill (d,t)))
down (ds', t) = (fmap.first) (:ds') (extract (unwrap t))
```

## illissius:

Thanks, these were very interesting!

(You have a ‘Just’ in the definition of plain ‘up’, I assume that’s a mistake?)

I noticed that fmap fill . extract :: f a -> f (f a), which is the same type as duplicate from Comonad – does this have any significance?

29 July 2010, 12:18 pm## Sjoerd Visscher:

Great stuff!

At first it was a bit disappointing that extract is so complicated for functor composition, but I played a bit with the code and tweak2 can be simplified (if I didn’t make a mistake) to:

It’s interesting that (tweak2 . second extract) is very much like down! Probably because Fix f is like repeated functor composition of f.

29 July 2010, 2:38 pm## jberryman:

Hi Conal,

I’m still trying to process your post, and will probably need to catch up on the previous posts you mention, but I wonder if you caught a haskell-cafe message I sent a few days ago and if you had any thoughts:

http://www.haskell.org/pipermail/haskell-cafe/2010-July/080961.html

Your approach seems similar at first skim to what I had been playing around with, but as I said I’m still trying to grok all of it.

Brandon

29 July 2010, 6:27 pm## conal:

illissius wrote:

Yes it was. I made a late change to the library code and didn’t fix the post accordingly. Fixed now.

Wow. I hadn’t noticed. I’ll play around some more. Tugging at such patterns has led me to fruitful connections in the past.

Thanks!

29 July 2010, 6:42 pm## conal:

Sjoerd: Wow — way simpler

`tweak2`

! I’ve edited the text and the library, adding your simplification. I also improved the definitions of`down`

, thanks to your remark about similarity with`tweak2`

.Thanks much!

29 July 2010, 7:42 pm## aditya mahajan:

This is really interesting (although I do not understand everything). Can the above formulation work for directed acyclic graphs, where multiple paths can lead to the same node?

30 July 2010, 7:29 am## Lucius Meredith:

Hey Conal,

Interesting. i don’t know if you’ve seen my postings about using the notion of location as the notion of name. i gave a couple of write ups on my blog. If we use ∂µMxµM as the notion of location for a datatype given by functor M, then when M is secretly a bi-functor in which the other parameter is supplied by nominal structure, then we get solvable domain equations by setting the nominal parameter to be the derived notion of location. For example, the (syntax of the) λ-calculus (with an explicit term for divergence) is given by the bi-functor

M[V,A] = 1 + V + VxA + AxA

If we hold V fixed and calculate ∂µMxµM with respect to A, then we can set V = ∂µMxµM and get a solvable domain equation. The Haskell code for this structure is on my blog post. Now, what i haven’t talked about, yet, is that we get a notion of inner product coming from these equations. Roughly, if names are “scalars”, then intuition suggests terms ought to be vectors. So, then what should be dual to a vector? It needs to be a structure, say, k, such that when “dotted” with a term yields a scalar. Well, since we have set names to be pairs, (k,t), of contexts and terms, then we have the obvious operations k.t := (k,t). At this juncture there are several design choices. You can generalize the notion of inner product space by replacing the role of field with the algebra names inherit from the term algebra, and then show that you can recover a real inner product with encodings of arithmetic in terms of the term algebra, or you can begin with the encodings of the field operations in terms of the term algebra and pepper these through your definitions.

Best wishes,

–greg

30 July 2010, 9:54 am## Brent Yorgey:

Very nice. I like how this formulation removes the leftward bias inherent in the original version of “down”. It also works for functors where there is no inherent ordering that can be placed on the children (I’m thinking here of things like general combinatorial species/quotient containers).

Also, a little while ago Conor McBride wrote a nice message to the libraries mailing list with the same version of down, as well as discard :: Loc f a -> a and decorate :: Loc f a -> Loc f (Loc f a) which make Loc f a comonad. decorate in particular gives a notion of “moving sideways” without having to go up and then back down.

9 August 2010, 6:45 am## conal:

Brent: Thanks for the pointer to Conor’s message. I guess I’d better follow the Haskell lists more closely. I like the Comonad connection!

9 August 2010, 7:37 am## Conal Elliott » Blog Archive » Topless data:

[…] « Another angle on zippers “Everything is a function” in Haskell? […]

20 December 2010, 12:56 pm## Robin Green:

I’ve been trying to implement this in OCaml, and I kept thinking “How are left and right going to be implemented?” Now that I’ve come to implement them, I still don’t get it. You say that the interface is simpler because it doesn’t have left and right – but in order for that argument to hold, it must be simple to move left and right. How do you do it?

4 September 2011, 4:30 am## conal:

Robin: does the remark following the type of

`down`

answer your question?For instance, if

4 September 2011, 11:42 am`f = []`

, then`down`

yields alistof child zippers, which you can traverse as you like.## Robin Green:

I figured it out. It’s necessary to go up, then down, then do a case split on all the possibilities (looking at both the derivative

4 September 2011, 4:15 pmandthe reconstructed upper level). It’s not very simple at all!## conal:

Robin: I wasn’t suggesting that

5 September 2011, 8:24 pm`left`

&`right`

are easy to implement. Rather that they might be unnecessary (pure speculation). Do youreallywant`left`

&`right`

instead of the list (or whatever functor element) of children?