范畴论：1.2 类型和函数

由类型【Type】和函数【Function】组成的范畴在编程中扮演者重要的角色。所以，让我们来谈谈什么是类型以及为什么需要它们。

2.1 who need type?

对于静态vs动态、强类型vs弱类型的优点，一直存在着异议。下面让我用一个思维实验，来说明这些选择。想象数以百万计的猴子在电脑键盘上快乐地敲击随机键，生成程序，编译和运行它们。

使用机器语言，任何由猴子生成的字节组合都可以被机器识别并运行。但是对于高级语言，我们确实需要感谢编译器能够检测出词法和语法错误。很多猴子为此而没有香蕉可以吃，但剩下的程序将更有可能是有用的。类型检查为防止无意义的程序提供了障碍。此外，在动态类型语言中，类型不匹配需要在运行时才会发现，但在强类型静态检查的语言中，在编译时就会发现类型不匹配，从而在有机会运行之前消除许多不正确的程序。

所以现在的问题是，我们是想让猴子开心呢，还是想作出正确的程序呢？

假设在我们思维实验中猴子的目标是莎士比亚全集的制作，我们循环使用拼词法检查器和语法检查器，这样会大大增加成功的几率。而类型检查器则会锦上添花，确保罗密欧一旦被声明为人类，他就不会长出叶子，或者在他强大的引力场中捕获光子。

2.2 Types Are About Composability

范畴论是关于组合箭头【Arrow】的，但并不代表任意两个箭头【Arrow】都可以组合。一个箭头【Arrow】的目标【Target】对象，必须与下一个箭头【Arrow】的源【Source】对象保持一致（即待组合的箭头首尾需要呼应）。在编程中则表现为我们将一个函数结果传递给另一个函数，如果目标函数无法解释源函数产出的数据，程序将无法运行。两端必须适配才可以正常工作。语言的类型系统越强，这种匹配就越能被描述和机械地验证。

我听到的反对强静态类型检查的唯一严肃的论点是，它可能会消除一些语义正确的程序。实际上，这种情况极少发生，而且在任何情况下，每种语言都提供了某种后门，在真正必要的时候可以绕过类型系统。甚至在Haskell中也有unsafeCoerce。但是这些设备应该谨慎使用。

我常听到的另一个论点是，处理类型给程序员带来了太多负担。在我使用C++编写迭代器时，不得不写一些类型声明时，我对这种情绪表示理解与同情，但除此之外，有一种叫做类型推演【type inference 】的技术，它允许编译器从使用它们的上下文中推断出大多数类型。在C++中，您现在可以声明一个变量auto，并让编译器推演出它的类型（Java中也具备了这种技术）。

在Haskell中，除了极少数情况外，绝大多数情况下类型标注（就是不要依赖类型推演，手动声明类型）完全是可选的。但是我建议：程序员应该倾向于使用它们，因为它们可以告诉我们很多关于代码语义的信息，而且它们使得编译错误更容易理解。在Haskell中通过设计类型来开始一个项目是一种常见做法。之后，类型标注会驱动实现，并成为编译器强制注释。

但是强静态类型经常被作为不测试代码的借口。有时你可能会听到Haskell程序员说，“如果它编译过了，那它一定是正确的。”当然，从保证程序输出正确的角度而言，类型正确并不能代表输出的正确。这种漫不经心的态度导致Haskell的代码质量并没有人们预想中那么强。似乎，在商业环境中，修复bug的压力只适用于一定的质量水平，这与软件开发的经济性和最终用户的容忍度有关，而与编程语言或方法论无关。一个更好的标准是衡量有多少项目落后于进度或者交付时功能的完成度。

至于单元测试可以取代强类型的论点，请考虑强类型语言中常见的重构实践：改变特定函数的参数类型。在强类型语言中，修改该函数的声明，然后修复所有构建中断就足够了。但在弱类型语言中，一个函数现在期望不同数据的事实不能传播到调用站点。单元测试可能会捕捉到一些不匹配，但是测试几乎总是一个概率性的过程，而不是确定性的过程。测试被证明并不是一个优秀的替代品。

2.3 What Are Types?

凭直觉而言，类型(types)就是关于值(values)的集(sets)。Bool类型是True和False两个元素的集(set)。而Char则是所用Unicode字符的集(set)，比如q、w、e、r

集(sets)可以是有限的，也可以无限的，String类型是Char列表的同义词，它就是无限集的例子。

当我们将x声明为Integer的时候

//Scala Grammar
val x: BigInt

我们说它(指的就是x)是整数集(set)中的一个元素。Haskell中的Integer是一个无限集(infinite set)，它可以用来进行任意精度的算术运算，Haskell中还有一个Int类型，它对应于机器类型，是一个有限集(finite-set)，就像C++中的int一样

