type-theorysubtyping

What is the difference between subtyping and subsumption?


What is the difference between subtyping and subsumption? Does subsumption mean implicit coercion?


Solution

  • Yes, you're mostly right.

    Subtyping is a relation over two types. By itself, it doesn't say how this relation actually applies to the typing of expressions.

    Subsumption usually means the presence of a typing rule for expressions that allows to apply subtyping to their types implicitly. There are languages that have subtyping but no subsumption rule, and where it must be invoked explicitly with a special type annotation (e.g., OCaml).

    There's also the somewhat independent aspect of whether subtyping is "coercive". Coercive subtyping changes the value it is applied to. For example, in a language where Int <: Float, subtyping may be coercive, because ints and floats are different domains. Typical OO-style subtyping on objects usually is non-coercive. However, this is a somewhat fuzzy notion, since it often depends on the choice of semantic model, and may not necessarily make an observable difference (unless a language allows to reverse subtying with downcasts). In practice, it refers to implementation techniques more than semantics.