Gradual Typing with Unification-based Inference

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. This paper studies the combination of gradual typing and unification-based type infer-ence, with the goal of developing a system that helps programmers increase the amount of static checking in their program. The key question in combining gradual typing and infer-ence is how should the dynamic type of a gradual system interact with the type variables of an inference system. This paper explores the design space and shows why three straightfor-ward approaches fail to meet our 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