Luke Palmer wrote:
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.
Note that there is a really subtle difference between derivative and zipper which is probably the source of confusion. For lists, both are the same, though. The derivative of the list type with respect to the element type is d List = d (\a -> 1 + a * List a) = \a -> List a + a * d List a d List a = List a + a * d List a d List a ~ List a * List a The very last isomorphism of types is not trivial and probably the reason why you were stumped.
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
The difference between zipper and derivative shows up here. Namely, your second equation for DDTree a does not follow from the first, it should be DDTree a = DList (a * DDTree a) * a ^^ two Ds
To understand this intuitively, DDTree a is the context in which a DTree can appear within itself.
The context in which DDTree a can appear within itself is indeed the zipper. But this is different from the derivative with respect to a , which gives the context in which a can appear within DDTree a . To get the zipper, you have to derive the pattern functor with the respect to the variable that will tie the recursion, in this case f . d (DTreeF a) = d (\f -> 1 + List (a * f)) = 0 + (d (\g -> List g) (a * f)) * d (\f -> a * f) = d List (a * f) * a
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.
Then, the zipper is a *list* of these things: ContextDTree a = List (DList (a * DTree a) * a) After all, what you describe is only the context of DTree a within a single level, but it might be many levels down in the tree. Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com