Covariance and contravariance are intimately related to "mapping" and only incidentally related to subtype polymorphism. In particular, if we assume we have a function

    coerce : a -> b

which can only be applied when a is a subtype of b then we can dispense with subtyping entirely through explicit coercion.

Now, covariance occurs when you can "map" over a structure "in the same direction".

    mapCovariant : (a -> b) -> (f a -> f b)

while contravariance occurs when maps "flip"

    mapContravariant : (a -> b) -> (f b -> f a)

and we get the subtyping relationship naturally from applying coerce

    covariantCoerce = mapCovariant coerce
    contravariantCoerce = mapContravariant coerce

Now all of this only applies "mathematically" where things are necessarily constant. This implies that we ought to think of mapCovariant and mapContravariant as working on "transformations of data" instead of operating imperatively.

In the event that we have mutability then we can violate covariance and contravariance as noted. Really, though, this is a consequence of a larger problem.

In any mutable type we can apply a transformation on that type while maintaining all references to it

    a = [1, 2, 3];
    a.mapCovariant(fun (x) -> repeat "a" x);

    // a : [String]
    // a == ["a", "aa", "aaa"]

If we're adamant about treating things as transformations then functions like mapCovariant cannot operate mutably since they allow the changing of a generic type.

Mutation invariably involves....invariance. There are many ways of looking at this, here is mine: If a := b and a.F := c, then we must assume b.F := c is possible. However, such edges are not tractable in a type system, so we conservatively rely on invariance instead.

Agreed. (Syntactic) types are exactly incoherent with the kind of "spooky action at a distance" that mutability enables. Semantic type layers could do more, perhaps.

I've got a whole type system going based on non-syntactic types that supports aggressive type inference in the presence of subtyping. It uses type trees rather than coercions, and types are built based on observation. Will write more aboit it soon.

Sounds really interesting! I look forward to seeing more

This is a fantastic explanation of covariance and contravariance. Much better than most explanations I've seen from the Scala community.

f-bounded types (such as in the article) still leave properties to be desired, however: http://tpolecat.github.io/2015/04/29/f-bounds.html

Interfaces have variance too, as long as they give rise to a subtyping relationship (which, in most languages that have them, they do).

Ha! Cunningham's law.

I see that many OOP languages (of various purity) have interfaces that may be extended by other interfaces. Is that what you're talking about?

I also found that *variance is used in the context of Haskell, but it seems to be far from being widely used.

Haskell being my template of a language with a good-looking interplay of polymorphism and algebraic typing.

variance is used in Haskell all the time. Haskell's subtyping/type-subsumption relation is less pervasive than an OO language's, but it's critical. Furthermore, variance is more fundamental than subtyping. It is not at all a stretch to say that the type mechanics of function composition are based on contravariance/covariance matching.