Zippers: Derivatives of Regular Types

Explains the Zipper, which is a data structure that acts as a cursor of a purely functional data structure.

1. Zippers: Derivatives of Regular Types Jay Coskey 2017-02-18 (updated 2017-06-07) “But yeah, this stuff is a barrel of laughs. With a hole in it.” — Conor McBride, 2016-11-12 Copyright 2017, by Jay Coskey. License: CC-BY-SA .  

2. TL;DR A purely functional data structure (PFDS) can be edited efficiently by a using type of cursor that can be moved around the data structure, and always points to a "focus element". Such cursors are called Zippers. Gérard Huet's 1997 paper, "Functional Pearl: The Zipper", summarized a means of creating a purely functional version of a tree data structure with a built-in cursor that allows efficient updates. This was based on a technique called pointer reversal that dates to the 1960s. This pattern was extended by Conor McBride's paper "The Derivative of a Regular Type is its Type of One-Hole Contexts". (1)(2) This has sparked a great deal of research into the interpretation, application, and extension of these ideas, including higher-order derivatives of types, purely functional filesystems, etc. (1) McBride's much-cited paper was rejected from LICS 2001, among other reasons, for being short on explanation. (2) Though these are great papers, the last chapter of Learn You a Haskell might be a better introduction to zippers. 2

3. Early Zippers The history of the zipper goes back to 1851: "It will be seen that the clasps and cord being constructed and arranged as above described, the clasps can be moved freely up and down on the flanged ribs, bringing the said clasps near together and leaving the cord between the pairs of clasps loose or in a loop form, as shown in Figs. 2 and 3." — Elias Howe (an early expert on zippers and closures) U.S. Patent #8540; Nov 25, 1851. Zippers are commonly seen on garments, such as the coat worn by Arthur Fonzarelli. 3

4. 4 E x a m p l e s Z i p p e r

5. Introducing the "zipper-list" Copying a new list from an old one is, in general, O(n), because you have to "walk" the list. But if we only want to replace the head, it's O(1). We can easily take oldList = oldHead : oldTail and create newList = newHead : oldTail. Editing the inside of a list can be O(1) if it's arranged as two lists head-to-head, and the editing is only done where they meet. We'll call this element the "focus". By convention, let's choose the the right-hand list to be the "forward" one, and the other to be the "reversed" one, which records transactions or breadcrumbs to the full data structure list. We'll call this pair a "list-zipper". The list-zipper holds the same data as a list, but in a form that allows O(1) editing at the focus. 5 , ( ) "Forwards list" "Reversed list"

6. The "zipper-list" — some code data List a = Empty | Cons a (List a) deriving (Show, Read, Eq, Ord) The zipper for a list consists of two lists , with one reversed, as shown below. Head elements can be edited, or moved between the two lists for traversal. type ListZipper a = ([a], [a]) goLeft :: ListZipper a -> ListZipper a goLeft ( x : xs , ys ) = ( xs , x : ys ) goRight :: ListZipper a -> ListZipper a goRight ( xs , y : ys ) = ( y : xs , ys) pushRight :: ListZipper a -> a -> ListZipper a pushRight( xs , ys ) z = (xs, z : ys ) popRight :: ListZipper a -> ListZipper a popRight (xs, y : ys ) = ( xs , ys) replaceRight :: ListZipper a -> ListZipper a replaceRight(xs, y : ys) z = (xs, z : ys) xs (reversed) ys 6 We could choose to adopt the convention that the element in "focus" is the head of the right-hand list (here in blue).

7. What's the derivative of a List? A list-zipper consists of two lists, the first one reversed, as shown below. The focus element can be edited, or moved between the two lists for traversal. List a = Nil | Cons a (List a). We can write this algebraically as L(a) = 1 + a • L ( a), or as: List a = Nil | List1 a | List2 a a | List3 a a a | … = 1 + a + a 2 + a 3 + … = LZip( a) = L(a ) • L(a ) = L(a) 2 = = = L'(a) This list-zipper and the classical derivative of (the algebraic representation of) the list type are isomorphic. We call LZip(a) the " derivative " of L(a). Note: This type derivative should not be confused with numerical differentiation or automatic differentiation (AD).   7 xs (reversed) ys An ordered pair of lists, L(a) • L(a).

