How do we reduce the cost of static verification for programmers? Type systems offer a low-tech but effective means to achieve this: Programmers express properties of programs using types; type checking verifies that a program adheres to the specification that its type expresses. Many traditional type systems cannot easily express data invariants or pre/post-conditions, but compilers can conveniently reconstruct all missing type information. On the other hand, type reconstruction in more expressive and sophisticated type systems (such as type systems with Generalized Algebraic Datatypes -- GADTs) is often undecidable or non-modular. Programming in a fully explicit fashion, where programmers provide all type information, is prohibitive, so there is need for eliminating the uninformative annotations.

This talk is about my work on bridging the gap between full type reconstruction and fully explicitly typed programming in such sophisticated type systems, now implemented in the Glasgow Haskell Compiler: How do we implement and specify modular, predictable, and economical (in terms of annotations) type inference in order to bring the advantages of both worlds to programmers? I will present my initial approach to type inference for GADTs and how it has benefited from the introduction of implication constraints in more recent work. I will show recent surprising results that indicate that ML-style polymorphism may not scale to advanced type system features, and how to work around these problems. I will finally describe ongoing work on taking one step further: Engineering a type inference specification and implementation to be parametric over a constraint domain without giving up modularity. Alongside the main theme, this talk will touch on some of my work on semantics and formal metatheory, and will mention exciting ongoing work on game-based serialization as well as ideas for future research.