[胡说翻译]写给程序员的范畴论·类型与函数

原文链接：Category Theory for Programmers: Types and Functions

前篇：[胡说翻译]写给程序员的范畴论·分则能成（Category: The Essence of Composition）

类型和函数的分类在编程中起着重要作用，所以让我们来讨论一下什么是类型以及为什么我们需要它们。

谁需要类型？

讨论静态类型 v.s. 动态类型，或者强类型 v.s. 弱类型随时可能会在办公室引发一场战争。为了世界和平，让我们用一个思想实验来阐述这个问题。想象一下，我们有百万只猴子（a.k.a. 程序猿）坐在电脑前开心地随机敲打键盘，编写程序，编译并运行。

如果它们在敲机器语言，那么任意的敲击组合都可以被接受并运行。不过对于高级语言而言，我们希望编译器可以给我们检查词法和语法错误。一旦引入了编译器，很多猴子将无法得到香蕉作为奖励，愤愤离去——不过剩下的程序就更有可能是有用的了。类型检查器提供了另一道屏障，减少了无意义程序的出现。动态类型语言里，类型错误会在运行时被检测出来，而一个强类型的静态语言可以在编译时就发现类型错误，阻止这些错误程序的运行。

问题来了：我们是想要猴子们开心，还是想要更多正确的程序？

通常来说，这个思想实验的目标是敲出一部莎士比亚的巨著（旅游业绩+2）。如果我们有拼写和语法检查，成功的几率就会大大增加。而类型检查器（或者其它同类产品）可以进一步地确保：如果罗密欧还是个人，他就不能用他的叶子进行光合作用。

类型与可组合性

范畴论就是关于如何组合箭头的学科。不过不是什么箭头都可以随便组合的。一个箭头的目标必须和下一个箭头的起点相同。在编程中，这就相当于我们将一个函数的返回值用作另一个函数的参数。如果第二个函数没有办法正确接收第一个函数产生的数据，程序就会出错。组合的两端必须契合。类型系统越强，这个“契合”的描述就越准确，也更容易被自动验证。

我听过对强静态类型检查最强烈的反对不过于会误伤一些语义上正确的程序。实际上，这样的事情很少发生，更何况各种语言都为此开好了“后门”，允许你在必要的时候绕过类型系统。哪怕强如Haskell也提供了unsafeCoerce。不过使用这类操作时要小心为上。弗朗茨·卡夫卡笔下的角色，格里高尔·萨姆莎（译注：出自小说《变形记》），把自己变成了一个巨型Bug（译住：臭虫，这里是个双关笑话），想必大家都知道结局有多么悲惨。

另一个争议点在于：处理这么多的类型对程序员而言太麻烦了。在我自己用 C++ 编写了一些迭代器声明之后，我对此深感同情。不过有一种技术叫做类型推导（Type Inference），可以让编译器帮助我们根据上下文搞定绝大多数的类型信息。在C++里，你可以使用auto来定义变量，将类型推导的差事扔给编译器完成。

在Haskell中，除了极少的情况外，类型标记（Type Annotations）完全是可选的。程序员若是无论如何想用，也是因为类型可以提供大量的语义信息，并且可以让编译错误更容易理解。使用Haskell来编写项目的通常习惯是先从设计类型开始。随后，类型标记指引着程序实现的道路，并且可以用作编译器强制检查的代码注释。

强静态类型通常被用作“我不想测试代码”的接口。你可能听过某些Haskell程序员跨下海口：“能编译的代码就是好代码！”。当然，从来没有人保证过类型正确的程序一定产生正确的输出结果。这种漫不经心的态度的结果是，在多项研究中，Haskell 在代码质量方面并没有像人们预期的那样遥遥领先。似乎在商业软件中，是否要修复一个Bug的紧迫性与经济成本和用户的容忍度息息相关，反倒和编程语言或者方法论没什么联系。多少项目落后于预期进度或者交付时缺斤少两也许是更好的判别标准。

至于那些说单元测试可以取代强类型的论调，让我们考虑一个强类型语言里常见的代码重构：修改某个函数的参数类型。在强类型语言里，你只需要修改声明并修复所有的编译错误即可。而在一个弱类型语言里，“函数现在需要一个完全不同的数据”这件事并没有传达给相应的调用位置。尽管单元测试确实可以捕获一些错误，但是测试很多时候是一个概率问题，而不是一个确定的过程，自然也不能成为证明的等价物。

