This post is dedicated to this versatile tool being applied to thrists to obtain an isomorphic data structure which I call the ThristZipper.
As the ideogram demonstrates, this zipper consists of three parts:
- the left-associate thrist (usually holding the already visited portion),
- the focus element e,
- the (right-associative) thrist (usually to be iterated over).
data LeftThrist :: (* → * → *) → * → * → * where
LeftNil :: LeftThrist k a a
LeftCons :: LeftThrist k a b → k b c → LeftThrist k a c
Again, the types match up. Now we can define ThristZipper:
data ThristZipper :: (* → * → *) → * → * → * where
Focus :: LeftThrist k a b → k b c → Thrist k c d → ThristZipper k a d
It remains to define all the operations on ThristZipper that will make it a versatile tool.
We start with zipInto:
zipInto :: Thrist k a b → Maybe (ThristZipper k a b)
zipInto Nil = Nothing
zipInto (Cons e r) = Just (Focus LeftNil e r)
We can similarly define zipLeftInto, advancing, focus manipulation, maps, folds and getting out on the right or in the left. These are of course left as an exercise to the reader, but I will define retract (the opposite movement from advance) here for good measure:
retract :: ThristZipper k a b → Maybe (ThristZipper k a b)
retract (Focus LeftNil _ _) = Nothing
retract (Focus (LeftCons r e') e t) = Just (Focus r e' (Cons e t))
And a lot prettier in Ωmega (svn HEAD):
retract (Focus []lt _ _) = Nothing
retract (Focus [r; e']lt e t) = Just (Focus r e' [e; t]l)
PS: I definitely plan to make all this part of thrist-1.0 when it arrives.
No comments:
Post a Comment