What do types mean? — From intrinsic to extrinsic semantics

Abstract

A definition of a typed language is said to be ``intrinsic'' if itassigns meanings to typings rather than arbitrary phrases, so that ill-typedphrases are meaningless. In contrast, a definition is said to be ``extrinsic'' if all phrases have meanings that are independent of theirtypings, while typings represent properties of these meanings.For a simply typed lambda calculus, extended with integers, recursion, andconditional expressions, we give an intrinsic denotational semantics and adenotational semantics of the underlying untyped language. We thenestablish a logical relations theorem between these two semantics, and showthat the logical relations can be ``bracketed'' by retractions betweenthe domains of the two semantics. From these results, we derive an extrinsicsemantics that uses partial equivalence relations.