8. Trivial derivative examples: Maybe and Either Maybe data Maybe a = None | Just a M(a) = 1 + a M(a) = 1 Either data Either a b = Left a | Right b E(a, b) = a + b E(a, b) = E(a, b) = 1   8 These are one-element "collections", so they have end up having trivial cursors .

9. Back to Lists: the one-hole context Some sources write: LZip( a) = L(a ) • L( a) = "the context" while others write: LZip(a) = a • L(a) • L(a) This form splits the zipper into two parts that are easier to work with using formal methods. The "focus element" is on the left, while the "one-hole context " is on the right. Consider the case where we want to find the (type) derivative of a triplet. Triplet(a) = (a, a, a) = a 3 Triplet(a) = 1 • (◦, a, a) + 1 • (a, ◦, a) + 1 • (a, a, ◦) Triplet-Zipper(a) = 3 • a 2 // or (a, 3 • a 2 ), if ones chooses that convention   9 xs (reversed) ys xs (reversed) (Unit) ys ( ) , ( , , ) A "one-hole" context of a 3

10. What's the derivative of a Binary Tree? (1) Recall that List a = data BTree a = Empty | Node a (BTree a) (BTree a) = 1 + • T(a) 2 T'( a) = (a) = • T(a) 2 } = a • T(a) T'(a) } + 1 • T(a) 2 // Need to solve for T'(a) = { • T(a) 2 = L(2 • a • T(a)) • T(a) 2 Tree-Zipper a = TZip (LTree a) (RTree a) [ (Direction, a, BTree a) ] Functional data structures can be thought of as having a … context = part "below" the focus element + part "above" a focus element   10 Children of focus node List of steps from root to focus node. LTree a RTree a Part of tree "above" node Part of tree "below" node (the "path") (the "children" of the focus element)

11. What's the derivative of a Binary Tree? (2) Here are different (ad hoc) approaches, driven by reasoning about cursors. The Learn You a Haskell approach: data BTree a = Empty | Node a (BTree a) (BTree a) -- 1 + a • T(a) 2 data Crumb a = LeftCrumb a (BTree a) | RightCrumb a (BTree a) -- 2 • T(a) type Breadcrumbs a = [Crumb a] -- [2 • T(a)] type Zipper a = (Breadcrumbs a, BTree a) -- ( [2 • T(a)], T(a) ) The Simon Roßkopf approach ("Zippers and Data Type Derivatives") data Direction = L | R -- 2 type Location a = ([Direction], BTree a) -- ( [2], T(a) ) data AboveContext a = Top | LSubTree a (BTree a) (AboveContext a) | RSubTree a (BinaryTree a) (AboveContext a) data Context = Context (BTree a) (BTree a) (AboveContext a) -- Left child, right child, portion of tree above type Zipper a = (a, Context a) The Chris Taylor approach: data BTree a = Empty | Node a (BTree a) (BTree a) T(a) = 1 + a • T(a) 2 T(a, r ) = 1 + a • r 2 -- r = T(a) 2 is the recursive part of the tree = 2 • a • r = (BTDirection, a, BTree) ….   11

12. a … What's the derivative of a Rose Tree? Recall that L(a) = , and that L'(a) = L(a) 2 (**) Define a Rose tree as: data Rose a = Rose a [Rose a] Let R = Rose and L = [ ], then R(a) = a • L(R(a)) R'(a) = R(a) = • L(R(a)) } = a • L(R(a)) } + L(R(a)) -- Product rule = a • L'(R(a)) • R'(a) + L(R(a)) -- Chain rule = L(R(a)) • { -- Using (**) = L(R(a)) • L(a • L(R(a)) 2 ) = DRose [Rose a] [ (a, [Rose a], [Rose a]) ]   a a a a a a a … … a a a … a a … … … Children of selected node List of parent contexts (parent, left siblings , right siblings) Rose tree diagram 12 Alternate definition, by Ralf Hinze: data Rose' a = Branch' a (Forest a) data Forest a = NilF | ConsF (Rose' a) (Forest a)

