Polymorphic typing by abstract interpretation

Abstract

This paper presents a generic method which uses the framework of Abstract Interpretation as defined by the Cousots [6] to build type reconstruction algorithms. Fundamentally, this method is based upon the combination of an upper and a lower approximation as well as the use of widening operators to insure algorithm termination. We illustrate this method with a type reconstruction algorithm of the expressions of a ML-like language more or less similar to Mycroft's ML+ type system[14]. We first show that restricting recursively defined constants to monomorphic types—as in ML—can be seen as a widening operator. Then we exhibit a less restrictive operator which lets recursively defined expressions have polymorphic types, while still insuring algorithm termination.