什么是类型

对类型最简单直接的理解即为“值的集合”。类型Bool（请记住，具体的类型在Haskell中要首字母大写）是一个两个元素——true和false——的集合。类型Char则是所有Unicode字符的集合，其中包含了如'a'或者'牛'这样的字符。

集合可以是有限的，也可以是无限的。String类型，相当于一个Char列表，就是无限集合的例子。

当我们需要声明x的类型是Integer（整数）时：

x :: Integer

我们说这是整数集合中的一个元素。Haskell中的Integer是一个无限集合，它可以被用于任意精度的数值计算。我们同样也有一个有限版本的整数类型Int，它对应着数值的机器表示，就像C++的int一样。

有一些微妙之处使得类型和集合难以分辨。不过我保证，我不是什么数学的忠实拥趸。好消息是，我们有一个集合的范畴，就叫做Set。在Set中，对象就是集合，而态射（箭头）就是函数。

Set是一个非常特殊的范畴，因为我们可以窥探其内部并获取很多直观感受。例如我们知道一个空的集合没有元素；我们知道有很多特殊的单元素集合（one-element set）；我们知道函数可以将一个集合内的元素映射到另一个集合：函数可以将两个元素映射到同一个结果上，但是一个元素不能有两个结果；我们知道恒等函数（identity function）总是将元素映射为自身，诸如此类。我们接下来的计划是逐步忘掉这些知识，然后使用范畴论的术语——对象和箭头——来表示它们。

在一个理想的世界中，我们可以说Haskell的类型就是集合，而函数就是集合之间的数学函数。只有一个小问题：数学函数不会执行任何代码——它们生来就知道答案。Haskell的函数则需要自己计算答案。如果答案可以在有限的步骤内被计算出来，倒也不是什么大事，无论多少步都可以。但是有不少计算需要使用递归（recursion），这可能永远停不下来。我们不能仅仅禁止Haskell中的非终止函数，因为区分终止函数和非终止函数是不可判定的——这便是大名鼎鼎的停机问题。这就是为什么计算机科学家们提出了一个绝妙的点子——或者说一个重要的后门，取决于你的视角——在每个类型集合中再塞下一个bottom值： _|_，或者写作$\bot$。这个值对应着永不停歇的计算。因此，对于这个函数：

f :: Bool -> Bool

它可以返回True，False，或者_|_用以表明函数计算永不停止。

一旦你接受了bottom，你就会发现将所有的运行时错误都转变为bottom方便至极，你甚至可以显示地标明函数返回一个bottom。后者可以通过undefined表达式来完成：

f :: Bool -> Bool
f x = undefined

这个定义可以通过类型检查，因为undefined的类型是bottom，它可以是任何类型的值，包括Bool，你甚至可以这样写：

f :: Bool -> Bool
f = undefined

（不需要写x）因为bottom同样也是Bool -> Bool类型中的一员。

可能返回bottom的函数被称之为偏函数（partial function）。相对地，我们还有全函数（total function）。对于每一个可能的参数，它都能返回合法的结果。

正是因为bottom，Haskell的类型和函数并不属于Set范畴，而是Hask范畴。从理论的角度来看，这是永无休止的复杂性的根源，因此我们就此打住。从实用性的角度来看，我们当然可以忽略非终止函数和bottom，然后将Hask范畴视为真正的Set范畴（可以参考这篇文章）。

为什么需要一个数学模型？

作为一个程序员，你当然对你所使用的语言的语法了如指掌。在语言标准的开头中，这些概念通常以形式化的符号来表示。不过语言的语义要更加难以描述：它通常会占用更多的页数，总是不够形式化，而且几乎从未完备。因此争论也从未停止过，并且有各种小作坊产出的书籍在致力于解释清楚这些细枝末节的语言标准。

我们当然有用于描述语言语义的形式化工具。但是由于它们过于复杂，你只能在简化过的学术研究语言中看到它们的身影，而非在现实使用的编程重型武器中。其中一个形式化工具，操作语义（operational semantics），可以用于描述程序执行的机制。它定义了一个形式化的理想解释器。工业语言——例如C++——的语义通常就是不太形式化的操作语义——用抽象机器（abstract machine）的概念——来描述的。

