Last week, I went to Boston for a few days to work with Amal on our ongoing multi-language parametricity project. We got some solid work done before hitting a roadblock on Friday afternoon and realizing that we're going to have to go back and rework a number of things in order to show the second result that we want to have in our paper. Our first result -- that one can combine a static language that has parametric polymorphism with a dynamic language, and still have guaranteed parametricity in the combined language by way of a run-time "sealing" technique -- is feeling solid now, but the second result still needs a lot of work. It tries to leverage the first result to prove that parametricity is also guaranteed for contracted terms in a purely dynamic language (where the contracts are implemented by embedding dynamic terms in the static language at types that are the static counterparts to whatever contracts you want 'em to have, and then immediately embedding those terms right back in the dynamic language). You wouldn't think that proving this second result would be too much of a leap once the first result is in place, but there are some really nasty bits when you actually try to do it.
I did have a cute contracts-are-not-types realization on Thursday afternoon. In a dynamic language, there are no type variables, no type abstractions, and no type applications. So that means that when we define the relatedness of two untyped terms that have a ∀α.τ contract on them -- meaning that at runtime, they are supposed to behave like parametrically polymorphic functions -- we can't define it in terms of the relatedness of their subterms. In fact we can't even talk about their subterms, because we don't know anything about the structure of the terms to start with -- they can't be type abstractions, because those don't exist! Instead, we have to say that two terms that are related to each other at the ∀α.τ contract are also related to each other at the τ contract, in an extended contract environment that has a binding for any free αs in τ. At first, I was all, "Wait, what? Which type are they actually?", and then I realized that that was the wrong question.
Anyway, today I scanned and sent Amal the seventeen handwritten pages that I produced over the three days I was in Boston; they'll be a starting point for sorting out the remaining nasty bits. I'm not gonna lie: this project has been long and difficult, and I'm looking forward it to being done this year. (It will be done this year!) But I've gotten a lot out of it; Amal pointed out that if I go to OPLSS this summer, there won't be anything new to me in the material she's presenting. That was good to hear -- both because it makes me feel like I've truly learned something, and because a little break, in between trying to absorb new material from all the other OPLSS speakers, will be most welcome if I do go.
