A Types-as-Sets Semantics for Milner-Style Polymorphism

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 λ-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.