面向对象语言为编程语言引入了所谓的子类型系统,简单说就是“猫是动物”、“狗是动物”,小类型(猫)可以被当作大类型(动物)用。但是对于函数本身,却有一个奇怪的不对称。

Bird Magic(Animal animal); // 使用魔法把任何一种动物伪装成鸟

假设这个函数的指针 fp 可以被传递给另外一个地方,比如下面这段代码:

Mouse jerry = new Mouse;
Animal animal = Magic(jerry); // 此处,Magic 的类型理应是接受 Mouse 返回 Animal

不难观察到,传进去的是一个相对于 Animal 更小的类型;Magic 本身返回一个小的类型 Bird,但是我们却可以把它当作大类型 Animal 去使用!也就是说,这种类型系统允许我们“传入小变大”“传出大变小”。

这样的非对称,虽然并不难以理解,但实际上却是有着深刻的道理的。换句话说,如果子类型允许我们“小变大”,那么一定会造成这样的非对称。下面,我们将试着用大炮打蚊子,使用范畴论证明这一点。

范畴

范畴论(或曰犯愁论)是一种非常抽象的学科,可以说它是抽掉一切实质内容,单纯研究对象、对象间关系及其组合的东西。最基本的东西,就是范畴了。

范畴 $\cal{C}$ 由以下两部分组成:

  1. 一些对象 $Ob(\cal C)$ 。
  2. 对象间的态射 $Arr(\cal C)$ ,比如从对象 $a$ 到对象 $b$ 的态射 $f: a \rightarrow b$ 。

简单地说,这些对象就是一些节点,而态射就是对象间的箭头。范畴要求态射满足如下条件:

  1. 对每个对象,有一个到自身的态射(恒等态射)。
  2. 有一个组合法则,可以把态射 $f: X \rightarrow Y, g: Y \rightarrow Z$ 组合起来,形成一个新态射 $g \circ f: X \rightarrow Z$ 。

注意了,这里我们没有对“对象是什么”和“态射到底是什么”做出任何论断!态射可以是函数吗?当然可以!但是并非所有态射都是函数,态射甚至可以是字符串、自然数……并且,对象 $X$ 到对象 $Y$ 的态射并不一定是唯一的。

另外还需要提醒一下,虽然这里的态射在记号上看起来非常类似函数(其实是故意的),但并非如此。虽然我们可以给“箭头”命名,但要注意,和函数的情形不同,这里一个名称只对应一个箭头。

下面举一个栗子:自然数。自然数作为范畴,可以设置成这样,只有一个对象,态射是自然数集合 0、1、2、3、……组合法则是加法。是的,态射不是函数而是一个数字……

再举一个可能更熟悉的栗子。考虑 $\bf{Set}$ 范畴,对象是所有集合,那么态射就是集合间的映射。这就是为什么态射在记号上看起来很像一般的函数。

函子

函子是我们迈出的第一步!什么是函子?函子就是范畴间的“映射”!(或者也可以叫范畴间的“函数”,反正两种说法都不严格)

不妨先回忆一下什么是函数。一个函数 $f: A \rightarrow B$ 是一系列箭头,任给一个 $A$ 里的元素,都有唯一一个发射出去的箭头到 $B$ 里的一个元素。

类比到范畴上。一个从范畴 $\cal C$ 到范畴 $\cal D$ 的 函子 $F: \cal C \rightarrow \cal D$ 满足以下条件

  1. 对于每个 $\cal C$ 里的对象 $A$ ,都有一个 $\cal D$ 中的对象 $F(A)$ 与之对应。
  2. 对于每个 $\cal C$ 里的态射 $f$ ,都有一个 $\cal D$ 中的态射 $F(f)$ 与之对应。

对于自己到自己的箭头,还有一个额外的要求:

  1. 范畴 $\cal C$ 中的对象 $A$ 的恒等态射,通过函子 $F$ 发送到范畴 $\cal D$ 上后,必须仍然是从 $F(A)$ 指向 $F(A)$ 。

换句话说,范畴 $\cal D$ 是被 $\cal C$ 和 $D$ 唯一确定的……吗?别忘了,范畴还有一个组合法则必须确定!不过在这篇文章中,不妨暂且认为这不是一个问题~

Hom 集合和 Hom 函子

如果你精通集合论,应该注意到了第一节里对范畴的定义非常不严格。什么叫“一些对象”?为什么不说“对象集合”?是的,这是一个很好的问题,因为范畴论并不要求这些对象组成集合!此外,范畴论也不要求对象间的“箭头”(态射)组成集合!不过呢,既然你精通集合论,应该知道,除了集合,那就是类了。是的,的确如此。不过,这节只考虑它们组成集合的情况。

