Last updated on Friday, December 13, 2024

Variance and polymorphism recap

Explaining variance systematically is not in scope for CS-214: we just want you to develop an intuition of why variance rules exist, and what issues they prevent. However, since some of you have asked for details, here is a complete write-up!

The first thing to know about is subtyping. Scala has a type hierarchy, like Java. A is a subtype of B, written A <: B, iff values of type A can be used in all contexts where values of type B can be used. For example, a String can be used anywhere an Object is expected, so String <: Object.

In particular, if A <: B, then a variable of type B can hold a value of type A. (I like to think as “type A is more specific than type B”)

<: is a relation between types. Like any other relation, we can define it by giving its axioms (for example ≤ on ℕ is a relation between natural numbers, and its axioms are ∀ n, n ≤ n and ∀ m, n ≤ m ⇒ n ≤ m + 1).

What are the axioms for <:? There are two axioms to make the relation reflexive and transitive, plus one for each way to form a type. I have given each of the rules below a name in [square brackets], to make them easier to refer to:

Relation axioms:

[Ref] ∀ A, A <: A (reflexivity, e.g. Int <: Int)
[Tr] ∀ A B C, A <: B && B <: C ⇒ A <: C (transitivity, e.g. Cons[Int] <: List[Int] and List[Int] <: Iterable[Int] hence Cons[Int] <: Iterable[Int])

Axioms for simple types:

[Ext] If A[T1, ..., Tn] extends B[Q1, ..., Qn] then A[T1, ..., Tn] <: B[Q1, ..., Qn]
[Fn] If A >: a and b <: B then A => b <: a => B (the “robustness principle”; we say that functions are contravariant in their inputs and covariant in their output)

You can check that these axioms are consistent with the principle that A <: B iff values of type A can be used in all contexts where values of type B can be used.

But wait! I didn’t include any axioms about generic types! Let me make one first attempt (I’ve omitted the rules for some advanced type system features that we have not studied yet):

Axioms for generics

For some classes C, if A <: B then C[A] <: C[B] (in that case we say that C is covariant in T)
For some other classes C, if A >: B then C[A] <: C[B] (in that case we say that C is contravariant in T)
More generally, for some classes C, if each of A1 and B1, …, An and Bn verify one of either <: or :>, then C[A1, ..., An] <: C[B1, ..., Bn]

“Some classes” is not precise. I can try to be more specific…

[C+] If C[T] is covariant in T and A <: B, then C[A] <: C[B]
[C-] If C[T] is contravariant in T and if A >: B, then C[A] <: C[B]
[Cls] (Same thing generalized to multiple parameters, requiring each pair to be in the right direction)

… but this doesn’t help: we need rules to tell us when a class is covariant or contravariant in a parameter. In Scala, we ask the user to declare it using variance annotations (+T, -T), and we then check whether the annotations are consistent with our principle: A <: B iff values of type A can be used in all contexts where values of type B can be used.

So, the rules:

[Cov] A +X parameter of a type C[+X] can only appear in covariant positions in the types of its public fields, functions, in type bounds, and in the types it extends.
[Contra] A -X parameter of a type C[-X] can only appear in contravariant positions in the types of its public fields, functions, in type bounds, and in the type it extends.

You may see where this is going: “appears in covariant position” is a relation! Here are its axioms:

We say that X appears in covariant position in T if any of the following are true:

[CovOut] T is a type of the form A => X (e.g. Int => X)
[CovCls] T is a type of the form C[X], and C is declared as C[+A]
[CovSup] T is a bound of the form A >: X (e.g. def f[A >: X](a: A): Unit)
[CovCov] X appears in covariant position in Y, and Y appears in covariant position in T (just like in math: + × + == +)
[ContraContra] X appears in contravariant position in Y, and Y appears in contravariant position in T (- × - == +)

We say that X appears in contravariant position in T if any of the following are true:

[ContraIn] T is a type of the form X => A (e.g. X => Int)
[ContraCls] T is a type of the form C[X], and C is declared as C[-A]
[ContraSub] T is a bound of the form A <: X (e.g. def f[A <: X](c: C): Unit)
[CovContra] X appears in covariant position in Y, and Y appears in contravariant position in T (+ × - == -)
[ContraCov] X appears in contravariant position in Y, and Y appears in covariant position in T (- × + == -)

Remember: all appearances of a type must be consistent with its annotation.

There is an intuition behind these rules: variance annotations allow us to treat an instance of a class as having multiple different types (e.g. a variable of type List[String] also has type List[Object] and List[Any]), and we must make sure that all usages of the class (calling methods, reading fields) are compatible with all these types. Furthermore, the function rules are a special case of the class ones (A => B is just Function[-A, +B]).

