The Meaning of Types From Intrinsic to Extrinsic Semantics

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.