有人可以解释类型协变/逆变和范畴论之间的联系吗？
我刚刚开始阅读范畴论，如果有人能解释 CS 逆变/协变和范畴论之间的联系，我将非常感激。一些示例类别是什么（即它们的对象/态射是什么？）？提前致谢？
I am just starting to read about category theory, and would very much appreciate it if someone could explain the connection between CS contravariance/covariance and category theory. What would some example categories be (i.e. what are their objects/morphisms?)? Thanks in advance?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
Going Deep Channel in Microsoft Channel9 中提供了有关逆变/协方差的精彩视频。您可以从这里开始：
There are very nice videos about contravariance/covariance in Going deep channel in Microsoft Channel9. You can start here:
从 $C$ 到 $D$ 的逆变函子与从 $C$ 到 $D^{op}$ 的正常（即协变）函子完全相同，其中 $D^{op}$ 是 $D$ 的相反类别。因此，最好首先理解相反的类别——然后你就会自动理解逆变函子！
逆变函子在计算机科学中并不经常出现，尽管我可以想到两个例外：
您可能听说过子类型上下文中的逆变。尽管这在技术上是同一个术语，但联系确实非常薄弱。在面向对象编程中，类形成偏序；每个偏序都是一个具有“二元 hom 集”的类别——给定任意两个对象 $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 |- Int ---------- ...... ---------- A |- Int它是态射 $(B\vdash Int)\to(A\ vdash Int)$ -- 注意方向的变化。基本上这就是说，如果你有一个将 A 转换为 B'a 的函数，以及一个带有 B 类型自由变量 x 的 Int 类型表达式，那么你可以用“let x = fy in . .." 并得到一个仍为 Int 类型的表达式，但其唯一的自由变量为 $A$ 类型，而不是 $B$ 类型。
A contravariant functor from $C$ to $D$ is the exact same thing as a normal (i.e. covariant) functor from $C$ to $D^{op}$, where $D^{op}$ is the opposite category of $D$. So it's probably best to understand opposite categories first -- then you'll automatically understand contravariant functors!
Contravariant functors don't come up all that often in CS, although I can think of two exceptions:
You may have heard of contravariance in the context of subtyping. Although this is technically the same term, the connection is really, really weak. In object oriented programming, the classes form a partial order; every partial order is a category with "binary hom-sets" -- given any two objects $A$ and $B$, there is exactly one morphism $A\to B$ iff $A\leq B$ (note the direction; this slightly-confusing orientation is the standard for reasons I won't explain here) and no morphisms otherwise.
Parameterized types like, say, Scala's PartialFunction[-A,Unit] are functors from this simple category to itself... we usually focus on what they do to objects: given a class X, PartialFunction[X,Unit] is also a class. But functors preserve morphisms too; in this case if we had a subclass Dog of Animal, we would have a morphism Dog$\to$Animal, and the functor would preserve this morphism, giving us a morphism PartialFunction[Animal,Unit]$\to$PartialFunction[Dog,Unit], telling us that PartialFunction[Animal,Unit] is a subclass of PartialFunction[Dog,Unit]. If you think about that, it makes sense: suppose you have a situation where you need a function that works on Dogs. A function that works on all Animals would certainly work there!
That said, using full-on category theory to talk about partially ordered sets is big-time overkill.
Less common, but actually uses the category theory: consider the category Types(Hask) whose objects are the types of the Haskell programming language and where a morphism $\tau_1\to\tau_2$ is a function of type $\tau_1$->$\tau_2$. There is also a category Judgments(Hask) whose objects are lists of typing judgments $\tau_1\vdash\tau_2$ and whose morphisms are proofs of all the judgments on one list using the judgments on the other list as hypotheses. There is a functor from Types(Hask) to Judgments(Hask) which takes a Types(Hask)-morphism $f:A\to B$ to the proof
B |- Int ---------- ...... ---------- A |- Intwhich is a morphism $(B\vdash Int)\to(A\vdash Int)$ -- notice the change of direction. Basically what this is saying is that if you've got a function that turns A's into B'a, and an expression of type Int with a free variable x of type B, then you can wrap it with "let x = f y in ..." and arrive at an expression still of type Int but whose only free variable is of type $A$, not $B$.