Many languages allow some form of type-level computation, where we allow more complex types to reduce definitionally to simpler ones, whether by β-reduction or other means. Yet once dependency is introduced between arguments, this gets even harder: a reduction in earlier arguments to a function might make later arguments ill-typed. GHC has recently struggled with this aspect of type-level computation, and we have come up with an algorithm that (we believe) handles all the tricky cases. At the same time, it would seem that other languages would have had to battle this same problem. Maybe each language has its own solution… and maybe they’re all different! This discussion will be about sharing and discussing these approaches to see if there is any commonality, and whether perhaps it is worthwhile to write up a “best” approach.

Principal Researcher at Tweag. 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. I am a core contributor to the Glasgow Haskell Compiler (GHC) and Chair of the Board of Directors at the Haskell Foundation.