Контравариантный функтор от $ C $ до $ D $ - это то же самое, что нормальный (т. Е. Ковариантный) функтор от $ C $ до $ D ^ {op} $, где $ D ^ {op} $ - это противоположная категория из $ D $.Так что, вероятно, лучше сначала понять противоположные категории - тогда вы автоматически поймете контравариантные функторы!
Контравариантные функторы не так часто встречаются в CS, хотя я могу вспомнить два исключения:
Возможно, вы слышали о контравариантности в контексте подтипов.Хотя это технически один и тот же термин, связь действительно очень слабая.В объектно-ориентированном программировании классы образуют частичный порядок;каждый частичный порядок является категорией с «бинарными множествами гомов» - для любых двух объектов $ A $ и $ B $ существует ровно один морфизм $ A \ to B $ тогда и только тогда, когда $ A \ leq B $ (обратите внимание на направление;эта слегка сбивающая с толку ориентация является стандартом по причинам, которые я не буду здесь объяснять), а в противном случае нет морфизмов.
Параметризованные типы, такие как, скажем, функция PartialFunction Scala [-A, Unit], являются функторами из этой простой категории.... мы обычно фокусируемся на том, что они делают с объектами: учитывая класс X, PartialFunction [X, Unit] также является классом.Но функторы также сохраняют морфизмы;в этом случае, если бы у нас был подкласс Dog of Animal, у нас был бы морфизм Dog $ \ to $ Animal, и функтор сохранял бы этот морфизм, давая нам морфизм PartialFunction [Animal, Unit] $ \ to $ PartialFunction [Dog,Unit], сообщая нам, что PartialFunction [Animal, Unit] является подклассом PartialFunction [Dog, Unit].Если вы думаете об этом, это имеет смысл: предположим, у вас есть ситуация, когда вам нужна функция, которая работает на Dogs.Функция, которая работает на всех животных, безусловно, будет работать там!
Тем не менее, использование полной теории категорий для разговоров о частично упорядоченных множествах - это слишком много.
Менее распространенный, но на самом деле использует теорию категорий: рассмотрим категорию Types (Hask), чьи объекты являются типами языка программирования Haskell и где морфизм $ \ tau_1 \ to \ tau_2 $ является функцией типа $ \ tau_1 $ -> $ \ tau_2 $.Существует также категория «Суждения» (Hask), объектами которой являются списки типизированных суждений $ \ tau_1 \ vdash \ tau_2 $ и морфизмы которых являются доказательствами всех суждений в одном списке с использованием суждений в другом списке в качестве гипотез.Существует функтор от Types (Hask) к суждениям (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 = fy in... "и получим выражение еще типа Int, но единственная свободная переменная которого имеет тип $ A $, а не $ B $.