Gradual Typing

It is a widely accepted view that dynamically type-checked languages are a good choice for scripting and prototyping, while statically type-checked languages are a better choice for large-scale software engineering projects, performance, and long-term code maintainability; bigger debates are raging about which paradigm is better-suited for programming education. Gradual Typing can bridge these divides:

• Even large software projects start with small prototypes. Using Gradual Typing, developers can rapidly iterate on various designs using dynamic typing, and gradually move over stabilized parts of the code to static typing to reap its benefits. The same is true for any extensions to existing statically-typed codebases as part of their ongoing maintenance.
• Interacting with the outside world such as the filesystem, databases, or the internet mostly happens via low-level interfaces that do not neatly correspond to a language's type system. This is very common in scripting tasks, but also in larger applications. In both cases, not having to worry about the type-checker where it is less helpful while still getting its help elsewhere in the code is useful.
• Even if one subscribes to the idea that teaching programming should first happen in a dynamically-typed language to build computational intuition, having typed standard libraries and corresponding IDE is helpful to students even if they do not use type annotations on their own.

Almost all current implementations of gradually-typed languages were created by adding gradual typing to an existing language. Starting from a dynamically-typed language, this requires designing a type system that can capture the many idioms of the language and type its current standard library. So far, this has always forced a choice between unsoundness (e.g. TypeScript, Hack) and huge overheads due to expensive run-time type checks (e.g. Racket, Reticulated Python, Safe TypeScript). In contrast, starting from a statically-typed language is complicated because in such languages, types may affect the semantics of a program (for example, through overloading). This in turn often violates the gradual guarantee, the key property that allows programmers to add type annotations to stabilized dynamic code without changing what their program does (e.g. in C#).

The goal of my research in this area is to find ways to design a modern, industrial, object-oriented programming language that has efficient, sound, and well-behaved (in the sense of the gradual guarantee) Gradual Typing.