Operational Semantics and Polymorphic Type Inference

Abstract

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