All for Nothing: Gradual Typing with Polymorphism and Blame


Amal Ahmed


Static and dynamic typing offer complementary advantages: static typing provides early error detection, efficient execution, and better documentation of code, whereas dynamic typing encourages rapid development and makes it easier to adapt to changing requirements. As a result, they each have their adherents, but recently interest has emerged in a 'third way' that combines the best of both worlds.

In this talk, I will present a language that integrates statically typed and dynamically typed components, similar to the gradual types of Siek and Taha (2006), and show how to extend it to incorporate parametric polymorphism. This language, dubbed the polymorphic blame calculus, is a core calculus of casts between more and less precise types. Our system includes a notion of blame (as found in contracts), which allows us to show that when more-typed and less-typed portions of a program interact, that any type failures are due to the less-typed portion.

Values of polymorphic type satisfy a strong semantic property known as relational parametricity. Our system permits a dynamically typed value to be cast to a polymorphic type, with the type enforced by dynamic sealing. We have shown that this method of enforcement is so strong as to ensure relational parametricity.

(Joint work with Robby Findler, Jacob Matthews, and Philip Wadler)