Type inference and type containment

Abstract

Type inference, the process of assigning types to untyped expressions, may be motivated by the design of a typed language or semantical considerations on the meanings of types and expressions. A typed language GR with polymorphic functions leads to the GR inference rules. With the addition of an "oracle" rule for equations between expressions, the GR rules become complete for a general class of semantic models of type inference. These inference models are models of untyped lambda calculus with extra structure similar to models of the typed language GR. A more specialized set of type inference rules, the GRS rules, characterize semantic typing when the functional type σ → τ is interpreted as all elements of the model that map σ to τ and the polymorphic type ∀t.σ(t) is interpreted as the intersection of all σ(τ). Both inference systems may be reformulated using rules for deducing containments between types. The advantage of the type inference rules based on containments is that proofs correspond more closely to the structure of terms.