A semantic model of types for applicative languages

Abstract

If integer constants are added to the syntax of the pure lambda calculus, then primitive integer values have to be added to the underlying domain V of values. Unlike functions, primitive values should not be applied; we want a run-time error to occur if an attempt is made to apply them as functions. Expressions that might lead to run-time errors are separated out by imposing a “type” structure on expressions. A systematic model of types is developed, in which types are formalized as “ideals” (sets with a certain structure). Polymorphic functions are handled by introducing a quantifier for taking conjunctions of types. Operations for constructing new types from old lead to the consideration of higher-order or meta types, which are called “kinds” to avoid confusion with types. Finally, the semantic model of types is applied to show the soundness of a proof system for inferring the types of expressions.