BROADCASTS.com

b'

I answer a listener's question about the semantics of subtyping, by discussing two different semantics: coercive subtyping and subsumptive subtyping.\\xa0 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.\\xa0 With coercive subtyping, we have subtyping axioms "A <: B by c", where c is a function from A to B.\\xa0 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.\\xa0 Subsumptive subtyping says that A <: B means that the meaning of A is a subset of the meaning of B.\\xa0 So this kind of subtyping depends on a semantics for types.\\xa0 A simple choice is to interpret a type A as (as least roughly) the set of its inhabitants.\\xa0 So a type like Integer might be interpreted as the set of all integers, etc.\\xa0 Luo argues that subsumptive subtyping does not work for Martin-Loef type theory, where type annotations are inherent parts of terms.\\xa0 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.