Abstract Gradual Typing with Unification-based Inference.pdfVIP

Gradual Typing with Unification-based Inference Jeremy G. Siek Manish Vachharajani University of Colorado at Boulder {siek,manishv}@colorado.edu Abstract Static and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a sin- gle language by giving the programmer control over which portions of the program are statically checked based on the presence or ab- sence of type annotations. This paper studies the combination of gradual typing and unification-based type inference, with the goal of developing a sys- tem that helps programmers increase the amount of static checking in their 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. This pa- per explores the design space and shows why three straightforward approaches fail to meet our design goals. In particular, the com- bined system should satisfy the criteria for a gradual type system: 1) when a program is unannotated, only a few type errors are de- tected 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. This paper presents 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. We prove that the new type system satisfies the above criteria for a gradual type system. The paper also develops an efficient inference algorithm and proves it sound and complete with respect to the type system. Categories and Subject Descriptors D.3.3 [Programming Lan- guages]: Language Constructs and Features; F.3.3 [Logics and Pro- gram Constructs]: Studies of Program Constructs—Type structure General Terms Languages, Algorithms Keywords dynamic typing, static typing, type inference, unifica- tion, gradual typing, simply ty