Abstract

This work presents the design, implementation, and evaluation of a Hindley-Milner-style type inference algorithm with a not-widely adopted level-based generalization and separated constraint generation and solving. The implementation relies on the intrinsically scoped and generic abstract syntax generated with the recently introduced Free Foil framework. It targets an object language similar to lambda calculus extended with let-polymorphism, natural numbers, and boolean literals. We demonstrate the correctness of our prototype through a test suite and highlight the benefits of intrinsic scoping and modular design enabled by Free Foil. The thesis concludes by discussing the system's strengths, limitations, and directions for future work toward a reusable type inference library.