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))

14 Comments

  1. 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?

  2. 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:

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

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

  3. 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

  4. conal:

    illissius wrote:

    Thanks, these were very interesting!

    :)

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

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

    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?

    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!

  5. 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!

  6. 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?

  7. 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

  8. 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. 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!

  10. Conal Elliott » Blog Archive » Topless data:

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

  11. 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?

  12. conal:

    Robin: does the remark following the type of down answer your question?

    Since down yields an f-collection of locations, we do not need sibling navigation functions (left & right).

    For instance, if f = [], then down yields a list of child zippers, which you can traverse as you like.

  13. 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 and the reconstructed upper level). It’s not very simple at all!

  14. conal:

    Robin: I wasn’t suggesting that left & right are easy to implement. Rather that they might be unnecessary (pure speculation). Do you really want left & right instead of the list (or whatever functor element) of children?

Leave a comment