Semantics of subtyping

Iowa Type Theory Commute

I answer a listener's question about the semantics of subtyping, by discussing two different semantics: coercive subtyping and subsumptive subtyping. The terminology I found in this paper by Zhaohui Luo; see Section 4 of the paper for a comparison of the two kinds of subtyping. With coercive subtyping, we have subtyping axioms "A <: B by c", where c is a function from A to B. The idea is that the compiler should automatically insert calls to c whenever an expression of type A needs to be converted to one of type B. Subsumptive subtyping says that A <: B means that the meaning of A is a subset of the meaning of B. So this kind of subtyping depends on a semantics for types. A simple choice is to interpret a type A as (as least roughly) the set of its inhabitants. So a type like Integer might be interpreted as the set of all integers, etc. Luo argues that subsumptive subtyping does not work for Martin-Loef type theory, where type annotations are inherent parts of terms. For in that situation, A <: B does not imply List A <: List B, because Nil A is an inhabitant of List A but not of List B (which requires instead Nil B).
Join the telegram group here.