(In-)Coherence under Transitivity of Coercive Subtyping

While coercions improve ergonomics, the freedom to add them introduces the risk of inconsistency. In particular, multiple coercion paths between the same two types may produce different results. Example 6. Suppose we have the following coercions, which would prove quite useful for pretty printing and serialization:

• Real → String
• Degrees → Real
• Radians → Real
• Radians → Degrees

Then a value of type Radians can be converted to String along two different paths:

• Radians → Real → String or
• Radians → Degrees → Real → String.

These may yield different string outputs (e.g. depending on whether the intermediate repre- sentation is degrees or reals), which breaks consistency.

Quite similarly, we might be tempted to define specialized coercions for

• Degrees → String, which renders into 1.23 °
• and Latitude → String, yielding 1.23 °N.

Obviously, in the presence of transitivity such type hierarchies will collapse under inconsistencies.

A coercion system is considered or consistent (or coherent) if, for any given source type σ and target type τ, all valid coercion paths from σ to τ are uniquely defined, i.e. they produce the same result for the same value. Coherence thus guarantees predictability and prevents semantic ambiguity.

Related