может ли кто-нибудь объяснить связь между ковариантностью/контравариантностью типов и теорией категорий?

Контравариантный функтор из $C$ в $D$ — это то же самое, что и нормальный (т.е. ковариантный) функтор из $C$ в $D^{op}$, где $D^{op}$ — категория, противоположная $D$. Так что, вероятно, лучше сначала понять противоположные категории — тогда вы автоматически поймете контравариантные функторы!

Контравариантные функторы не так часто встречаются в CS, хотя я могу вспомнить два исключения:

1. Возможно, вы слышали о контравариантности в контексте подтипирования. Хотя технически это один и тот же термин, связь действительно очень слабая. В объектно-ориентированном программировании классы формируют частичный порядок; каждый частичный порядок является категорией с «бинарными хом-множествами» — для любых двух объектов $A$ и $B$ существует ровно один морфизм $A\to B$ тогда и только тогда, когда $A\leq B$ (обратите внимание на направление; эта немного запутанная ориентация является стандартом по причинам, которые я не буду здесь объяснять) и никаких морфизмов в противном случае.

   Параметризованные типы, такие как, скажем, PartialFunction[-A,Unit] в Scala, являются функторами из этой простой категории для самого себя... мы обычно фокусируемся на том, что они делают с объектами: учитывая класс X, PartialFunction[X,Unit] также является классом . Но функторы также сохраняют морфизмы; в этом случае, если бы у нас был подкласс Dog от Animal, у нас был бы морфизм Dog$\to$Animal, и функтор сохранил бы этот морфизм, дав нам морфизм PartialFunction[Animal,Unit]$\to$PartialFunction[Dog, Unit], сообщая нам, что PartialFunction[Animal,Unit] является подклассом PartialFunction[Dog,Unit]. Если подумать, в этом есть смысл: предположим, у вас есть ситуация, когда вам нужна функция, которая работает на Dogs. Функция, которая работает со всеми животными, безусловно, будет работать и там!

   Тем не менее, использование полной теории категорий, чтобы говорить о частично упорядоченных множествах, является излишним.

2. Менее распространен, но на самом деле использует теорию категорий: рассмотрим категорию Types(Hask), объекты которой являются типами языка программирования Haskell и где морфизм $\tau_1\to\tau_2$ является функцией типа $\tau_1$-> $\тау_2$. Существует также категория суждений (Hask), объектами которой являются списки суждений о типах $\tau_1\vdash\tau_2$, а морфизмами которых являются доказательства всех суждений из одного списка с использованием суждений из другого списка в качестве гипотез. Существует функтор от Types(Hask) к Judgments(Hask), который переводит Types(Hask)-морфизм $f:A\to B$ в доказательство

     B |- Int
    ----------
      ......
    ----------
     A |- Int

который является морфизмом $(B\vdash Int)\to(A\vdash Int)$ -- обратите внимание на изменение направления. По сути, это говорит о том, что если у вас есть функция, которая превращает A в B'a, и выражение типа Int со свободной переменной x типа B, то вы можете обернуть это выражением «let x = f y in . .." и получить выражение по-прежнему типа Int, но единственная свободная переменная которого имеет тип $A$, а не $B$.

Есть очень хорошие видеоролики о контравариантности/ковариантности в канале Going Deep в Microsoft Channel9. Вы можете начать здесь:

• E2E: Брайан Бекман и Эрик Мейер — Co/Contravariance in Physics and Programming, 1 из 3
• E2E: Брайан Бекман и Эрик Мейер — Co/Contravariance in Physics and Programming, 2 of 3
• E2E: Брайан Бекман и Эрик Мейер — Co/Contravariance in Physics and Programming, 3 of n
• E2E: Джем-сессия на белой доске с Брайаном Бекманом и Грегом Мередитом - Монады и системы координат