The Meaning of Types -- From Intrinsic to Extrinsic Semantics
John C. Reynolds
A definition of a typed language is said to be ``intrinsic'' if it assigns meanings to typings rather than arbitrary phrases, so that ill-typed phrases are meaningless. In contrast, a definition is said to be ``extrinsic'' if all phrases have meanings that are independent of their typings, while typings represent properties of these meanings.
For a simply typed lambda calculus, extended with recursion, subtypes, and named products, we give an intrinsic denotational semantics and a denotational semantics of the underlying untyped language. We then establish a logical relations theorem between these two semantics, and show that the logical relations can be ``bracketed'' by retractions between the domains of the two semantics. From these results, we derive an extrinsic semantics that uses partial equivalence relations