A Flexible Framework for Type Inference with Existential Quantification

Abstract. 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 infor-mation. 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 quan-tification and demonstrates the framework on a small object-oriented typed assembly language. The framework is flexible enough to support language features such as downward casts, arrays, and interfaces. The framework is based on category theory, the first such application of cat-egory theory to type inference to the best of our knowledge.