Operational Semantics and Polymorphic Type Inference

Abstract

Three languages with polymorphic type disciplines are discussed, namely the
\nλ-calculus with Milner's polymorphic type discipline; a language with imperative
\nfeatures (polymorphic references); and a skeletal module language with structures,
\nsignatures and functors. In each of the two first cases we show that the
\ntype inference system is consistent with an operational dynamic semantics.
\nOn the module level, polymorphic types correspond to signatures. There is
\na notion of principal signature. So-called signature checking is the module level
\nequivalent of type checking. In particular, there exists an algorithm which either
\nfails or produces a principal signature.