Functional Pearl: Dependent type inference via free higher-order unification
share
Many type theories rely significantly on dependent types. Implementing a proof assistant or a programming language based on such a theory is often challenging, as type inference is notoriously hard in the presence of dependent types. The cornerstone of dependent type inference is higher-order unification. Even though many algorithms exist, state-of-the-art is implementing it directly for a particular proof assistant. We propose a novel approach for abstract syntax representation, which we call free scoped monads. This approach capitalizes on the ideas of free monads and Swierstra's data types à la carte, combining them with intrinsically well-scoped term representation via Bird and Patterson's de Bruijn notation as nested data types. These constructions allow us to handle scopes in a language-agnostic way and provide generic higher-order unification algorithms, which serve as a foundation for dependent type inference. Using the Haskell programming language, we apply this approach to simply typed lambda calculus and Martin Löf Type Theory. We show that our approach is transparent for the user, yet provides non-trivial type inference almost for free.
READ FULL TEXT