Archive for March, 2006


Thursday, March 23rd, 2006

Lucas Dixon and I had a chat on the way to the bus stop, then I wrote this.

Take terms (from some suitable free monad) and compress them, yielding skeletons whose bones are the paths to variables. A Zipper 0 is a path in a term with only closed terms hanging off on either side. At the end of such a path, you either have a variable or a ‘joint’, being a term node with skeletons branching off.

If you’re smart enough to spot that mapping naughtE across anything is a no-op, you get a rather cheaper, yet still purely functional, implementation of substitution.

\textbf{explode} throws away the structure, giving you your term back. OK, my whiteboard doesn’t have a typechecker, so the second case in explode should yield an exploded node \left< \textsf{inr}\:\mathbf{map explode}\:f\right>.