On Polymorphic Recursion, Type Systems, and Abstract Interpretation

The problem of typing <I>polymorphic recursion</I> (i.e. recursive function definitions <I>rec{x = e}</I> where different occurrences of <I>x</I> in <I>e</I> are used with different types) has been investigated both by people working on type systems and by people working on abstract interpretation. Recently, Gori and Levi have developed a family of abstract interpreters that are able to type all the ML typable recursive definitions and interesting examples of polymorphic recursion. The problem of finding type systems corresponding to their abstract interpreters was open (such systems would lie between the let-free fragments of the ML and of the Milner-Mycroft systems). In this paper we exploit the notion of principal typing to: (i) provide a complete stratification of (let-free) Milner-Mycroft typability, and (ii) solve the problem of finding type systems corresponding to the type abstract interpreters proposed by Gori and Levi.