A graphical presentation of MLF types with a linear-time unification algorithm.
Didier Rémy and Boris Yakobowski
The ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2007)
Nice, France, January 16, 2007
Abstract
MLF is a language that extends both ML and System F and combines the benefits of both. We propose a dag representation of MLF types that superposes a term-dag, encoding the underlying term-structure with sharing, and a binding tree encoding the binding-structure. This representation is more canonical as it factors out most of the notational details of the original definition; it is also closely related to first-order terms. Moreover, it permits a simpler and more direct definition of type instance that combines type instance on first-order term-dags, simple operations on dags, and a control that allows or rejects potential instances. Using this representation, we build a linear-time unification algorithm for MLF types, which we prove sound and complete with respect to the specification.