问题在于：我们很难用操作语义证明程序的相关内容。为了展示程序的某个属性，你不得不在这个理想解释器上面先运行它。

程序员不用形式化地证明自己程序的正确性，这无可厚非。我们总是想当然地认为自己写的程序是对的。没有人会坐在电脑前说“让我写两行代码看看它们能做些什么”。我们总是认为我们所写的程序会按照我们的期望执行并得到预期中的结果，否则每一次执行都是心脏骤停的体验。这意味着我们可以对所写的程序进行推理，并通过大脑中的“解释器”运行它们。只是这样做很难记录每一个变量罢了。电脑比人类更适合执行程序：如果不是如此，我们为何还需要电脑？

我们还有另一个选择：基于数学的指称语义（denotational semantics）。基于指称语义，每个编程结构都有其数学解释。如果你希望证明什么性质，你只需要完成一个数学定理就好了。你可能觉得证明定理很难，但是人类已经有了上千年的数学使用史，在这条历史长河里你总能捞上来些积累的知识和经验。此外，与专业的数学家们的证明相比，我们所遇到的问题总是要简单得多。

考虑这个Haskell实现的阶乘函数，Haskell是一个很适合指称语义的语言：

fact n = product [1..n]

表达式[1..n]表示一个包含了从1到n所有整数的列表。product函数将列表内的所有元素相乘。这段代码就像数学课本上一样简洁。与之相比，以下是C语言的实现：

int fact(int n) {
  int i;
  int result = 1;
  for (i = 2; i <= n; ++i)
    result *= i;
  return result;
}

什么罐头我说？

好吧，我承认我确实偷懒了：阶乘显然有它的数学定义。精明的读者这时候就要问了：从键盘上读取输入或者发送一个数据包的数学定义是什么？在很长一段时间里，这都是一个尴尬的问题，导致了相当复杂的解释。这似乎让指称语义中看不中用，在很多实用程序上格格不入，而这些任务又可以轻松被操作语义搞定。欧金尼奥·莫吉（Eugenio Moggi）将计算副作用映射到单子（Monad）上。这个发现不仅给了指称语义新生，使得纯函数再次有用武之地，还给传统编程语言指明了方向。我们在介绍了更多范畴论后再来谈论单子的概念。

数学概念的最重要的目的之一当然是形式化地证明程序的正确性。当你在写代码卖钱的时候这听起来没有那么重要，但很多领域的软件失败的代价极其高昂，甚至要将人命作为赌注的筹码。但即便你在编写一个在线健康系统，你也可能会偏爱Haskell标准库中那些带有正确性证明的函数和算法。

纯真的函数

C++（以及其它指令式语言）里的函数和数学上的函数不是一个东西。数学上的函数只是从值到另一个值的映射。

数学函数可以很容易地在编程语言里实现：给定一个输入，我们在函数中计算输出即可。例如一个平方函数只不过是把输入的数字和自己相乘。每次调用皆是如此，而且只要输入相同，输出也一定相同。平方函数并不会随着月相而发生改变。

此外，计算一个数字的平方也不会产生任何副作用（side effect），例如给你家狗狗额外加餐。这种函数是没法简单地用数学函数来表示的，

在编程语言中，给定相同输入总是产出相同输出且没有任何副作用的函数被称为纯函数（pure function）。在一个纯函数式语言，例如Haskell中，所有的函数都是纯函数。因此，这些语言更容易使用指称语义和范畴论来描述。对于其它语言来说，你当然可以将自己限制在“你不准写副作用”的语言子集中，或者将所有的副作用分割到另一个部分中去。之后我们将看到如何使用单子实现在纯函数中表示各种各样的副作用。所以将自己限制在数学函数之上对于我们而言并没有任何损失。

类型的例子

一旦你认定了类型就是集合，你可以想到一些相当奇特的类型。例如，空集对应的类型是什么？并不是C++的void，而是Haskell里的Void。这是一种不包含任何值的类型。你可以定义一个接收Void类型参数的函数，但你永远无法调用它。因为调用需要一个类型为Void的值，而这个值压根就不存在。至于这个函数可以返回什么，没有任何限制：它可以返回任何类型（尽管实际上它不会，因为它没法被调用）。换句话说，它是一个返回类型是多态的函数。在Haskell中，这个函数有个名字：

