The type inference and generalization algorithms used in both OCaml and GHC are based on type levels, a concept originally pioneered by Didier Rémy in 1992 (called ranks at that time). As we descend into an abstract syntax tree, the levels increase, and thus we can use the level of a type variable to determine whether it should be generalized. (Generalization is sound only when it affects only those type variables local to a definition.) Levels form a powerful organizing principle in a type inference and checking implementation. Interestingly, both OCaml and GHC have found additional uses for levels, beyond just generalization. This talk will explore what levels are, how they can be used for generalization, and the other applications for them in both compilers.

Software Engineer at Jane Street. I believe that clever application of theory can eliminate a great deal of programmer errors – specifically, I think fancy types and functional programming are the future. I completed my PhD in 2016 at University of Pennsylvania working under Stephanie Weirich; my dissertation topic was the integration of dependent types into the Haskell programming language. My work now centers around improvements to OCaml’s type system to empower more performant programming – without sacrificing safety. In addition, I am a contributor to the Glasgow Haskell Compiler (GHC) and frequent collaborator on its type system and implementation.