13. When to zip? For regular data types! What are they? The regular types are explained in section 2 of Conor McBride's paper "The Derivative of a Regular Type is its Type of One-Hole Contexts", using sequent calculus. They are like algebraic data types, in that they include polynomials, where: "sum" is alternation (A  |  B, meaning A or B, but not both) "product" is combination (A B, meaning A and B together) This is denoted in sequent calculus by: Regular types also includes least fixed points. (See Data.Functor.Fixedpoint .) This can be used to find type derivatives. See, for example, "∂ for Data: Differentiating Data Structures, by Conor McBride", et. al., at http://strictlypositive.org/dfordata.pdf   13 Meaning: When the assertions above the line are true, the statement below the line are also true.

14. When not to zip: Nat & multi-dimensional arrays 14 The set of Natural numbers, Nat, is defined inductively. data Nat = Z | S Nat one = S Z, two = S one, three = S two, etc. At first it looks like a List, but it's different: Nat isn't a container of items of arbitrary type. List-Zippers rely on reversing the order of part of the value on one side of the focus element, but Nat has a fixed, inherent ordering. (This point can be made formal by using the fixed-point operator.) What about an n-dimensional array? Spoiler-alert: Zippers are cursors into purely functional data structures, and make use of the fact that there is a unique path to the focus element. But n-dimensional arrays have cycles. (Well, you could represent the grid as a multi-dimensional tree of sorts….)

15. Note: Zippers are not Lenses Functional programming has notions both of zippers and lenses. (*) Up = toward the head (as in Weak Head Normal Form), and Down is the opposite (**) Left/Right = among data at a fixed Up/Down level 15 Zippers Lenses Basically cursors Basically getters/setters Navigates by going Up/Down(*) and Left/Right (**) Access members directly, without a cursor

16. 16 A p p l i c a t i o n s Z i p p e r

17. An application: A Very Simple File System ( VSFS) (from Learn You a Haskell) We can (poorly) define a very simple filesystem as type Name = String type Data = ByteString data FSItem = File Name Data | Folder Name [FSItem] deriving (Show) What would be the zipper for this FSItem class? data FSCrumb = FSCrumb Name [FSItem] [FSItem] deriving (Show) type FSZipper = (FSItem, [FSCrumb]) Then fsUp :: FSZipper -> FSZipper fsUp (item, FSCrumb name ls rs : crumbs) = (Folder name (ls ++ [item] ++ rs), crumbs) Oleg Kiselyov has devised a related Zipper File System (ZFS). It uses a very different implementation approach (including ZipperM). 17

18. 18 Z i p p i e r Z i p p i e r &

19. Higher order derivatives (Not to be confused with Derivatives of Higher Order Types (HOTs)] 1. Derivative types are essentially purely functional, yet still "updateable" cursors into a data structure that provide O(1) mutation. 2. The derivative of a regular type is also a regular type, so the 2 nd derivative is well-defined. It can rerepsent O(1) splicing. ( See Higher Order Zippers , by Christophe Poucet.) 3. [Kiselyov] Zippers with several holes can represent multiple accessors into a data structure. If they are thought of as operating in parallel, then different variations can represent: At one extreme: serializable isolation At another extreme: no isolation, i.e., ANSI Read Uncommitted = "dirty read" isolation Zippers can support either or these, or modes inbetween (e.g., Committed Read, or Repeatable Read), or even subtransactions, using "push" or "pull" mode. See "Two-hole zippers and transactions of various isolation modes", by Oleg Kiselyov https://mail.haskell.org/pipermail/haskell/2005-May/015844.html 19

20. 20 I m p l e m e n t i o n Z i p p e r

21. The Haskell module Data.Generics.Uniplate.Zipper (@ haskell.org ) was inspired by the 2010 paper Scrap Your Zippers: A Generic Zipper for Heterogeneous Types, by Michael D. Adams. This approach: generalizes Huet's zipper to support non-heterogeneous types, and abstracts away the logic that's dependent on the type the zipper traverses. However, it adds the constraint that the types traversed be instances of a particular data class (see Data.Generics.Uniplate.Operations). 21 Implementing zippers the easy way