absurd :: Void -> a

（记住a是一个类型变量，可以表示任何类型）这个名字并非巧合。在逻辑上，我们对类型和函数之间的联系有更深入的解释，我们称之为柯里-霍华德同构（Curry-Howard isomorphism）。Void类型表示错误的命题（矛盾），absurd（悖缪）函数的类型对应着**爆炸原理（principle of explosion, “from falsehood, anything follows”）**的陈述：从一个错误的前提出发，你可以得到任何想要的结论。

下一题，只有一个元素的类型是什么？你可能并不能马上想到，不过它就是C++的void。考虑一个参数和返回值都是这个类型的函数。如果参数类型是void，我们总是可以立即调用它。如果它是一个纯函数，那么它只能返回相同的结果。看看下面这个例子：

int f44() { return 44; }

你可能认为这个函数什么都没有接收，但是我们刚刚已经看到了，什么值都不接收的函数是无法调用的。那么这个函数到底接收了什么？从概念上讲，它需要一个虚拟值，该值只有一个实例，所以我们不需要显示写出来。不过在Haskell中，我们有对应的符号来表示这个值：()。所以，非常有趣，在Haskell里调用这样的函数看起来和C++非常相似。此外，由于Haskell程序员都非常简洁，()同样也是这个类型的名字。上面的函数用Haskell表示如下：

f44 :: () -> Integer
f44 () = 44

第一行申明了f44接收类型为()的参数，读作unit，并返回一个整数。第二行通过0匹配unit的唯一构造的方式定义了函数的实现，并返回一个44。你可以传入一个unit的值来调用f44：

f44 ()

请注意，接收unit的每个函数都相当于从目标类型中选取单个元素（这里选择了44）。事实上，你可以认为f44就是数字44的另一个表达方式。这个例子展示了我们如何使用函数（箭头）来避免显式地使用集合中的元素。从unit类型到任意类型A的函数可以与集合A中的元素一一对应。

那么以void为返回类型——或者说在Haskell里，以unit为返回类型——的函数呢？在C++里这样的函数被用于副作用，但是这在数学世界中行不通。一个返回unit的纯函数只能丢弃它的参数。

数学上，一个从集合A映射到单个元素集合的函数只能将所有可能的输入都映射到那一个元素。对于每个类型A，我们都可以定义一个这样的函数，以下是Integer的版本：

fInt :: Integer -> ()
fInt x = ()

无论你传递什么数字进去，它总是返回unit。出于简洁的目的，Haskell允许你使用通配符（Wildcard）_（下划线）来丢弃一个参数，这样你就不用费尽心思给它取一个名字了。以上的代码可以被写为：

fInt :: Integer -> ()
fInt _ = ()

注意，这个函数的实现不依赖于传进来的值，甚至不依赖参数的类型。

对于任意给定类型，函数都可以用同一套公式套出来的函数，就被称为多态函数。你可以一口气实现一堆函数，只需要将具体类型替换为类型参数即可。一个接受任意参数但返回unit类型的函数该叫什么呢？当然叫unit：

unit :: a -> ()
unit _ = ()

在C++中，你可以这样实现函数：

template<class T>
void unit(T) {}

谈下一话题：有两个元素的类型是什么呢？在C++里，这个类型叫做bool，可以预见它在Haskell里被写作Bool。唯一的区别是C++的bool是一个内置类型（Built-in Type），而在Haskell我们要这样定义：

data Bool = True | False

（上面的代码读作“Bool要么是True，要么是False”）理论上来说，我们也可以在C++里重新定义布尔类型：

enum bool {
  true,
  false
};

很遗憾，C++的enum本质上其实是个整数。你可以使用C++ 11的enum class，不过你需要手动指明每一个值所属的类型，即bool::true和bool::false，再别说你还要在使用的时候把头文件给加上。

一个返回Bool的纯函数只能二选一：要么是True要么是False。这样的函数我们称之为谓词（Predicate）函数。例如Haskell标准库中的Data.Char就有像isAlpha或者isDigit这样的函数。在C++中也有类似的函数：isalpha和isdigit，不过这俩函数其实返回的是int而不是bool。实际的谓词函数也定义在std::ctype中，形式为ctype::is(alpha, c)和ctype::is(digit, c)。