13

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?

4

2 回答 2

9

从 $C$ 到 $D$ 的逆变函子与从 $C$ 到 $D^{op}$ 的正常（即协变）函子完全相同，其中 $D^{op} $是$D$。所以最好先理解相反的类别——然后你就会自动理解逆变函子！

逆变函子在 CS 中并不经常出现，尽管我能想到两个例外：

  1. 您可能听说过子类型化上下文中的逆变。尽管这在技术上是同一个术语，但这种联系真的非常非常弱。在面向对象编程中，类形成偏序；每个偏序都是具有“二进制 hom 集”的类别——给定任意两个对象 $A$ 和 $B$，当 $A\leq B$ 时，恰好存在一个态射 $A\to 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 的函数。适用于所有动物的功能肯定会在那里工作！

    也就是说，使用完整的范畴论来讨论偏序集是非常过分的。

  2. 不太常见，但实际上使用类别理论：考虑类别 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)-morphism $f:A\to B$ 用于证明

     B |- 诠释
    ----------
      ……
    ----------
     A |- 整数

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

于 2011-05-02T00:13:08.863 回答