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.