<译> 类型与函数

原文见 http://bartoszmilewski.com/2014/11/24/types-and-functions/

上一篇 ->复合：范畴的本质

类型与函数构成的范畴在编程中担任着重要的角色。我们讨论一下类型是什么，为什么需要它。

谁需要类型？

关于静态 vs 动态，强类型 vs 弱类型，似乎存在着一些争论。下面我用一个思想实验让这些选择变得更直观一些。想象一下，无数只猴子在快乐的随机敲打着键盘，产生程序，编译，然后运行。

对于机器语言而言，猴子们产生的任何字节的组合都会被计算机接受并运行。我们应该庆幸，高级的语言，因为有负责检查词法与语法错误的编译器的存在，导致大部分猴子因为努力敲打键盘却未得到香蕉而拂手而去，而剩下的那些猴子胡乱敲打所生成的程序如果能通过编译，它们更有可能变成有用的程序。类型检查也提供了一个门槛，可以拦截无意义的程序。此外，在强类型的静态语言中，可以在编译期间发现类型错误，从而在大部分不正确的程序运行之前就干掉了它们，而动态类型语言只能在运行时进行类型检查……

那么，问题就来了，我们想让猴子们高兴么，或者我们想产生正确的程序么？

这个关于猴子的思想实验，通常的目标是让打字的猴子们创作一部莎士比亚全集的。在这个过程中，如果有拼写检查与语法检查，就可以提高成功的可能性。类型检查的比喻具有更重要的意义，因为它可以确定，一旦罗密欧被识别为人类，那么他就无法生根发芽长出树叶或者在他强大的重力场中捕获光子。

类型关乎复合

范畴论与箭头的复合有关。但是并非任意两个箭头都可以复合。一个箭头的目标对象必须与下一个箭头的源对象相同，这样的两个箭头方能复合。在编程中，我们将一个函数的返回结果传递给另一个函数。如果目标函数不能正确的解析源函数传递来的数据，程序就不会工作。首尾必须相连，方能实现复合。编程语言的类型系统越强，箭头的配合就越容易描述与检验。

我见过唯一的一场反对强类型检查的严肃争论，认为它可能会扼杀一些程序，而这些程序在语义上却是正确的。现实中，这种情况出现的几率非常之小，并且每一种语言都提供了某种后门，可以让代码在真正需要的时候通过类型检查。即使是 Haskell 这样的语言，也有这种后门。但是这种设施应该谨慎使用。卡夫卡的小说《变形记》中的葛里高尔，当他变异为巨大的甲虫时，打破了类型系统，其结局大家也都看到了。

我见过的另一场争论，是认为类型的处理给程序员带来巨大的负担。在不得不为 C++ 的迭代器写一些类型声明的时候，我深有同感。但是有一种技术叫类型推导，它可以让编译器在需要的时候能够根据上下文推导出大部分类型。在 C++ 中，现在可以用 auto 变量，其类型具体是什么就交付给编译器来确定。

在 Haskell 中，大部分场合，类型声明并非必须。不过 Haskell 程序猿还是趋向于使用类型声明，因为他们可以让代码具有语义，也能使得编译错误更容易理解。Haskell 的实际编程中，往往是在项目的一开始就进行类型设计，然后用类型的声明驱动程序的实现，最终类型声明会变成代码注释，但是这种注释对于编译器是有意义的。

强静态类型通常用于代替代码测试。你可能有时听到 Haskell 程序猿说，『能通过编译，它就是正确的』。当然，没人能担保类型是正确的程序就能够产生正确的输出。这种骑士般的态度所引发的结果就是，有些人研究发现强类型的 Haskell 在代码质量方面的进展并没有像大家预期的那样好。不过，在商业软件开发中，似乎修复 bug 的压力只停留在一个特定的质量级别，这个级别介乎软件开发成本与用户的容忍限度之间，它与编程语言或编程范式的关系不太大。更好的评价指标应该是检查有多少项目延期交付了，或者有多少项目在大幅消减了函数式编程范式之后它及时交付了。

至于单元测试能够替代强类型检查方面也有一些争论，考虑一下强类型语言中的常见的重构行为：改变一个函数的参数类型。在强类型语言中，修改函数的声明就可以修复所有的构建错误。在弱类型语言中，函数的变化却无法传播到它被调用的地方。单元测试虽然能够捕捉到一些错误，但是测试总是概率意义上的，而不是一个确定的过程。测试是一种贫弱的证明。

类型是什么

对于类型，最简单的直觉就是它是值的集合。 Bool 类型（记住，Haskell 中具体类型是大写字母开头）是一个含有 2 个元素 True 与 False 的集合。 Char 类型是所有 Unicode 字符的集合。