That’s it! That’s all we’ve covered up to this point in the class. The rules guarantee the soundness of the type system, which is to say that they prevent type errors. The exercises I posted on variance earlier show many examples of ways in which things could go wrong if these rules were not in place. The exercise essentially fall into two categories:

Is XYZ a subtype of ABC? ⇒ For these use the <: axioms above. Or use the nice trick below.
Is this class definition well formed? ⇒ For these use the the Cov/Contra rules above.

Nice trick: Once you understand the rules about covariant and contravariant positions well, you can use the following trick for subtyping questions: to show that ABC is a subtype of XYZ, you need to find a path ABC <: ABC1 <: ABC2 <: … <: XYZ such that each step is either:

An application of the [Ext] rule (e.g. Cons[Int] <: List[Int])
A substitution where any type a in covariant position may be replaced by a type A :> a and any type B in contravariant position may be replaced by a type b <: B (e.g. Object => List[Int] <: String => List[Any])

Unfortunately I won’t have time to redo all the exercises from the midterms and exercise sheets and questions to clearly show how these rules apply to them. If you do it on any of these examples, please do post a comment below. If you have trouble with a specific example, please make a post below showing the exact steps you applied and where you got stuck, and we’ll help. In the meantime, there are some examples below that you can copy in a worksheet:

For covariant and contravariant positions:

trait T[+A, -B]

trait T0[+X] extends T[Int, X]
// Error: covariant type B occurs in contravariant position in type T[Int, B]

trait T1[+X] extends T[X, Int]
// OK

trait T2[+X] extends T[T[X, Int], Int]
// OK

trait T3[+X] extends T[T[Int, X], Int]
// Error: covariant type X occurs in contravariant position in type T[T[Int, X], Int]

trait T4[+X] extends T[Int, T[X, Int]]
// Error: covariant type X occurs in contravariant position in type T[Int, T[X, Int]]

trait T5[+X] extends T[Int, T[Int, X]]
// OK

trait Q0[-X] extends T[Int, X]
// OK

trait Q1[-X] extends T[X, Int]
// Error: contravariant type X occurs in covariant position in type T[X, Int]

trait Q2[-X] extends T[T[X, Int], Int]
// contravariant type X occurs in covariant position in type T[T[X, Int], Int]

trait Q3[-X] extends T[T[Int, X], Int]
// OK

trait Q4[-X] extends T[Int, T[X, Int]]
// OK

trait Q5[-X] extends T[Int, T[Int, X]]
// contravariant type X occurs in covariant position in type T[Int, T[Int, X]]

class C0[-A](val x: A)
// Error: contravariant type A occurs in covariant position in type A of value x

class C1[-A](val x: Int => A)
// Error: contravariant type A occurs in covariant position in type Int => A of value x

class C2[-A](val x: A => Int)
// OK

class C3[-A](val x: A => Int => Int)
// OK

class C4[-A](val x: (A => Int) => Int)
// Error: contravariant type A occurs in covariant position in type (A => Int) => Int of value x

class D0[+A](val x: A)
// OK

class D1[+A](val x: Int => A)
// OK

class D2[+A](val x: A => Int)
// Error: covariant type A occurs in contravariant position in type A => Int of value x

class D3[+A](val x: A => Int => Int)
// Error: covariant type A occurs in contravariant position in type A => Int => Int of value x

class D4[+A](val x: (A => Int) => Int)
// OK

trait E0[+T] { def f(t: T): Unit }
// Error: covariant type T occurs in contravariant position in type T of parameter t

trait E1[+T] { def f(): T }
// OK

trait E2[+T] { def f(g: T => Int): Unit }
// OK

trait E3[+T] { def f(g: Int => T): Unit }
// Error: covariant type T occurs in contravariant position in type Int => T of parameter g

trait U[-X, +Y]

trait V0[-X, +Y] extends U[U[X, Y], U[X, Y]]
// Error: contravariant type X occurs in covariant position in type U[U[X, Y], U[X, Y]]

trait V1[-X, +Y] extends U[U[Y, X], U[X, Y]]
// OK

