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.
In this talk, we will illustrate both kinds of definitions for a purely functional language with intersection types that is a sublanguage of the Forsythe programming language. As with Forsythe, the intrinsic definition will use limits in a category, but now this will be a category of algebraic lattices rather than a functor category.
We will also give a domain-theoretic definition of the corresponding untyped language, and establish logical relations between these definitions. Finally, we will define embedding-retraction pairs between the typed and untyped semantics, prove that these pairs "bracket" the logical relations, and use this fact to derive an extrinsic semantics, in which types denote partial equivalence relations.