A types-as-sets semantics for milner-style polymorphism

Publisher Website
Google Scholar
Abstract
In this paper we present a semantics for Milner-style polymorphism in which types are sets. The basic picture is that our programs are actually terms in a typed &lgr;-calculus, in which the type information can be safely deleted from the concrete syntax. In order to allow for common programming constructs, we allow reflexive or infinite types, and we also allow opaque types, which have private representations. An adaptation of Hindley's Principal Typing Theorem then asserts that the type information can be reconstructed. Thus expressions are polymorphic, since they may have more than one correct typing, but values are not. Expressions that are not well-typed are syntactically ill-formed, as they are in conventional mathematics, rather than having the meaning “wrong”. The resulting semantics is simpler than that for fully polymorphic models [Leivant 83], and generalizes the standard constructions, such as retracts and ideals.

This publication has 0 references indexed in Scilit: