Subtyping and subsumption
Subtyping is a relation between two types. It often comes with a typing rule called “subsumption”, which says that if type B is a subtype of type A (usually shown as B <: A), then a value of type B can be assumed to have type A.
When we make an operation implicit in a language, we need to make sure that it is (1) safe (2) performant. Users will be doing it without realizing, and we don’t want to accidentally break things or make them slow.
Examples: out-of-bounds array accesses should be caught, dangling pointers shouldn’t be allowed or dereferencing them should be caught in runtime.
Example: if I have a function f : A -> B and a value x : A after subsumption, f(x) shouldn’t fail in compile time or runtime.
There could be different safeties that the language guarantees. Some of those safeties may also be checked in runtime instead of compile time.
From a programmer’s perspective however, these are not enough to make sure that the program will work as before when subsumption is used. If I can pass a value of type B where A is expected, I need to make sure B, when used as A, acts like A.