22. Implementing zippers with delimited continuations A completely different approach to cursors into immutable types was provided by Oleg Kiselyov. Rather than think of the derivative of a data type, think of derivatives in terms of traversal. Replace the zipper data structures discussed thus far with an isomorphic approach involving delimited continuations. Capture the "forward" traversal of the data structure by Continuation Passing Style (CPS) conversion. Then use "Reynolds defunctionalization" on that to make the control structure explicit as delimited continuations (per Danvy). Then use "refunctionalization" to get back to where you started. A snippet of Kiselyov's stack-trace-like code: data Zipper t a = ZDone (t a) | Z a (Maybe a -> Zipper t a) make_zipper :: T.Traversable t => t a -> Zipper t a make_zipper t = reset $ T.mapM f t >>= return . ZDone where f a = shift (\k -> return $ Z a (k . maybe a id)) 22

23. Implementing zippers the hard way One implementation approach actually derive the type of a zipper, based on the underlying type. This program written by Ralf Hinze and Johan Jeuring uses a customized build of the Haskell compiler called Generic Haskell (written by Andres Löh). A description of this endeavor can be found in the 56pp. paper ( PDF ) called The paper Generic Haskell: practice and theory , by Hinze and Jeuring. Note that this is not an example of dependent types, since the type of the zipper depends on the type — not the value — of the underlying type. 23

24. 24 O d d i t i e s Z i p p e r

25. Taylor series and the prestidigitation of types data BTree a = End a | Branch (BTree a) (BTree a) T = a + T 2 = a + (a + T 2 ) 2 = a + a 2 + 2aT 2 + T 4 = … = a + 1 a 2 + 2 a 3 + 5 a 4 + 14 a 5 + … In regular algebra, T = a + T 2  T 2 – T + a = 0  T = This is solved by the Taylor series T = a + 1 a 2 + 2 a 3 + 5 a 4 + 14 a 5 + …. The paper "Seven Trees in One", by Andreas Blass, has an example where one example of such power series type magic is made rigorous. Conor McBride points out in a comment here that ½ is not isomorphic to X 2 , since info on the ordering of pairs is lost. Beware of intuition! Moral: Be bold when using such analogies to draw inspiration, but cautious when determining what is actually works.   25 ( 1 … 2 … 5 …. ) Count of non-isomorphic trees by # values

26. Differential equations over types? In calculus, some differential are solved by using power series. Consider the power series Notice how the denominators are the number of permutations of a set? I have a hunch that the solution to the differential type equation T' a = T a could be construed as being Set a Can Set a be represented as a regular type? TODO: Is there a meaningful solution to T''(a) = -T(a) ? TODO: Can we take square roots of type derivatives? One guy named Paul Dirac once won a Nobel Prize basically for taking the square root of a differential operator! 26 f(x) ≈ f(0) + * x + * x 2 + * x 3 + …  

27. The Zipper Monad (by Dan Piponi) There is a monad hidden behind every zipper: http://blog.sigfpe.com/2007/01/monads-hidden-behind-every-zipper. html "The catch is that it's a monad in the wrong category, making it hard to express in Haskell." (and a comonad, too: http://cs.ioc.ee/~tarmo/tsem05/uustalu0812-slides.pdf , as a result of the strick-push-monad vs. lazy-pull-comonad dichotomy) 27

28. 28 R e s o u r c e s A d d i t i o n a l

29. Resources — Introduction to Zippers You Could Have Invented Zippers, by Edward Z. Yang (a good introduction to Zippers) http://blog.ezyang.com/2010/04/you-could-have-invented-zippers/ The chapter on Zippers from Learn You A Haskell, by Miran Lipovača (a more complicated intro) http://learnyouahaskell.com/zippers FUNCTIONAL PEARLS: The Zipper, by Gérard Huet (a paper that helped popularize Zippers) http://gallium.inria.fr/~huet/PUBLIC/zip.pdf Zippers, Derivatives -- Oh what fun!, by Travis Athougies (derives the Zipper for a Rose tree) http://travis.athougies.net/posts/2015-01-16-zippers-derivatives-oh-what-fun.html Zippers and Data Type Derivatives, by Simon Roßkopf https://www21.in.tum.de/teaching/fp/SS15/papers/11.pdf Zippers [parts 1 – 4], by Pavel Panchekha https://pavpanchekha.com/blog/zippers/huet.html The Algebra of Algebraic Data Types, by Chris Taylor http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of-algebraic-data-types/ Other Zipper-related wikis: https://en.wikibooks.org/wiki/Haskell/Zippers and https://wiki.haskell.org/Zipper 29