这里存在一些微妙之处，使得类型(types)和集(sets)的识别变得棘手。涉及环形定义(circular definitions)的多态函数存在一些问题，你不可能拥有所有集(sets)的集(set)；但正如我所承诺的，我并不是数学的顽固派。但最棒的是，这里有一个集(sets)的范畴，我们称它为???，我们将使用它。在???中，对象(objects)即是集(sets)，而态射(arrows)则是函数(functions).

PS:前面有说过，范畴是由对象和箭头组成的，???是集(set)的范畴，那么自然它的对象就是集(set)，而态射/箭头则是函数

???是一个非常特殊的范畴，因为它我们可以窥探其中的对象，并得到很多直觉上的知识。例如，我们知道空集(empty set)中没有元素。我们知道还有特殊的单元素集(one-element sets)。我们知道函数将一个集(set)上的元素映射到另一个集合(set)上的元素，它们还可以将两个元素映射到一个元素，但不能将一个元素映射到两个元素。我们还知道恒等函数将集(set)中的每个元素映射到自身，以此类推。But：我们的计划是逐渐忘记所有这些信息，而是用纯粹的范畴术语来表达所有这些概念，也就是用对象(objects)和箭头(arrows)来表达。

在理想情况下，我们可以说Haskell中的类型(types)就是集(sets)，Haskell中的函数则是集(sets)之间的数学函数。这里仍有一个小问题：数学中的函数并不执行任何代码——它只知道答案。Haskell函数必须通过计算才能得出答案。如果答案可以通过有限的计算步骤得到——不管这个步骤有多大——那这就不是问题。但有些计算涉及递归，而且可能永远不会终止。我们不能禁止Haskell中的非终止函数，因为无法区分终止函数和非终止函数——这就是著名的停止问题。这也就是为什么计算机科学家想出了绝妙的主意，或者说是一个重要的骇客，即通过一个特殊值（称为bottom），来拓展每一个类型，该特殊值表示为_|_或者Unicode的⊥，该”值“对应于非终止计算，因此如果一个如下声明的函数：

val f: Boolean => Boolean

那么它的返回值包括True、False和_|_，后者意味着它永远不会结束。
有趣的是，一旦接受bottom作为类型系统的一部分，就可以方便地将每个运行时错误视为bottom，甚至允许函数显式地返回bottom。后者通常使用undefined表达式表示，如:

//Haskell使用undefined
f :: Bool -> Bool
f x = undefined
//Scala使用???
val f: Boolean => Boolean = x => ???

该定义可以通过类型检查，因为undefined的计算结果是bottom，它是任何类型的成员，包括Bool。你甚至可以这样写:

//Haskell
f :: Bool -> Bool
f = undefined
//Scala
def f: Boolean => Boolean = ???

(注意：这里没有x =>)因为underfined也是类型 Bool -> Bool的成员

可能返回bottom的函数也被成为偏函数(partial function)，与全函数(total function)相对，后者（即全函数）为所有的可能的入参返回有效的结果。

因为Bottom，你会看到Haskell的类型和函数所组成的范畴被称之为Hask，而不是???。从理论的角度来看，这是无休止的复杂性的来源，所以在这一点上，我将使用我的屠刀并终止这条推理线。从务实的角度来看，可以忽略非终止函数和Bottom，并将Hask作为合法的???，这也是可以的。(参见末尾的参考书目)

2.4 Why Do We Need a Mathematical Model?

作为一名程序员，您非常熟悉编程语言的语法和句法，语言的这些方面通常在语言规范一开始就使用形式标志（formal notation）描述好了。但是，我们却很难描述语言的意思，或者说是语义(semantics)；它需要更多的页面，且不够形式化和完整。因此语言学家之间的讨论从未休止，以及一大批致力于解释语言标准细微之处的书籍。

有很多形式化工具，用于描述语言的语义，但是由于它们的复杂性，它们大多用于简化的学术语言，而不是实际的编程巨兽。其中一个叫做操作语义【Operational semantics 】的工具描述了程序执行的机制。它定义了一个形式化的理想化解释器。工业语言(如c++)的语义通常使用非形式化的操作推理（称为“抽象机器”）来描述。

但问题是很难用操作语义【Operational semantics 】来证明程序。要显示程序的属性，本质上必须通过理想化的解释器“运行它”。

程序员从未执行过形式化的正确性证明并不重要。我们总是“认为”我们写的程序是正确的。没有人坐在键盘前说，“哦，我只需要写几行代码，看看会发生什么“。我们认为我们编写的代码将执行特定的操作，从而产生预期的结果。而当结果并没有符合预期时，我们通常会很惊讶。这意味着我们要对自己编写的程序进行推理，我们通常通过在头脑中运行一个解释器来进行推理。要记住所有的变量真的很难。计算机擅长运行程序——而人类却不行！如果是的话，我们就不需要电脑了。

