|
|
Пишет Journal de Chaource (![[info]](http://lj.rossia.org/img/syndicated.gif){kind=small} lj_chaource)@ 2021-08-17 08:49:00 |
 |
|
 |
|
|
|
|
|
|
 |
|
 |
Covariance, contravariance, and subtyping
1. "Covariance" and "contravariance" are properties of a type constructor that follow automatically from the definition of the type constructor. A type constructor is covariant if a `map` function exists and satisfies the functor laws, and contravariant if `contramap` exists and satisfies the contrafunctor laws. If neither `map` nor `contramap` function can be found (e.g., because the type signature cannot be implemented or because the laws cannot be satisfied), the type constructor is neither covariant nor contravariant.
Covariance and contravariance are not labels arbitrarily chosen by the programmer. In Scala, one can declare List[A] without covariance but Option[+A] with covariance. But this makes no sense. List[_] is covariant according to its definition because a `map` function exists with correct properties. It is a problem if the compiler does not recognize the covariance of List[_] automatically.
2. "Subtyping" is a relation between types that requires to have an automatic conversion from one type to another. If A is a subtype of B (we write A <: B), the compiler will automatically insert a conversion function from A to B whenever it is necessary.
If a function `f` is defined to have an argument of type `B`, but the programmer writes `f(x)` where `x` has type `A`, then the compiler will automatically insert a conversion function (say, `a2b` of type A => B) and rewrite `f(x)` into `f(a2b(x))`.
Each compiler defines in its own way what types will be subtypes of others. In Scala, the programmer is able to define an implicit conversion between arbitrary types. So, Scala supports essentially arbitrary subtyping relations. Whether they are useful is up to the programmer.
3. If we have a subtyping relation A <: B and a covariant type constructor F[_], the subtyping relation between F[A] and F[B] is automatically established through the `map` function. In other words, we have a type conversion function F[A] => F[B] as `_.map(a2b)`. Similarly for contravariant type constructors.
4. I realized that the interpretation of subtyping as subsets or supersets is incorrect. Here are the details.
Types can be understood as sets of allowed values that a variable might have in a program. For example, the type `Int` is the set of all 32-bit integers. The type `Boolean` is the set of two elements `{false, true}`. The type `String` is the set of all character sequences (which can be arbitrarily long but finite; we assume a computer with unbounded memory). We can avoid problems with sets that are "too large" by a simple trick: we do not allow all functions but only functions with a finitely long implementation code. So, the type `String => String` is not the (uncountable) set of all functions from String to String, but the set of all functions that can be implemented via a finitely long program code. The set of such functions is countably infinite. With this trick, all types in a programming language are viewed as either finite sets or countably infinite sets.
If we have a subtyping relation A <: B and we interpret A and B as sets, it is not true that A must be a superset of B, or that A must be a subset of B. It may be true in some cases but not in other cases. Here are the main examples and counterexamples:
Example with subtypes being subsets: The type Option[A] is defined as Some[A] or None. The type Some[A] is a subtype of Option[A]. For a fixed `A`, the set of all values of type Some[A] is a subset of all values of type Option[A].
Remark: here "X is a subset of Y" means that there is an injective map from X to Y. Similarly with supersets. X is a superset of Y if and only if Y is a subset of X.
Examples with subtypes being supersets: Function types are contravariant in the first argument. So, the type of functions Option[A] => Boolean (an example of such a function is `_.nonEmpty`) is a subtype of the type of functions Some[A] => Boolean. The set of all functions of type Option[A] => Boolean is a superset of the set of functions of type Some[A] => Boolean, because the type Option[A] => Boolean is equivalent to a pair (Some[A] => Boolean, None => Boolean). And the set of pairs (x, y), where x is from X and y is from Y, is a superset of the set of all x from X.
Another example of superset is given by object-oriented inheritance, or inheritance of "structural types" or "records". A record {a: A, b: B, c: C} is a subtype of {a: A, b: B} because we can drop the value `c` and convert the first type into the second one. Equivalently, the tuple (A, B, C) is a subtype of (A, B) because we can obtain a conversion function of type ((A, B, C)) => (A, B) by dropping the third value. The set of all triples (A, B, C) is a superset of the set of pairs (A, B).
Example of neither subset nor superset: As the two preceding examples show, we can have a situation where A <: B and C <: D while A is a subset of B but C is a superset of D. Then the types of pairs (A, B) and (C, D) will have a subtyping relation (A, B) <: (C, D) but there is neither a subset nor a superset relation between the sets (A, B) and (C, D).
1. "Covariance" and "contravariance" are properties of a type constructor that follow automatically from the definition of the type constructor. A type constructor is covariant if a `map` function exists and satisfies the functor laws, and contravariant if `contramap` exists and satisfies the contrafunctor laws. If neither `map` nor `contramap` function can be found (e.g., because the type signature cannot be implemented or because the laws cannot be satisfied), the type constructor is neither covariant nor contravariant.
Covariance and contravariance are not labels arbitrarily chosen by the programmer. In Scala, one can declare List[A] without covariance but Option[+A] with covariance. But this makes no sense. List[_] is covariant according to its definition because a `map` function exists with correct properties. It is a problem if the compiler does not recognize the covariance of List[_] automatically.
2. "Subtyping" is a relation between types that requires to have an automatic conversion from one type to another. If A is a subtype of B (we write A <: B), the compiler will automatically insert a conversion function from A to B whenever it is necessary.
If a function `f` is defined to have an argument of type `B`, but the programmer writes `f(x)` where `x` has type `A`, then the compiler will automatically insert a conversion function (say, `a2b` of type A => B) and rewrite `f(x)` into `f(a2b(x))`.
Each compiler defines in its own way what types will be subtypes of others. In Scala, the programmer is able to define an implicit conversion between arbitrary types. So, Scala supports essentially arbitrary subtyping relations. Whether they are useful is up to the programmer.
3. If we have a subtyping relation A <: B and a covariant type constructor F[_], the subtyping relation between F[A] and F[B] is automatically established through the `map` function. In other words, we have a type conversion function F[A] => F[B] as `_.map(a2b)`. Similarly for contravariant type constructors.
4. I realized that the interpretation of subtyping as subsets or supersets is incorrect. Here are the details.
Types can be understood as sets of allowed values that a variable might have in a program. For example, the type `Int` is the set of all 32-bit integers. The type `Boolean` is the set of two elements `{false, true}`. The type `String` is the set of all character sequences (which can be arbitrarily long but finite; we assume a computer with unbounded memory). We can avoid problems with sets that are "too large" by a simple trick: we do not allow all functions but only functions with a finitely long implementation code. So, the type `String => String` is not the (uncountable) set of all functions from String to String, but the set of all functions that can be implemented via a finitely long program code. The set of such functions is countably infinite. With this trick, all types in a programming language are viewed as either finite sets or countably infinite sets.
If we have a subtyping relation A <: B and we interpret A and B as sets, it is not true that A must be a superset of B, or that A must be a subset of B. It may be true in some cases but not in other cases. Here are the main examples and counterexamples:
Example with subtypes being subsets: The type Option[A] is defined as Some[A] or None. The type Some[A] is a subtype of Option[A]. For a fixed `A`, the set of all values of type Some[A] is a subset of all values of type Option[A].
Remark: here "X is a subset of Y" means that there is an injective map from X to Y. Similarly with supersets. X is a superset of Y if and only if Y is a subset of X.
Examples with subtypes being supersets: Function types are contravariant in the first argument. So, the type of functions Option[A] => Boolean (an example of such a function is `_.nonEmpty`) is a subtype of the type of functions Some[A] => Boolean. The set of all functions of type Option[A] => Boolean is a superset of the set of functions of type Some[A] => Boolean, because the type Option[A] => Boolean is equivalent to a pair (Some[A] => Boolean, None => Boolean). And the set of pairs (x, y), where x is from X and y is from Y, is a superset of the set of all x from X.
Another example of superset is given by object-oriented inheritance, or inheritance of "structural types" or "records". A record {a: A, b: B, c: C} is a subtype of {a: A, b: B} because we can drop the value `c` and convert the first type into the second one. Equivalently, the tuple (A, B, C) is a subtype of (A, B) because we can obtain a conversion function of type ((A, B, C)) => (A, B) by dropping the third value. The set of all triples (A, B, C) is a superset of the set of pairs (A, B).
Example of neither subset nor superset: As the two preceding examples show, we can have a situation where A <: B and C <: D while A is a subset of B but C is a superset of D. Then the types of pairs (A, B) and (C, D) will have a subtyping relation (A, B) <: (C, D) but there is neither a subset nor a superset relation between the sets (A, B) and (C, D).