集合可能是有限或无限的。 String 类型，它与 Char 列表同义，它就是个无限集的例子。

当我们将 x 声明为 Integer 时：

x :: Integer

我们想说的是， x 是一个整型数集中的一个元素。在Haskell 中， Integer 是有限集，它能够用于任意精度的算术。还有个有限集，叫 Int ，它与机器类型有关，就像 C++ 的 int 。

有一些微妙的东西，可以使得类型与集合的定义更为精巧。比如多态函数存在一些问题，因为事实上你不可能拥有一个所有集合的集合。但是我承诺过，我不会过于数学化。集合的范畴是个伟大的概念，它的名字就叫做 Set ，我们以后只在它上面工作。在 Set 中，对象是集合，态射（箭头）是函数。

Set是个非常特殊的范畴，因为我们实际上只能从它的内部拮取一些对象，并通过操作这些对象来认识它。例如，我们知道空集不包含任何元素。我们知道存在只含有一个元素的集合。我们知道函数可以将一个集合中的元素映射到另一个集合。它们也能将两个元素映射为一个，但是却不能将一个元素映射为 2 个。我们还知道恒等函数可以将一个元素映射为本身，等等。现在我们不妨将逐步忘记这一切，去使用纯粹的范畴论语言——对象与箭头——去表达这些概念。

在理想世界中，我们可以说 Haskell 的数据类型是集合，Haskell 的函数是集合之间的数学函数。只不过有个小问题：数学函数不可被执行——它只知道答案。Haskell 函数必须要计算出答案。如果答案可以在有限步骤中被计算出来，这不是什么问题，然而步骤的数量可能会很大。有些计算是递归的，它可能永远不会终止。在 Haskell 中我们不能阻止停不下来的函数，因为这就是著名的停机问题。这就是为什么计算机科学家搞出来一个聪明的点子，也可以说是一个巨大的 hack，这取决于你的视角，它将每一种类型增加了一个特殊值，叫做 底 （Bottom），用符号表示为 _|_ ，也可以用 Unicode 字符 ⊥ 。这个『值』与无休止计算有关。因此，若一个函数声明为：

f :: Bool -> Bool

它可以返回 True ， False 或 _|_ ；后者表示它不会终止。

有趣的是，一旦你接受了将 底 作为类型系统的一部分，就可以将每一种运行时错误作为 底 来对待，甚至可以容许函数显式的返回 底 。后者通常用于未定义的表达式，例如：

f :: Bool -> Bool f x = undefined

这种类型的定义之所以能通过类型检查，是因为 undefined 的求值结果是底，而底可以是任何类型的值，所以它也是 Bool 类型的值。甚至，你可以这样不要那个 x ，即：

f :: Bool -> Bool f = undefined

因为底也是类型 Bool->Bool 这种类型的值。

可以返回底的函数被称为偏函数，与全函数相对，后者总是对于每种可能的参数值返回有效的结果。

由于底的存在，你将会看到 Haskell 类型与函数的范畴会被称为 Hask，而不是 Set。从理论上来看，这是导致出现无休止的复杂性的源头，因此在这一点我要动用我的庖丁之刀将复杂砍掉。从实用的角度来看，不理睬无休止的函数与底是没有问题的，将 Hask 视为一个友善的 Set 即可（详见本文末尾的参考文献）。

为何我们需要一个数学模型？

身为程序猿，你所熟悉的是编程语言的语法。编程语言的各个方面在这门语言诞生之初是通过形式化标记描述的。但是语言的语义却很难描述，有时用一本挺厚的书来描述，可能也无法完整的说清楚。因此，语言专家们之间的讨论永无休止，那些讲解语言的工业化标准的书籍已经汗牛充栋了。

有些形式化工具可描述语义，但是由于它们太复杂了，以至于只是在一些简化的学院级语言中使用了它们。此类工具中，有一个工具叫做 操作语义（operational semantic） ，它描述的是程序的执行机制。它定义了形式化理想化的解释器。工业级语言的语义，类似 C++，用的是非正式的操作语义，称之为『抽象机器』。

使用操作语义存在的问题是要难以证明程序的正确性。要展现一个程序的性质，你只能在一个理想化的解释器中去『运行』它。

没关系，反正程序猿不需要去形式化的证明程序的正确性。我们总是『思考』我们在写正确的程序。没有人在键盘前说，『呃，我随手写几行代码，看看会发生什么』。我们思考的是，我们所写的代码会拥有正确的行为，产生我们想要的结果。一旦程序做不到这些，我们通常会相当惊讶。这意味着，我们在写代码的时候没有对程序进行推导，只是在写完后才在自己的大脑中的解释器中运行它的时候才进行正确性推导。这样做的问题是很难跟踪所有的变量。计算机善于运行程序，人类却不能！如果我们能，就没必要发明计算机了。

