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 inup
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')
indown
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 typefa :: f a
and their contexts of typeDer g (f a)
; - form all
f
-extractions of each suchfa
, yielding values of typea
and their contexts of typeDer 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 pmSjoerd 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 pmjberryman:
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 pmconal:
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 pmconal:
Sjoerd: Wow — way simpler
tweak2
! I’ve edited the text and the library, adding your simplification. I also improved the definitions ofdown
, thanks to your remark about similarity withtweak2
.Thanks much!
29 July 2010, 7:42 pmaditya 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 amLucius 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 amBrent 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 amconal:
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 amConal Elliott » Blog Archive » Topless data:
[…] « Another angle on zippers “Everything is a function” in Haskell? […]
20 December 2010, 12:56 pmRobin 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 amconal:
Robin: does the remark following the type of
down
answer your question?For instance, if
4 September 2011, 11:42 amf = []
, thendown
yields a list of 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 and the reconstructed upper level). It’s not very simple at all!
4 September 2011, 4:15 pmconal:
Robin: I wasn’t suggesting that
5 September 2011, 8:24 pmleft
&right
are easy to implement. Rather that they might be unnecessary (pure speculation). Do you really wantleft
&right
instead of the list (or whatever functor element) of children?David Feuer:
It turns out that
3 September 2018, 1:53 pmHoley
is essentially the same asTraversable
. Using a bleeding-edgebifunctors
, you gettraverseBia :: (Traversable t, Biapplicative p) => (a -> p b c) -> t a -> p (t b) (t c)
. The implementation of that function is itself very shady: it takes advantage of structure implied byTraversable
that can’t be obtained directly from its methods. You can then apply a funny continuation-passing biapplicative Roman Cheplyaka came up with to get a functionholesIn :: Traversable t => t a -> t (a, a -> t a)
. See https://stackoverflow.com/a/49044894/1477667 for the full details. What this all means is that while it’s certainly much easier, and likely more efficient, to get holes from generics, it’s possible to get away with something weaker.David Feuer:
Sorry, I should have said weaker than
3 September 2018, 1:55 pmTraversable
, not the same.