On Thu, Jul 1, 2010 at 1:54 PM, Sergey Mironov
Hello list! I am trying to understand zipper concept using papers like [1] and [2]. Though main idea looks clear, I still have a problem in applying it for custom data types.
Please help me with deriving Zipper-type from
data DTree a = P | D [(a, DTree)]
Looking in [1] ('Zippers via Differentiation' chapter) I tried to do the following:
1. Find a DTreeF type which is a pattern functor ([2], chapter 2.1) of my DTree 2. Write DTreeF in 'algebraic' form (using '+' and '*') 3. Find DTreeF' - "derivative" of DTreeF 4. Define my zipper type using list of DTreeF'
Step 1 likely ends with
data DTreeF a x = P | D [(a,x)]
[2] says that using this pattern functor one could build a fixed-point version of DTree:
data Fix f = In {out :: (f (Fix f))} data DTreeFP = Fix DTreeF
but seems that I have nothing to do with it right now.
Step 2 is my main question:
In [1] authors did it for binary tree:
data Tree a = Leaf a | Bin (Tree a) (Tree a)
data TreeF a x = Leaf a | Bin x x
and thus
TreeF = a + x * x
TreeF' = x + x
My DTree has inner list of tuples. How should I rewrite it in terms of '+' and '*' ?
I would just use List. IIRC the derivative of list is: data DList a = DLIst [a] [a] Understood as the elements before the focused one and those after it. Unfortunately I can't remember how that is derived, and my own experiments failed to come up with anything similar. That may indicate that the rest of this message is nonsense. data DTree a = P | D [(a, DTree a)] Can be written algebraically as: DTree a = 1 + List (a * DTree a) DTree a = Mu f. 1 + List (a * f) Differentiating: DDTree a = Mu f. DList (a * f) * a DDTree a = DList (a * DTree a) * a To understand this intuitively, DDTree a is the context in which a DTree can appear within itself. So that is: The (a * DTree a)s that appeared before and after the current list element, together with the a that was paired with the current element. At least that is how I understand it. I admit there was some handwaving going on in the details. Luke