Graphical types and constraints - second-order polymorphism and inference

MLF is a type system that seamlessly merges ML-style implicit but second-class polymorphism with System-F explicit first-class polymorphism. We propose a dag representation of MLF types that superimposes a first-order term-dag, encoding the underlying term structure (with sharing), and a binding tree encoding the binding structure. This permits a simple and direct definition of type instance, that combines type instance on term-dags, simple operations on the binding tree, and a control that allows or rejects potential instances. Using this representation, we build a linear-time unification algorithm for MLF types. We then extend graphic types into a system of graphic constraints that can be used to perform type inference in both ML or MLF. We give a few semantic preserving transformations on constraints, and propose a strategy for applying those transformations to solve typing constraints. We show that the resulting algorithm has optimal complexity for MLF type inference, and that, as for ML, this complexity is linear under reasonable assumptions. We finally present a church-style version xMLF of MLF, in which all parameters of functions, all type abstractions, and all type instantiations are explicit. We give a set of reduction rules for simplifying type instantiations. The resulting system is confluent when strong reduction is allowed, and enjoys the subject reduction property. We also show progress for weak-reduction strategies, including call-by-name and call-by-value, with or without the value restriction. We exhibit a type-preserving encoding of MLF into xMLF, ensuring the type soundness of MLF.