CODEWITHSUNDEEP
type-theorysubtyping
user1804599
user1804599

Reputation:

What is the difference between subtyping and subsumption?

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

Upvotes: 5

Views: 1132

Answers (1)

Andreas Rossberg
Andreas Rossberg

Reputation: 36118

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.

Upvotes: 6

Related Questions