30. Resources — Papers by Conor McBride The Derivative of a Regular Type is its Type of One-Hole Contexts, by Conor McBride http://strictlypositive.org/diff.pdf (Generalized Huet's paper; helped popularize Zippers.) Here "regular" basically means built upon primitive types, and closed under sum, product, and (least) fixed points. ∂ for Data: Differentiating Data Structures, by Conor McBride, et. al. http://strictlypositive.org/dfordata.pdf (A formal approach, using sequent calculus) Clowns to the left of me, jokers to the right (Dissecting Data Structures), by Conor McBride, et. al. http://strictlypositive.org/Dissect.pdf (Another paper using a formal approach) 30

31. Resources — Implementations and Applications Implementations Scrap Your Zippers: A Generic Zipper for Heterogeneous Types, by Michael D. Adams https://michaeldadams.org/papers/scrap_your_zippers/ , and source code at https://michaeldadams.org/papers/scrap_your_zippers/ScrapYourZippers.hs "Generic Haskell: practice and theory", by Ralph Hinze and Johan Jeuring http://www.cs.uu.nl/research/techreps/repo/CS-2003/2003-015.pdf Create derivative types at runtime using a custom Haskell build. Also see Exploring Generic Haskell, a thesis by Andres Löh: https://www.andres-loeh.de/ExploringGH.pdf Several papers on implementing zippers as delimited continuations, by Oleg Kiselyov http://okmij.org/ftp/continuations/zipper.html Kiselyov's implementation treats derivatives not as data types, but as traversal functions using CPS (Continuation Passing Style). Hackage's implementation of zippers based on Kiselyov's traversal work https://hackage.haskell.org/package/zippers Applications xmonad: "The tiling window manager that rocks" http://xmonad.org/ Zipper-based file server/OS [ZFS] http://okmij.org/ftp/continuations/zipper.html#zipper-fs "A referentially transparent filesystem with transactional semantics in 540 lines of Haskell." Strengthening the Zipper, by Tristan Allwood and Susan Eisenbach https://www.doc.ic.ac.uk/~tora/clase/CLASE-Medium.pdf A zipper-based tool to traverse heterogeneous data types: specifically, Haskell expressions. 31

32. Resources — Higher Order Zippers Zippers & Taylor Series A Taylor Series for Types, by Dan Piponi http://blog.sigfpe.com/2006/06/taylor-series-for-types.html The denominator in Taylor's series can be interpreted as the number of permutations of a set. Note that X^2 is not isomorphic to 2*X^2/2, since info on ordering is lost. F[X + Y] = exp(Y d/dX) F[X] Seven Trees in One, by Andreas Blass https://arxiv.org/abs/math/9405205 Takes a bit of intuition gained from a Taylor series (that there is a bijection between the set of all seven-tuples of binary trees and the set of all trees) and formalizes it. More on Higher Order Zippers Higher Order Zippers, by Christophe Poucet http://blog.poucet.org/2007/07/higher-order-zippers/ This provides the intuition that second-order zippers provide O(1) splicing. Two-hole zippers and transactions of various isolation modules, by Oleg Kiselyov https://mail.haskell.org/pipermail/haskell/2005-May/015844.html Zippers with multiple holes can represent transactions run in parallel, including all the ISO standard isolation levels, and more. A blessed man's formula for holey containers, by Dan Piponi http://blog.sigfpe.com/2008/06/blessed-mans-formula-for-holey.html A 19th century priest/mathematician discovered a formula for the nth derivative of a composition of functions. 32

