Show notes

VARIANCE IN TYPE SYSTEMS

What languages do you use? Are they typed? How are they typed?

Strong vs Static types

Type system: a program. logic assigned by the programmer to represent all valid states a program can be in. This happens statically / at compile time. No need to actually run the program. Formalizes the logic any runtime variant of a program accepts

SOUNDNESS: If the type system says it’s valid, then the runtime is valid COMPLETENESS: If the type system says it’s invalid, then the runtime isn’t valid

Ideally a type system is perfectly sound AND valid, but throwback to incompleteness theorems, we know that it can never be sure of 100% completeness.

Everything is straight-forward when you don’t with simple types.

Variance describes the rules of subtyping in a type system when dealing with higher-kinded types like arrays, maps, and functions, which themselves relate to an inner type.

Strangeloop 2019 “Typing the Untyped: Soundness in Gradual Type Systems” by Ben Weissmann

All Possible Types of Variance

The following is a description of all types of variances as they relate to the Array higher-kinded type. Some of these do not make sense for arrays, or are not desirable for arrays, but they may be so for other types. We’re just using arrays here as an example to illustrate all possible types.

Covariance

Square is a subtype of Shape, so [Square] is a subtype of [Shape]

Contravariance

Square is a subtype of Shape, so [Shape] is a subtype of [Square]

Invariance

Square is a subtype of Shape, but [Square] is completely unrelated to and distinct from [Shape]

Bivariance

Square is a subtype of Shape, so [Square] is both a subtype and supertype of [Shape]

Variance Rules

Generally speaking:

  • Producers are covariant
    • Function return types are producers, so they’re covariant in their return types
  • Consumers are contravariant
    • Function argument types are consumers, so they’re contravariant in their argument types.
  • Arrays and hashmaps are usually invariant. However, if you guarantee that your array is:
    • only a producer (aka. read-only), then it can be covariant
    • only a consumer (aka. write-only), then it can be contravariant
      • … but practically speaking, if something is writeable, then it’s also readable

These rules are derived solely based on their substitutability. More examples below!

Producers

  • Let’s look at this hierarchy: Entertainment > Music > Metal

  • Now let’s look at the producers of these types: Producer of Entertainment > Producer of Music > Producer of Metal

  • If you consume some Entertainment, you can ask a Producer of Entertainment, a Producer of Music, or a Producer of Metal, and nothing can go wrong.
  • If you consume Music, you can ask a Producer of Music, or a Producer of Metal, and nothing can go wrong.
  • If you consume Metal, you can ask a Producer of Metal, and nothing can go wrong.

Consumers

  • Let’s look at this hierarchy: Enery Sources > Vegetables > Bamboo

  • Now let’s look at the consumers of these types: Consumer of Enery Sources < Consumer of Vegetables < Consumer of Bamboo

  • If you produce some Energy Sources, you can ask a Consumer of Energy Sources, and nothing can go wrong.
  • If you produce some Vegetables, you can ask a Consumer of Energy Sources, or a Consumer of Vegetables, and nothing can go wrong.
  • If you produce some Bamboo, you can ask a Consumer of Energy Sources, a Consumer of Vegetables, or a Consumer of Bamboo, and nothing can go wrong.

Arrays and Hashes

Let’s say we have the following structure.

  Shape (parent or interface)
 /     \
Square  Circle (children)

Arrays are invariant because they cannot be covariant or contravariant:

  • Unsound with covariance: Function accepts [Shape] in parameter position, and [Square] is passed on invocation as an argument. This is unsound, because since the function accepts a [Shape], it could add a Circle to the array, but the array was initially declared of type [Square].
  • Unsound with contravariance: Function accepts [Square] in parameter position, and [Shape] is passed on innovation as an argument. This is unsound, because the function can only read Squares, but since we pass a [Shape], we’re able to supply a [Circle].
  • Unsound with bivariance: Arrays are unsound with bivariance because they are unsound with either covariance or contravariance.