Jason (jcreed) wrote,

Had another Aha moment in the shower.

So William was explaining to me at some point the original idea of "zippers" (due to Huet and his experience hacking unification), and the claim that this whole notion of recursive-datatype-object-with-hole is useful for functional programming because something of type T * TH (if T is the recursive datatype and TH is its one-hole type) is like a pointer into an object of type T. Why? Because the TH object is everthing 'above' the pointer, and the T object is everything below. There is a very natural function of type T * TH -> T that fills in the hole. So I observed that this function is wildly noninjective for exactly the reason that the function's domain is like T-with-pointer: for every place you could have a pointer in e : T, there is a T * TH pair that gets mapped to e. Wanting to come up with some sort of isomorphism, I wrote on the whiteboard something to the effect of

T * TH = T * TP

hoping that there would be another operation of finding "paths" for a type that might have some other cute connection to calculus. Trying to think of identities it ought to satisfy, I came up with an intuition that surely

(A * B)P = AP + BP

since a path through a tuple is either a path into the one side or the other, and immediately got my hopes up that "paths" was the coveted logarithm function. Sadly, I'm pretty certain this is wrong now. For one thing, T * TP isn't right at all: the set of paths depends heavily on the object that you want paths in. So instead I should write some dependently typed thing like

T * TH = Πt : T . TP(t)

That's certainly a dangerous tangle to get into.

However! I realized that I had just mentioned the idea of the function X * _ (as opposed to the function X + _) as an "alternative notion of hole" last night. I realized the intuitive meaning of starting with a type operator F, taking the X-derivative of μα. X * F(α), and subsequently plugging in the unit type for X, is exactly a thing of type μα.F(α) with one of the nodes in the "tree" singled out as marked. Since what you've done is wedged in the possibility for X-typed data to exist not in alternation (as with X + _) but in conjunction with every recursive call to the μ-bound variable. So an X-hole in this setup is a pointer that doesn't clobber the existing data. Plugging 1 back into X gets rid of all the potential pointers that didn't get chosen. And, amazingly enough, if you work out the calculation, this type does wind up being isomorphic to T * TH. So there's a very nice canonical-seeming zipper equation ("FTOZ"? :) that pops out, namely

μF * (μ(X + F))'(0) = (μ(X * F))'(1)


Actually, I think that paths may be something like natural log after all. I can't yet figure out any intuition for it for raw types (as opposed to type operators), but whatever. Here's the suggestively persuasive example:

Ignoring recursive types for the moment, suppose you have a type operator T(X). Let T'(X) be the type of Ts with one hole in place of an X. Let T#(X) be the type of paths through something of type T to an X. Then the zipper equation is

T'(X) * X = T(X) * T#(X)

I.e., if we have a T with an X-shaped hole and an X, then that gives us a T and residually a piece of information that says where the hole was. So suppose T is multisets over n-tuples of X for some fixed n. That is, T(X) = e^(n * X). Then

(e^(n * X))' * X = e^(n * X) * T#(X)
n * e^(n * X) * X = e^(n * X) * T#(X)

so it seems like T#(X) ought to be (n * X), the log of the original thing.
Tags: math, morning
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded