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.
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 .