A. Simon. Deriving a Complete Type Inference for Hindley-Milner and Vector Sizes using Expansion. Science of Computer Programming, 95(2):254–271, 2014.

Type inference and program analysis both infer static properties about a program. Yet, they are constructed using very different techniques. We reconcile both approaches by deriving a type inference from a denotational semantics using abstract interpretation. We observe that completeness results in the abstract interpretation literature can be used to derive type inferences that are backward complete, a property akin to the inference of principal typings. The resulting algorithm is similar to that of Milner-Mycroft, that is, it infers Hindley-Milner types while allowing for polymorphic recursion. Although undecidable, we present a practical check that reliably distinguished typeable from untypeable programs. Instead of type schemes, we use expansion to instantiate types. Since our expansion operator is agnostic to the abstract domain, we are able to apply it not only to types. We illustrate this by inferring the size of vector types using systems of linear equalities and present practical uses of polymorphic recursion using vector types.

Download: PDF Reference: Bibtex Electronic Copy: DOI