Subtyping - Coercions

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 coerce_{S → 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 (coerce_{T → U} ∘ coerce_{S → T}). The type coercion from a type to itself coerce_{T → T} is the identity function id_T

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) = coerce_{S2 → T2}(f(coerce_{T1 → 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 coerce_{float → float} given by coerce_{int → float} ∘ coerce_{float → int} would then be distinct from the identity coercion id_float.