但还有另一种选择。它叫做指称语义【denotational semantics】，它是基于数学的。在指称语义中，每一个编程结构都有其数学解释。这样，如果你想证明一个程序的一个性质，你只需要证明一个数学定理。你可能认为定理证明很难，但事实是我们人类已经建立数学方法几千年了，所以有大量积累的知识可以利用。此外，与专业数学家所证明的定理相比，我们在编程中遇到的问题通常非常简单，甚至可以说是微不足道的.

PS:在计算机科学中，指称语义【denotational semantics】是通过构造表达其语义的数学对象来形式化计算机系统的语义的一种方法。编程语言的形式语义的其他方法包括公理语义和操作语义。指称语义方式最初开发来处理一个单一计算机程序定义的系统。后来领域扩展到了由多于一个程序构成的系统，比如网络和并发系统

下面来考虑Haskell中的阶乘函数的定义，这是一种非常适用于指称语义的语言：

//Haskell
fact n = product [1..n]
//Scala
val fact = (n: Int) => (1 to n).product

表达式[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;
}

还要我说什么吗？

好吧，我首先承认这是我故意的中伤。阶乘函数具有明显的数学意义。聪明的读者可能会问：从键盘上读取字符或通过网络发送数据包的数学模型是什么？在很长一段时间里，这将是一个尴尬的问题，导致一个相当复杂的解释。似乎指称语义【denotational semantics】不适合编写有用程序所必需的大量重要任务，而这些任务可以很轻松的通过操作语义【Operational semantics 】来实现。范畴论带来了突破的曙光，Eugenio Moggi发现计算作用可以被映射到单子上。这被证明是一个重要的发现，它不仅赋予了指称语义【denotational semantics】以新的生命，使纯函数程序更加可用，而且为传统编程带来了新的曙光。稍后，当我们开发更多属于某一范畴的工具时，我将讨论单子。

使用数学模型进行编程的一个重要优点是可以对软件的正确性进行形式化的证明。在编写消费类软件时，这一点似乎并不那么重要，但在某些编程领域，失败的代价可能过高，甚至危及到人类的生命。但是，即使在为健康系统编写web应用程序时，您也可能会欣赏Haskell标准库中的函数和算法带有正确性证明的想法。

2.5 Pure and Dirty Functions

我们在c++或其他命令式语言中调用的函数，与数学家调用的函数是不同的。数学函数只是值到值的映射。

我们可以用编程语言实现一个数学函数：这样一个函数，给定一个输入值就会计算出输出值。比如一个函数产生一个数字的平方，它可能会将输入值乘以它自己。每次调用它的时候，它都会这样做，并且保证每次调用它的时候，相同的输入必须产生相同的输出。一个数的平方不随月相的变化而变化。

此外，计算一个数字的平方不应该有为您的宠物狗喂食的副作用。否则这样的“函数”不能轻易地建模为数学函数。

在编程语言中，在给定相同输入的情况下总是产生相同结果且没有副作用的函数称为纯函数。在像Haskell这样的纯函数语言中，所有函数都是纯函数。正因为如此，更容易给这些语言提供指称语义【denotational semantics】，并使用范畴论对它们进行建模。对于其他语言，总是可以将自己限制在一个纯子集中，或者单独推断副作用。稍后我们将看到monads如何让我们仅使用纯函数来建模各种作用【Effect】。所以我们不会因为把自己局限于数学函数而失去任何东西。

2.6 Examples of Types

一旦您意识到类型(types)就是集(sets)，您脑海中总会浮现出一些奇特的集。比如：什么类型对应于空集(empty set)？？No，它绝不是C++中的void，但是这个类型在Haskell中称为Void，它是一个没有任何值居住的类型。尽管你可以定义一个参数是Void的函数，但是你永远也无法调用它，因为为了调用它，你必须提供一个Void类型的值，但是这是不可能的。至于这个函数可以返回什么类型的值，这个没有限制。它可以返回任何类型的值(尽管他永远无法返回该值，因为我们无法调用该函数)。换句话说，它是一个返回类型具有多态性的函数。 Haskellers为这样的函数起了一个名字：

//Haskell
absurd :: Void -> a
//Scala
def absurd[A]: Nothing => A    PS: Scala中存在Nothing类型，它是空集对应的类型

(请记住，Haskell语法中，a是一个可以代表任何类型的类型变量，这与Java相反，Java中以大写的泛型表示任何类型，比如T)该名称并非巧合。从逻辑（也被称为柯里-霍华德同构）的角度来看，这是对类型和函数的深入理解。Void类型代表的是虚无(falsity)，而absurd函数的签名类型则暗示了虚无可以推理出任何/一切，就像中国的格言"失之毫厘谬以千里"。

