On Polymorphic Recursion, Type Systems, and Abstract Interpretation

Abstract. The problem of typing polymorphic recursion (i.e., recursive function definitions rec {x = e} where different occurrences of x in e 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 in-teresting 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