trait W0[+A]:
  def f0(): A // OK
  def f1(a: A): Unit // Error: covariant type A occurs in contravariant position in type A of parameter a
  def f2(a: Int => A): Unit // Error: covariant type A occurs in contravariant position in type Int => A of parameter a
  def f3(a: A => Int): Unit // OK
  def g00(): T[A, Int] // OK
  def g01(): T[Int, A] // Error: covariant type A occurs in contravariant position in type (): T[Int, A] of method g01
  def g10(a: T[A, Int]): Unit // Error: covariant type A occurs in contravariant position in type T[A, Int] of parameter a
  def g11(a: T[Int, A]): Unit // OK
  def g20(a: Int => T[A, Int]): Unit // Error: covariant type A occurs in contravariant position in type Int => T[A, Int] of parameter a
  def g21(a: Int => T[Int, A]): Unit // OK
  def g30(a: T[A, Int] => Int): Unit // OK
  def g31(a: T[Int, A] => Int): Unit // Error: covariant type A occurs in contravariant position in type T[Int, A] => Int of parameter a

trait W1[-A]:
  def f0(): A // Error: contravariant type A occurs in covariant position in type (): A of method f0
  def f1(a: A): Unit // OK
  def f2(a: Int => A): Unit // OK
  def f3(a: A => Int): Unit // Error: contravariant type A occurs in covariant position in type A => Int of parameter a
  def g00(): T[A, Int] // Error: contravariant type A occurs in covariant position in type (): T[A, Int] of method g00
  def g01(): T[Int, A] // OK
  def g10(a: T[A, Int]): Unit // OK
  def g11(a: T[Int, A]): Unit // Error: contravariant type A occurs in covariant position in type T[Int, A] of parameter a
  def g20(a: Int => T[A, Int]): Unit // OK
  def g21(a: Int => T[Int, A]): Unit // Error: contravariant type A occurs in covariant position in type Int => T[Int, A] of parameter a
  def g30(a: T[A, Int] => Int): Unit // Error: contravariant type A occurs in covariant position in type T[A, Int] => Int of parameter a
  def g31(a: T[Int, A] => Int): Unit // OK

trait W2[+A]:
  def f0[C <: A](c: C): Unit // covariant type A occurs in contravariant position in type  <: A of type C
  def f1[C >: A](c: C): Unit // OK
  def f00[C <: T[A, Int]](c: C): Unit // covariant type A occurs in contravariant position in type  <: T[A, Int] of type C
  def f01[C <: T[Int, A]](c: C): Unit // OK
  def f10[C >: T[A, Int]](c: C): Unit // OK
  def f11[C >: T[Int, A]](c: C): Unit // covariant type A occurs in contravariant position in type  >: T[Int, A] of type C

For subtyping:

trait F[-X, +Y]
trait G[-X, +Y] extends F[F[Y, X], F[X, Y]] // G[X, Y] <: F[F[Y, X], F[X, Y]]
trait H[-X, +Y] extends G[X, Y] // H[X, Y] <: G[X, Y]

class A extends B // A <: B
class B extends C // B <: C
class C // A <: B <: C

class Examples:
  val x0: B => G[B, B]

  val x1: A => G[A, C] = x0 // OK since (B => G[B, B]) <: (A => G[A, C])
  val x2: C => G[B, B] = x0 // Error due to B <: C replacement in contravariant pos.
  val x3: B => G[C, B] = x0 // Error due to B <: C replacement in contravariant pos.
  val x4: B => G[B, A] = x0 // Error due to A >: B replacement in covariant pos.

  val y0: G[B, B] => B

  val y1: G[C, A] => C = y0 // OK since (G[B, B] => B) <: (G[C, A] => C)
  val y2: G[B, B] => A = y0 // Error due to B >: A replacement in covariant pos.
  val y3: G[A, B] => B = y0 // Error due to B >: A replacement in covariant pos.
  val y4: G[B, C] => B = y0 // Error due to B <: C replacement in contravariant pos.

  val z0: G[B, B] => G[B, B]
  val z1: H[B, B] => F[F[B, B], F[B, B]] = z0 // OK by [Ext] and [Fn] rules
  val z2: H[C, A] => F[F[C, A], F[A, C]] = z1 // OK

A concrete example: Let’s take y3 above. We start from y0: G[B, B] => B. To assign it to y3: G[A, B] => B we need to prove that G[B, B] => B <: G[A, B] => B.

Technique 1, using the axioms:

      (G[B, B] => B) <: (G[A, B] => B)
<===>  G[B, B]       >:  G[A, B]        (by [Fn])
<===>    B           <:    A            (by [Cls])

We have A <: B, not B <: A, so this relation does not hold.

Technique 2, using the trick

To replaceA <: B, so we can replace B with A in contravariant positions. The first B is in covariant position in G[B, B] => B, so the replacement is illegal.

The proofs for z2 is similar, and the proof for z1 requires invoking the [Ext] rule in addition.