Zippity doo daa

January 13th, 2006 by Graham

The zipper is a useful data structure for navigating around tree-like structures in an efficient manner. I gave an introduction to the zipper, by starting with a simple type of trees

> data Tree     = Leaf | Node Tree Int Tree
and then showing how to arrive at the following definitions:

> type State    =  (Context, Tree)
> data Context  =  Top
>               |  NodeL Context Int Tree
>               |  NodeR Tree Int Context
> start         ::  Tree -> State
> start  t      =  (Top, t)
> left                   :: State -> State
> left (c, Node l n r)   =  (NodeL c n r, l)
> right                  :: State -> State
> right (c, Node l n r)  =  (NodeR l n c, r)
> up                     :: State -> State
> up (NodeL c n r, l)    =  (c, Node l n r)
> up (NodeR l n c, r)    =  (c, Node l n r)

Conor then explained the connection with differentiation, and also showed how to use the zipper to write an efficienct function that returns the mirror image of a tree. The lunch concluded with Nicolas Oury, who is visiting from France, explaining some of his work on simplifying the use of pattern matching in the Coq system.

Leave a Reply