STOP

This is the fourth of a series of posts based on experiences at POPL (Principles of Programming Languages), 2011, in Austin TX. (Here’s the firstsecond, and third.)

STOP (Script To Program Evolution) is a special interest workshop, colocated with POPL.

The day began with an invited talk by John Field (IBM Research) on Thorn, a new language for distributed computation with features for concurrency (actors with message passing) and gradual typing (like types).

I talked further about our POPL work, and gave a demo of our implementation. The response, as in POPL, was very encouraging: the overall consensus seemed to be that this was a really cool, “out-of-the-box” idea that would be great to continue work on.

Some students presented really cool work of particular interest to me. Tim Disney (UC Santa Cruz) talked about gradual information flow. It seems to me that this work can be extended to DCC (Abadi et al, POPL 1999), and thus may be more generally applicable to program analysis. Something to dig into when I have time. Ravi Chugh (UC San Diego) talked on polymorphic type inference with run-time logs. This work seemed to be along the lines of our POPL work, with some differences: we did not try to infer polymorphic types, but the types we infer are “principal” (most general). Frankly I do not think that their iterative inference algorithm based on contextual information has meaningful foundations; but I have to think more about this to be sure.

Phil Wadler expressed the need for evidence on whether type inference really matters for scripting languages. I had some thoughts around this, which I wanted to throw up for discussion but we ran out of time. I think that we need to be clear about what benefits types bring to programmers, and at what costs. Indeed, why would programmers want to evolve scripts to programs? Types improve robustness and performance. My stand is that to sell gradual typing, we need to sell performance, perhaps more so than robustness, since performance is a measurable benefit that the programmer can weigh against the cost of annotating or rewriting parts of the program.

Furthermore, should type inference coexist with gradual type checking? And what should the absence of type annotations mean: “dynamic” or “unknown”? (Remember Phil Wadler’s comment on the importance of syntax!)

After a quick lunch and a round of goodbyes, I rushed to the airport. There, I ran into Cormac Flanagan. Unfortunately, we were on different flights back. Picking up on a previous chat at POPL, we briefly talked some more on dynamic type inference and gradual typing; it seems they have made some interesting progress on semantic models for contracts, which may generalize some of this stuff. Seriously fun area to collaborate on in the future.