Deriving a complete type inference for Hindley–Milner and vector sizes using expansion

• A derivation of a complete type inference algorithm from the denotational semantics.
• An inference for vector types of polymorphic size.
• Practical implementation and application of polymorphic recursion.

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, implying that type annotations cannot improve the result of type inference, thus making type annotations optional. 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 distinguishes 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.