我们可以顺藤摸瓜,研究一下对象间的箭头。比方说,固定范畴 $\cal C$ 中的对象 $X$ 和 $Y$ ,它们之间的所有箭头,如果组成集合,就写作 $Hom_{\cal C}(X,Y)$ 或 $Hom(X,Y)$ ,称为 Hom 集合 (hom-sets)。

现在不妨扣掉其中一个对象,比如说 Y,可以得到一个带一个洞的东西 $Hom(A,-)$ 。我们可以给这个洞里塞一个 $\cal C$ 里的对象,得到一个集合。事实上,我们还可以塞进去态射。

  1. 如果塞一个 $\cal C$ 的对象 $X$ 进去,就可以得到一个集合 $Hom(A,X)$ 。
  2. 如果塞一个 $\cal C$ 的态射 $f: X \rightarrow Y$ 进去,就可以得到一个 $Hom(A,X) \rightarrow Hom(A,Y)$ 的函数,实际上是 $f \circ -$ ( $f$ 在左边)。
  3. 保留组合法则。

(没理解态射是怎么变换的?参考下面这张图!)

Proof1

对照函子定义,没错,这是个函子,而且名字就叫 Hom 函子 ,更确切地说,是 协变 Hom 函子 。协变是什么意思?简单说,就是函子保留了 $X \rightarrow Y$ 的顺序,形成了 $Hom(A,X) \rightarrow Hom(A,Y)$ 的顺序。

如果扣掉第一个参数,得到 $Hom(-,A)$ ,那么这里得到的会是逆变 Hom 函子。因为传入一个 $f: X \rightarrow Y$ 得到的会是 $Hom(Y,A) \rightarrow Hom(X,A)$ 。结论就是,态射 $f$ 会被组合到右边变成 $- \circ f$ 。

(态射的变换和协变的情形完全一致)

Proof2

总结一下,就是 $Hom(-,-)$ 在第一个参数上逆变,在第二个参数上协变。

将上面的结论全部放在一起,可以形成这样的一张图:

$$ \require{amscd} \begin{CD} Hom(A,B) @>{Hom(A,f)}>> Hom(A,B')\ @V{Hom(g,B)}VV @VV{Hom(g,B')}V\ Hom(A',B) @>>{Hom(A',f)}> Hom(A',B') \end{CD} $$

其中 $f: B \rightarrow B', g: A' \rightarrow A$ 。

子类型

现在已经做好了一切准备工作,只需要把子类关系往里面套了。

我们选取的范畴 $\cal C$ 如下:

  1. 对象是一切类型,如 Cat, Dog, Mammal, Animal, ...
  2. 存在 $X$ 到 $Y$ 的箭头,当且仅当 $X$ 是 $Y$ 的子类型。如存在态射 CatAnimal
  3. 组合法则使用一般的函数组合。

现在赋予态射含义:从 $X$ 到 $Y$ 的态射是类型为 $X \rightarrow Y$ 的函数,即参数类型是 $X$ 、返回值类型是 $Y$ , $Hom(X,Y)$ 就是所有 $X \rightarrow Y$ 函数。(注:上面的定义中的箭头是自然的 upcast。)亦可以认为,它就是子类型关系。

态射本身是可以组合的,并且可以看作有传递性。最终得到的传递闭包有什么用呢?由于子类型的 upcast 是非常自然的,所以这里所有态射(upcast 函数)均可以由编译器自动实现。

回到开头的栗子:

// 原本的函数签名是 Animal -> Bird
Bird Magic(Animal animal);

// 我们在实际使用时的用法是 Mouse -> Animal

由于 BirdMouse 都是 Animal 的子类型,所以存在函数 fg 分别把 BirdMouse upcast 到 Animal 类型上。

回到上一节末尾的图片,取

  • $A$ = Animal
  • $B$ = Bird
  • $A'$ = Mouse
  • $B'$ = Animal

会得到如下的图:

$$ \require{amscd} \begin{CD} Hom(\text{Animal},\text{Bird}) @>{Hom(\text{Animal},f)}>> Hom(\text{Animal},\text{Animal})\ @V{Hom(g,\text{Bird})}VV @VV{Hom(g,\text{Animal})}V\ Hom(\text{Mouse},\text{Bird}) @>>{Hom(\text{Mouse},f)}> Hom(\text{Mouse},\text{Animal}) \end{CD} $$

也就是,编译器可以自动得到 (Animal -> Bird) -> (Mouse -> Animal) 的 upcast,或者说,编译器可以自动推断出 Animal -> BirdMouse -> Animal 的子类型。

至此,我们证明了如果编译器中存在子类型,并且可以提供自然的 upcast,那么子类型关系在参数上逆变、在返回值上协变是必然的结果。

等等,发生了什么?

其实我也不知道发生了什么!一切的关键其实在 Hom 函子的特性,我们只是把子类型套在了 Hom 函子上而已。总之,单凭一些“东西”间的“箭头”,我们就导出了这个结论。是不是很 Exciting 呢?