Subtyping can have a simple semantics (Q1177151)

The semantics of typed languages are usually given by assigning some kind of collection to each type and interpreting an expression of some type as an element of the appropriate set. With subtyping, it is natural to assume that if \(A\) is a subtype of \(B\) then either (i) there is a conversion function \(c_{AB} : A \rightarrow B\), or (ii) the interpretation of \(A\) is a subset of the interpretation of \(B\). A priori, the first seems more general, but the second more intuitive. This paper gives a relatively straightforward construction, for an example function calculus, showing that any semantic structure satisfying condition (i) may be used to construct a semantic structure satisfying condition (ii). The main idea is simply to replace the interpretation of a type \(A\) by the union of the interpretations of all subtypes of \(A\). The only nontrivial problem is to give a coherent interpretation of expressions.