33. Resources — Lenses, Monads, and Regexes Zippers vs. Lenses Stackoverflow: Differences between lenses and zippers https://stackoverflow.com/questions/22094971/what-are-the-differences-between-lenses-and-zippers From Zipper to Lens https://www.schoolofhaskell.com/user/psygnisfive/from-zipper-to-lens Haskell libraries: Control.Lens.Zipper and Data.Lens.Zipper Zippers and monads The Monads Behind Every Zipper, by Dan Piponi http://blog.sigfpe.com/2007/01/monads-hidden-behind-every-zipper.html "Structured Computation on Trees or, What's Behind That Zipper? (A Comonad)" http://cs.ioc.ee/~tarmo/tsem05/uustalu0812-slides.pdf "The zipper datatype hides a comonad. This is exactly the comonad one needs to structure attribute evaluation". Functional Pearl: The Monad Zipper, by Tom Schrijvers and Bruno C. d. S. Oliveira http://ropas.snu.ac.kr/~bruno/papers/MonadZipper.pdf Use a zipper to help navigate a monad stack. Uses the monad transformer library Monatron (Jaskelioff 2008), which is now on Hackage. Regexes Derivatives of regular expressions (Old school: 1964) http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.98.4378 33

34. Extra Slides 34

35. What's the derivative of a Ternary Tree ? data TTree a = Empty | Node a (TTree a ) (TTree a) (TTree a) = 1 + a • T(a) 3 Let's take a look at the approach that uses the fixed point operator, μ . A tree can be defined as T = μ x.F X, yielding the zipper Z = List(F' T), where List X = μ Y.1 + X • Y, and F' is derived from F in some way. In the case of binary trees, F X = 1 + X 2 , and F' X = 2 • X. In the case of ternary trees, F X = 1 + X 3 , and F' X = 3 • X 2 . TODO: Derive the derivative using formal methods (fixed-point). 35

36. Summary Table ( TODO: Fill in table) 36 Haskell Algebraic Abstraction Derivative Notes data Void data Unit = Unit 1 data Bool = True | False 2 = 1 + 1 data Maybe a = Just a | Nothing a + 1 1 data Either a b = Left a | Right b a + b ∂(a + b) = ∂a + ∂b Sum rule data (a, b) = (a, b) a * b ∂(a, b) = ∂a*b + a*∂b Product rule F (G a) f ◦ g ∂f(g(a)) = ∂f| g(a) * ∂ g | a Chain rule a -> b b a ∂b a = (a, b a-1 ) ? data L a = Empty | Cons a (List a) μ x. 1 + L * x a 2 Data Nat = Zero | Succ Nat μ x. 1 + x N/A ? data BTree a = End | Node a (BT a) (BT a) μ x. 1 + x 2 data TTree = End | TT a …. μ x. 1 + x 3 data Rose a = Rose a [Rose a] μ x. [x] data Surreal = S [Surreal] [Surreal]

37. data Surreal = Surreal [Surreal] [Surreal ] -- From John H. Conway, to model 2-player games. Let's instead use Game m = G m [G m] [G m ] -- m = "move" Then G(m) = m • L(G(m)) 2 G'(m) = m • L(G(m)) 2 } + L(G(m)) 2 = m • 2 L(G(m)) } + L(G(m )) 2  Power rule = 2 m • L'(G(m)) G'(m) + L(G(m )) 2  Chain rule = 2 m • L(G(m)) 2 G'(m) + L(G(m )) 2  Previous result = L(G( m)) 2 {  Solve for G'(m) = L(G(m)) 2 L( )  Previous result = DG [G m] [G m] [ (leftRightChoice, m, (m, [ G m], [G m]), (m, [G m], [G m]) ) ] S' = DSurreal [Surreal] [Surreal] [ (leftRightChoice, Surreal, Surreal) ]   … … TODO: Derivatives of the Surreal Numbers? m m m … Diagram of 2-player Game tree Sweet merciful pancakes! What have we done?! … Children of selected node List of parent contexts 37 zero = S [ ] [ ] one = S zero [ ] negOne = S [ ] zero half = S [zero] [one] Q: Is there any easy method or identity to validate that a derivative type is correct? TODO: Validate via fixed-point methods that this is correct, and not problemmatic like D(Nat).