<译> 类型与函数

原文见 http://bartoszmilewski.com/20...

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

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

谁须要类型？

关于静态 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.

-> 下一篇：『范畴，可大可小』