A Flexible Framework for Type Inference with Existential Quantification

Preserving types through compilation guarantees safety of the compiler output without trusting the compiler: the compiler output is annotated with types and can be verified. Type inference can make this technique more practical by inferring most of the needed type information. Existential types, however, are difficult to infer, especially those with implicit pack and unpack operations.
This paper proposes a framework for type inference with existential quantification and demonstrates the framework on a small object-oriented typed assembly language. The framework is flexible enough to support language features such as downward cast, arrays, and interfaces. The framework is based on category theory, the first such application of category theory to type inference to the best of our knowledge.