Static and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a single language by giving the programmer control over which portions of the program are statically checked based on the presence or absence of type annotations. In this talk I review how gradual typing applies to functional and object-oriented languages and then present new work on integrating gradual typing with unification-based type inference. The goal of this is to provide tool assistance for increasing the amount of static checking in a program. The key question in combining gradual typing and inference is how should the dynamic type of a gradual system interact with the type variables of an inference system. I will explore the design space and show why three straightforward approaches fail to meet the design goals. In particular, the combined system should satisfy the criteria for a gradual type system: 1) when a program is unannotated, only a few type errors are detected at compile-time and the rest are detected at run-time, and 2) when the program does not contain dynamic type annotations (implicitly or explicitly), the type system should statically detect all type errors. I then present a new type system based on the idea that a solution for a type variable should be as informative as any type that constrains the variable. I show how the new type system satisfies the above criteria and describe an efficient inference algorithm for it.
Invited talk at FOOL 2008; Sunday, 13 January 2007; San Francisco, California, USA.