Type Compatibility

Consider the addition operation. It accepts two integral operands — the augend and the addend — and yields an integral sum. The type of both augend and addend is {…, −1, 0, 1, …}ᵀ. Each operand can happily alias any finite integer. Yet addition does not become invalid if the operands are constrained to narrower types:

It would be counterintuitive if the above code sample did not work as expected, because obviously any of the integers from 10 to 100 may meaningfully be added to any of the integers from 5 to 15. The restricted integral types {10, 11, 12, …, 99, 100}ᵀ and {5, 6, 7, …, 14, 15}ᵀ are type compatible with {…, −1, 0, 1, …}ᵀ because they are subtypes of it.

Generally speaking, wherever a type is expected, any subtype may be used instead. If an operation is meaningful for a particular value V, then it hardly matters what types V is construed to instantiate. Furthermore, if an operation is meaningful over some set of values, then it is because it is meaningful for each member of that set; it must therefore be meaningful over any subset of that set. Returning to the code sample above, the assignment to augend is acceptable because 25’s type — the type inferred for the literal phrase 25 — is compatible with [10..100].