有人能解释类型协方差/逆方差和范畴理论之间的联系吗?

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 $D元。So it's probably best to understand opposite categories first -- then you'll automatically understand contravariant functors!

在CS中,反变函数并不经常出现,尽管我可以想到两个例外:

1. 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.

2. 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 |- Int

这是一个变形$(b\vdash int)到(a\vdash int)$注意方向的改变。基本上,这是说,如果你有一个函数,将a变成b'a,并且有一个int类型的表达式,有一个b类型的自由变量x,那么你可以用“let x=f y in…”来包装它,得到一个仍然是int类型,但唯一的自由变量是$A$类型,而不是$B$类型的表达式。

有非常好的视频关于反方差/协方差 Going deep channel in Microsoft Channel9 . You can start here:

• E2E: Brian Beckman and Erik Meijer - Co/Contravariance in Physics and Programming, 1 of 3
• E2E: Brian Beckman and Erik Meijer - Co/Contravariance in Physics and Programming, 2 of 3
• E2E: Brian Beckman and Erik Meijer - Co/Contravariance in Physics and Programming, 3 of n
• E2E: Whiteboard Jam Session with Brian Beckman and Greg Meredith - Monads and Coordinate Systems