Coercions
In coercive subtyping systems, subtypes are defined by implicit type conversion functions from subtype to supertype. For each subtyping relationship (S <: T), a coercion function coerce: S → T is provided, and any object s of type S is regarded as the object coerceS → T(s) of type T. A coercion function may be defined by composition: if S <: T and T <: U then s may be regarded as an object of type u under the compound coercion (coerceT → U ∘ coerceS → T). The type coercion from a type to itself coerceT → T is the identity function idT
Coercion functions for records and disjoint union subtypes may be defined componentwise; in the case of width-extended records, type coercion simply discards any components which are not defined in the supertype. The type coercion for function types may be given by f'(s) = coerceS2 → T2(f(coerceT1 → S1(t))), reflecting the contravariance of function arguments and covariance of return values.
The coercion function is uniquely determined given the subtype and supertype. Thus, when multiple subtyping relationships are defined, one must be careful to guarantee that all type coercions are coherent. For instance, if an integer such as 2 : int can be coerced to a floating point number (say, 2.0 : float), then it is not admissible to coerce 2.1 : float to 2 : int, because the compound coercion coercefloat → float given by coerceint → float ∘ coercefloat → int would then be distinct from the identity coercion idfloat.
Read more about this topic: Subtyping