|
The Meaning of Types -- From Intrinsic to Extrinsic Semantics
John C. Reynolds December 2000 |
Abstract:
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 Available as PostScript, PDF, DVI. |