但是，还有一种选择，它叫 指称语义（Denotational semantic） ，是基于数学的。在指称语义中，每个编程结构都会被给出数学解释。使用它，如果你想证明程序的正确性，只需要证明一个数学定理。你可能觉得数学定理的证明是很难的，但是我们人类建立数学方法已经上千年了，因此有大量的知识资源可以利用。还有，与数学家所证明的那些定理相比，我们在编程中遇到的问题通常是相当简单的，生僻的问题很少。

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 发现了计算结果能够被映射为单子这一现象，不仅扭转了乾坤，使得指称语义大放异彩，并使得纯函数式程序变得更为有用，也使得传统的编程范式绽放出新的光芒。单子，我们以后在发展更多的范畴论工具时再予以探讨。

对于编程而言，拥有一个数学模型的重要的优点就是能够对软件的正确性给予形式化证明。这对于写消费级软件来说可能不是太重要，但是有些领域，失败的代价相当高，甚至会出人命。不过，事实上当你为健康系统写网络应用程序时，你可能会欣赏具有正确性证明的 Haskell 标准库中的函数与算法。

纯函数与脏函数

在 C++ 或其他命令式语言中，我们称之为函数的东西，与数学上被称为函数的东西是不同的。数学上的函数是值到值的映射。

在编程语言中，我们能够实现数学上的函数：一个函数，给它一个输入值，它就计算出一个输出的值。一个平方函数就是输入值自身的乘积。每次被调用时，对于相同的输入，它总是能保证产生同样的输出。一个数的平方不会随着月相的变化而变化。

再者，计算一个数的平方也不会对你的狗粮配方有副作用。如果有一个『函数』就是对你的狗粮配方有副作用，那么它的模型就与数学里的函数存在很大差异。

在命令式语言中，给予相同输入总是能得到相同输出的函数，被称为 纯函数 。在一种纯函数式语言中，例如 Haskell，所有的函数都是纯的。正是因为这一点，Haskell 更易于赋予语言以指称语义，并使用范畴论进行建模。对于其他语言，也可以构造出一个纯的子集，或者对副作用谨慎对待。以后我们将会看到单子是如何只借助纯函数来对各种副作用进行建模的。总之，我们用数学函数来约束自己，但是却没有任何损失。

类型的示例

一旦意识到类型是集合，你就可以思考一些相当生僻的类型。例如，空集这种类型是什么？在 Haskell 中，空集是 Void ，虽然 C++ 中也有个 void ，但它俩不是一回事。Haskell 中的 Void 是一个不存储任何值的类型。你可以定义一个接受 Void 的函数，但是你永远无法调用它。因为，要调用这个函数，必须向它提供一个 Void 类型的值，但这种类型的值并不存在。至于这个函数的返回值，不需要作任何限制。它可以返回任何类型，反正它根本没有机会运行。换句话说，它是一个具有多态返回类型的函数。Haskell 程序员将其命名为：

absurd :: Void -> a

记住， a 是一个类型变量，它可接受任何类型。函数的名字不太相符。这种类型与函数，在逻辑学上有更深入的解释，它们被称为 Curry-Howard 自同态。 Void 类型表示谎言， absurd 函数的类型相当于『由谎言可以推出任何结论』，也就是逻辑学中所谓的『爆炸原理』。

下一个类型相当于单例集合。它是只有一个值的类型。你可能意识不到，它实际上就是 C++ 中的 void 。考虑那些输入是 void 以及返回是 void 的函数。一个输入是 void 的函数总是能够被调用。如果它是纯函数，它就能否返回相同的结果。例如：

int f44() { return 44; }

你可能认为这种函数没有输入。但是刚才我们已经见识了，一个函数如果不接受任何值，它永远也无法被调用。那么，这个 f44 接受了什么？从概念上说，它接受了一个空值，而且不会再有第 2 个空值，因此我们就没必要再显式的提及它。然而 haskell 为控制提供了一个符号，即空的序对 () 。因此就有了搞笑的巧合（真的是巧合吗？），输入为 void 的函数，C++ 与 Haskell 的版本看上去是相同的。不过，在 Haskell 中， () 也可以用在类型、构造子上。 f44 的 Haskell 版本如下;

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

