Covariance and Controvariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers)

TL;DR

This paper revisits the concepts of covariance and contravariance in type systems, explaining their theoretical foundations and implementation techniques to both students and language designers, highlighting their coexistence and practical relevance.

Contribution

It provides a modern reexamination of covariance and contravariance in type theory, with simplified explanations and insights into advanced implementation techniques.

Findings

Reaffirmed that covariance and contravariance can coexist in programming languages.

Provided simplified explanations of complex type-theoretic concepts.

Shared undocumented advanced techniques used in compiler implementations.

Abstract

Twenty years ago, in an article titled "Covariance and contravariance: conflict without a cause", I argued that covariant and contravariant specialization of method parameters in object-oriented programming had different purposes and deduced that, not only they could, but actually they should both coexist in the same language. In this work I reexamine the result of that article in the light of recent advances in (sub-)typing theory and programming languages, taking a fresh look at this old issue. Actually, the revamping of this problem is just an excuse for writing an essay that aims at explaining sophisticated type-theoretic concepts, in simple terms and by examples, to undergraduate computer science students and/or willing functional programmers. Finally, I took advantage of this opportunity to describe some undocumented advanced techniques of type-systems implementation that are known only to few insiders that dug in the code of some compilers: therefore, even expert language designers and implementers may find this work worth of reading.