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

One Response to “Skeletons”

  1. ldixon Says:

    I think there is a small error: at the moment it looks like the variable must occur down every branch of a skeleton. But it should be possible that some branches don’t contain the variable.

    The original motivation for this idea was that I wanted a way to incrementally instantiate without having to parse through the whole of the term. We thought that providing “signposts” in the term would allow avoiding large sections of the term in which the variable did not occur.

    Anyway, for the binary tree case I think it should be ….

    Term V = μ T. V + 1 + T²

    Zipper V = [2×(Term V)]

    Skeleton V =
    μ S. Zipper ∅ ×
    (V + S × S + S × Term V + Term V × S × Term V x Term V)

    or more briefly:

    Skeleton V = μ S. Zipper ∅ × (V + (S + Term V)² )

    (by “(a + b)² = a² + 2ab + b²”)

Leave a Reply

You must be logged in to post a comment.