第一行代码描述了 f44 接受 () 类型（这个类型读作『unit』），将其映射为 Integer 类型。第二行代码是通过 unit 的构造子 () 的模式匹配来定义 f44 。只要你提供 unit 的值 () 就可以调用这个函数：

f44 ()

注意，每个 unit 函数都等同于从目标类型中选取一个值的函数（在此，就是选择 Integer 类型的值 44）。实际上，你可以将 f44 作为数字 44 的另一种表示方法，因此这也是如何通过与函数（箭头）的交互来代替集合中一个显式的元素的示例，也就是说数据与计算过程的本质上是没有区别的。从 unit 到类型 A 的函数相当于集合 A 中的元素。

让函数返回 void 类型会怎样，或者说，在 Haskell 中，让函数返回 unit 会怎样？在 C++ 中，这样的函数通常担当具有副作用的函数，但是我们知道这种函数并非数学意义上的函数。一个返回 unit 的纯函数，它什么也不做，或者说，它唯一做的就是丢弃它所接受的输入。

在数学上，一个从集合 A 到单例集合的函数会将 A 中的每个元素映射为单例集合中的元素。对于每个 A 都存在这样的函数。例如对于 Integer ，有：

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

你向这个函数提供任何整数，它都会给你返回一个 unit。本着简明扼要的精神，Haskell 允许你使用通配符模式，可以用下划线来替代要忽略的输入。这样你就不需要再为它重新弄个名字。上述函数可改写为：

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

注意，这个函数的实现不仅不依赖传给它的参数，它也不依赖参数的类型。

对于任意类型都具有相同形式的函数，称为参数型多态。用类型变量来代替一个具体的类型，就可以实现一个函数族。我们要怎么称呼一个从任意类型到 unit 的函数？当然，要称它为 unit ：

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

在 C++ 中，你可以这样来写：

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

我们的类型学里的下一个类型是二元集合。在 C++ 中，这个集合被称为 bool ，在 Haskell 中则称为 Bool 。二者的区别是，C++ 的 bool 是内建类型，而 Haskell 的则可以自行定义：

data Bool = True | False

这个定义得这么读： Bool 要么是 True ，要么是 False 。理论上，C++ 也可以用枚举来定义一个 Bool 类型：

enum bool {     true,     false };

但是 C++ 的 enum 的类型本质上是整型。C++ 11 的 enum class 倒是自成一类了，不过你肯定不想这样来用布尔值： bool::true 与 bool::false ，而且还要在代码中包含定义了这一类型的头文件。

输出 Bool 的函数被称为 谓词 。例如，Haskell 库 Data.Char 充满了类似 isAlpha 或 isDigit 这样的谓词。在 C++ 中，也有各类似的库，它也定义了 isalpha 与 isdigit 以及其他相似的方法，不过它们的返回值是 int 类型，而不是布尔类型；真正的谓词被定义为 ctype::is(alpha, c) ， ctype::is(digit, c) 之类。

挑战

1. 用你最喜欢的语言，定义一个高阶函数（或函数对象） memoize 。这个函数接受一个纯函数 f ，返回一个行为与 f 近乎相同的函数 g ，但是 g 只是第一次被调用时与 f 的功能相同，然后它在内部将结果存储了起来，后续再用同样的参数调用它，它只返回自己存储的那个结果。你可以通过观察 f 与 g 的运行效率来区分它们。例如，让 f 是一个需要耗费挺长时间才能完成计算的函数，这样，当第一次调用 g 的时候，它会运行的很慢，但是用同样的参数对 g 再次调用，则可以立即得到结果。

2. 标准库中用于生成随机数的函数，能够被 memoize 么？

3. 大多数随机数生成器都能够用一个种子进行初始化。请实现一个能够接受种子的函数，这个函数可将种子转交给随机数生成器，然后返回所得结果。这个函数能被 memoize 么？

4. 下面的 C++ 函数，哪一个是纯的？试着去 memoize 它们，然后多次调用后看看会发生什么：能被 memoize 还是不能。

(1) 文中的阶乘函数。 (2) std::getchar() (3) bool f() {   std::cout << "Hello!" << std::endl;   return true;  } (4) int f(int x)  {   static int y = 0;  y += x;  return y;  } 

5. 从 Bool 到 Bool 的函数有多少中？你可以将它们都实现出来么？

6. 将 Void ， () （unit）以及 Bool 作为对象，将与这些类型相关的所有函数作为箭头，你能画出一个范畴么？用函数名来标注箭头。

参考文献

1. Nils Anders Danielsson, John Hughes, Patrik Jansson, Jeremy Gibbons, Fast and Loose Reasoning is Morally Correct . This paper provides justification for ignoring bottoms in most contexts.