A Simple Semantics for ML Polymorphism

10 years 6 months ago
A Simple Semantics for ML Polymorphism
We give a framework for denotational semantics for the polymorphic “core” of the programming language ML. This framework requires no more semantic material than what is needed for modeling the simple type discipline. In our view, terms of ML are pairs consisting of a raw (untyped) lambda term and a type-scheme that ML’s type inference system can derive for the raw term. We interpret a type-scheme as a set of simple types. Then, given any model M of the simply typed lambda calculus, the meaning of an ML term will be a set of pairs, each consisting of a simple type τ and an element of M of type τ. Hence, there is no need to interpret all raw terms, as was done in Milner’s original semantic framework. In comparison to Mitchell and Harper’s analysis, we avoid having to provide a very large type universe in which generic type-schemes are interpreted. Also, we show how to give meaning to ML terms rather than to derivations in the ML type inference system (which can be infinitel...
Atsushi Ohori
Added 11 Aug 2010
Updated 11 Aug 2010
Type Conference
Year 1989
Where FPCA
Authors Atsushi Ohori
Comments (0)