Subtyping and coercion are two related concepts for enabling polymorphic re-use in programming languages. I want to lay out exactly what they are and how they exist in Rust, and in particular how they relate to variance which exists today, is being implemented, or will be implemented as part of the work on dynamically sized types (DST). My terminology will not exactly fit that used by PL people or Rust people, sorry.
In the general case (i.e., not just Rust) subtyping is a relation on types which says that T is a subtype of U if T is in some sense a more specific type than U. More precisely we might like to say that T and U denote sets of values and the set of values denoted by T is a subset of the set of values denoted by U. That gets complicated when thinking about existential types and so forth if we don't have explicit values for the introduction of such types, and if we do, then I think things get a little circular and not very helpful for thinking about real programming languages.
Thinking of expressions in a language, if an expression has type T, it can be used anywhere we would expect an expression of type U. This is inclusion polymorphism (aka the Liskov substitution principle or strong behavioral subtyping. There are subtle differences between these three terms, but I could only describe them in the most hand-wavy terms, so I won't).
Coercion is an operation on values (or expressions) where a value of type T can be changed in some way to a value of type U. An example is using an integer as a float - this is allowed transparently in many languages, but the compiler must insert code which does the low-level conversion from integer to float. We usually assume (hope?) that conversions due to coercion are cheap.
When actually writing code, subtyping and coercion often look the same. Many programmers do not realise there is even a difference. For example, 'subtyping' between pointer types in C++ with multiple inheritance is technically a coercion because of the pointer adjustment required by the implementation using multiple vtables.
Rust has basically no subtyping. The only subtyping it has is due to contravariance with respect to lifetime variables. I (Niko has done the hard work already) am currently extending this to variance (where safe, along the usual lines) with respect to subtyping. Rust has coercions between structs and traits given by `impl`s (well, between references to such things). It should, soon hopefully, have coercions between sub-traits and eventually, maybe sub-structs. Plus coercions between numeric types, etc., which are less interesting for now.
I would like to further classify subtyping and coercions along some axes. The key difference is that subtyping does not change the underlying value and coercion does (as discussed above). Both subtyping and coercion may be explicit or implicit. I sometimes refer to implicit subtyping as subsumption, but I'm not sure if that is common or correct. In Rust, subtyping is always implicit and coercion is sometimes implicit (trait objects) and sometimes explicit (numeric conversions, i.e., they require `as`. Coercion used to always be explicit until recently).
In Rust, only subtyping is used in the type inference algorithm.
The last axis I have thought of is a bit more hazy and a bit more of an implementation detail than a fundamental. It is that coercion restricts access to the value coerced. If coercion changes a value, it would be unsafe to continue to access the value via the old type. Either coercion must copy a value (i.e., only the new, copied value has the new type), or we must ensure that the old value cannot be accessed whilst the coerced value exists. Rusts linearity rules ensure this.
With DST, coercion becomes much more complicated. In particular we will add covariant coercions which must coerce fields of a struct. That is, they change things deep inside the struct, not just at the surface of a value. In contrast to subtyping, covariant coercion is always safe because we can no longer access the coerced value via its old type. (Thinking about proving safety gave me the insight that coercion actually _changes_ the type of a value, whereas subtyping gives multiple types to a single value (which is not to say that coercion always implies monomorphic types)).
We have talked a little (I think Niko has thought more) about perhaps changing the relationship between subtyping and type inference. Perhaps not all subtyping should be taken into account by the type inference algorithm. And/or perhaps some coercions should be taken account of. I don't really know - I have a hard time visualising how type checking would be affected by these changes.
I feel like I should have a point to make now, but I don't. I just did a lot of thinking to clarify all this in my head, so I thought I should write it down. And who knows? It might be helpful or interesting to someone else too.
In the general case (i.e., not just Rust) subtyping is a relation on types which says that T is a subtype of U if T is in some sense a more specific type than U. More precisely we might like to say that T and U denote sets of values and the set of values denoted by T is a subset of the set of values denoted by U. That gets complicated when thinking about existential types and so forth if we don't have explicit values for the introduction of such types, and if we do, then I think things get a little circular and not very helpful for thinking about real programming languages.
Thinking of expressions in a language, if an expression has type T, it can be used anywhere we would expect an expression of type U. This is inclusion polymorphism (aka the Liskov substitution principle or strong behavioral subtyping. There are subtle differences between these three terms, but I could only describe them in the most hand-wavy terms, so I won't).
Coercion is an operation on values (or expressions) where a value of type T can be changed in some way to a value of type U. An example is using an integer as a float - this is allowed transparently in many languages, but the compiler must insert code which does the low-level conversion from integer to float. We usually assume (hope?) that conversions due to coercion are cheap.
When actually writing code, subtyping and coercion often look the same. Many programmers do not realise there is even a difference. For example, 'subtyping' between pointer types in C++ with multiple inheritance is technically a coercion because of the pointer adjustment required by the implementation using multiple vtables.
Rust has basically no subtyping. The only subtyping it has is due to contravariance with respect to lifetime variables. I (Niko has done the hard work already) am currently extending this to variance (where safe, along the usual lines) with respect to subtyping. Rust has coercions between structs and traits given by `impl`s (well, between references to such things). It should, soon hopefully, have coercions between sub-traits and eventually, maybe sub-structs. Plus coercions between numeric types, etc., which are less interesting for now.
I would like to further classify subtyping and coercions along some axes. The key difference is that subtyping does not change the underlying value and coercion does (as discussed above). Both subtyping and coercion may be explicit or implicit. I sometimes refer to implicit subtyping as subsumption, but I'm not sure if that is common or correct. In Rust, subtyping is always implicit and coercion is sometimes implicit (trait objects) and sometimes explicit (numeric conversions, i.e., they require `as`. Coercion used to always be explicit until recently).
In Rust, only subtyping is used in the type inference algorithm.
The last axis I have thought of is a bit more hazy and a bit more of an implementation detail than a fundamental. It is that coercion restricts access to the value coerced. If coercion changes a value, it would be unsafe to continue to access the value via the old type. Either coercion must copy a value (i.e., only the new, copied value has the new type), or we must ensure that the old value cannot be accessed whilst the coerced value exists. Rusts linearity rules ensure this.
With DST, coercion becomes much more complicated. In particular we will add covariant coercions which must coerce fields of a struct. That is, they change things deep inside the struct, not just at the surface of a value. In contrast to subtyping, covariant coercion is always safe because we can no longer access the coerced value via its old type. (Thinking about proving safety gave me the insight that coercion actually _changes_ the type of a value, whereas subtyping gives multiple types to a single value (which is not to say that coercion always implies monomorphic types)).
We have talked a little (I think Niko has thought more) about perhaps changing the relationship between subtyping and type inference. Perhaps not all subtyping should be taken into account by the type inference algorithm. And/or perhaps some coercions should be taken account of. I don't really know - I have a hard time visualising how type checking would be affected by these changes.
I feel like I should have a point to make now, but I don't. I just did a lot of thinking to clarify all this in my head, so I thought I should write it down. And who knows? It might be helpful or interesting to someone else too.
4 comments:
Type Casts lead to Coercions
Coercions lead to implicits
Implicits lead to Scala
getting us is unique idea you can save time by getting our services under your roof only bella can creat such magic.
great post
Hello niice blog
Post a Comment