PS:我认为“道生一一生二二生三三生万物”更符合，道，一，二，三皆为虚妄，生万物

接下来是只有单个值的集所对应的类型。这是一种只可能有一个值的类型。您可能不会立即认出它，但它就是C++中的void。下面我们来考虑一个入参是void和返回值是void的函数，如果入参是void，那么我们可以任意的调用它，如果它是一个纯函数，那么该函数始终返回同样的结果，下面是这样的一个函数的例子：

int f44() { return 44; }

你可能会认为这是一个不需要任何入参的函数，但正如我们刚才所见，我们无法调用入参数为空(nothing)的任何函数，因为没有任何值可以表示空。那么该函数的入参到底是什么呢？从概念上讲，它接收一个虚拟值，该值只有一个实例，所以我们不必显式地提到它。然而在Haskell中，有一个专门的符号表示这个值，即一个空的括号:()。因此，在c++和Haskell中，对入参是void函数的调用看起来是一样的，这是一个有趣的巧合。此外，由于Haskell喜欢简洁，()还被用于类型，构造器以及和单元素集合(singleton set)对应的单一值。下面就是Haskell中的函数：

//Haskell
f44 :: () -> Integer
f44 () = 44
//Scala
val f44: Unit => BigInt = _ => 44

第一行中声明的f44函数，接收的类型是()，读音为"unit’，结果类型是Integer，第二行通过模式匹配unit的惟一构造函数()并生成数字44来定义f44。你可用通过提供unit的值()来调用该函数：

f44()

请注意，这种入参为unit的函数，等同于从结果类型中采撷一个单独的值用于返回(在f44函数中即是Integer类型的44)。实际上你可以讲f44看做是对数值44的一种不同表现形式。该例子阐述了我们可以使用函数(箭头)来代替结果集合中的某些显式元素。接收unit入参并返回A类型的值的函数，与A类型的集合中的元素，是一一对应的关系。
PS:Haskell中函数都是纯函数，因此这里所表述的函数，只能有一个返回值(包括元祖、列表等)，才能保证函数性(或者可以说是引用透明)

那么如果返回值类型是void的呢？或者，以Haskell语言来讲，就是返回unit的函数。在C++中这种函数通常用于副作用，但我们知道这些不是数学意义上的真正函数。返回unit的纯函数什么都不会做：它丢弃了入参。

从数学上讲，一个接收A集合，返回一个单元素集合的函数，他实际上是将A中的每一个元素映射到单元素集合的唯一值上。对于每一种类型，都有一个对应的这样函数。下面是Integer类型对应的函数：

//Haskell
fInt :: Integer -> ()
fInt x = ()
//Scala
val fInt: BigInt => Unit = x => ()

你可以传入任何的Integer类型的值，返回都是unit。本着简洁的精神，Haskell允许您使用通配符模式（下划线）来表示被丢弃的参数。这样您就不必为它创建名称。所以上面的内容可以改写为：

//Haskell
fInt :: Integer -> ()
fInt _ = ()
//Scala
val fInt: BigInt => Unit = _ => ()

请注意，上面的函数的实现不仅不依赖与函数传入的参数的值，甚至都不依赖于传入的参数的类型！！

可以对任何类型使用相同公式实现的函数，也被称为参数化多态。您可以使用类型参数而不是具体的类型，用一个公式来实现这类函数的整个系列。那么这种接收任意类型，并返回unit类型的多态函数，我们怎么称呼它呢？当然是称呼为unit啦：

//Haskell
unit :: a -> ()
unit _ = ()
//Scala
def unit [A]: A => Unit = _ => ()

在C++中，该函数可以这样来写：

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

接下来我们探讨的类型是二元元素的集合。在C++中我们称它为bool，而在Haskell中我们称它Bool。区别在于，在c++中bool是一种内置类型，而在Haskell中可以定义为:

//Haskell
data Bool = True | False
//Scala
sealed trait Bool
case object True extends Bool
case object False extends Bool

(理解这个定义的方法是：Bool要么是True，要么是False).从原则上讲，你也应该能够在c++中定义一个布尔类型作为枚举:

enum bool {true,false
};

入参是Bool的纯函数只从目标类型中选择两个值，一个对应True，另一个对应False

结果类型是Bool的纯函数也被称为谓词【predicates】。比如Haskell库中的Data.Char中充满了诸如isAlpha或者isDigit的谓词。在c++中有一个类似的库，其中定义了isalpha和isdigit，但是它们返回的是int而不是Boolean。实际的谓词在std::ctype中定义，并具有ctype::is(alpha, c)、ctype::is(digit, c)等形式。