covariance - 有人可以解释类型协方差/逆变和范畴论之间的联系吗？

Question

我刚刚开始阅读范畴论，如果有人能解释 CS 逆变/协方差和范畴论之间的联系，我将非常感激。一些示例类别是什么(即它们的对象/态射是什么？)？提前致谢？

Answer 1

从 $C$ 到 $D$ 的逆变仿函数与从 $C$ 到 $D^{op}$ 的正常(即协变)仿函数完全相同，其中 $D^{op}$ 是 opposite category $D$。所以最好先理解相反的范畴——然后你就会自动理解逆变仿函数!

逆变仿函数在 CS 中并不经常出现，尽管我可以想到两个异常(exception):

您可能听说过子类型上下文中的逆变。虽然这在技术上是同一个术语，但这种联系真的非常非常弱。在面向对象编程中，类形成偏序；每个偏序都是一个带有“二元hom-sets”的范畴——给定任何两个对象$A$和$B$，只有一个态射$A\to B$ iff $A\leq B$(注意方向；这个有点令人困惑的方向是标准，原因我不会在这里解释)，否则没有态射。

参数化类型，比如 Scala 的 PartialFunction[-A,Unit] 是从这个简单类别到自身的仿函数……我们通常关注它们对对象所做的事情:给定一个类 X， PartialFunction[X,Unit] 也是一个类.但是仿函数也保留了态射；在这种情况下，如果我们有一个 Animal 的子类 Dog，我们会有一个态射 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$。还有一个类别 Judgments(Hask)，其对象是类型判断列表 $\tau_1\vdash\tau_2$，其态射是一个列表上所有判断的证明，使用另一个列表上的判断作为假设。有一个从 Types(Hask) 到 Judgments(Hask) 的仿函数，它采用 Types(Hask)-态射 $f:A\to B$ 到证明

B |- 整数
----------
......
----------
A |- 整数

这是一个态射 $(B\vdash Int)\to(A\vdash Int)$ —— 注意方向的变化。这基本上是说，如果您有一个将 A 转换为 B'a 的函数，以及一个 Int 类型的表达式和一个 B 类型的自由变量 x，那么您可以用 "let x = fy in 包装它。 ..”并得到一个仍然是 Int 类型的表达式，但它唯一的自由变量是 $A$ 类型，而不是 $B$ 类型。