Most models of intersection types, such as filter models, are extrinsic semantics, i.e., terms have the same meaning as in a typeless model, and the type of a term denotes a property of its meaning. In contrast, the usual denotational semantics of a real programming languages is an intrinsic semantics, in which only well-typed terms have meanings, which are defined by induction on the proof of their typing.

We will illustrate this distinction by relating the two kinds of semantics for the functional sublanguage of the programming language Forsythe.

Keywords: intersection types, Forsythe, denotational semantics, intrinsic vs. extrinsic semantics.