Category-theory-for-programmers 阅读笔记

前言 & 介绍

Category Theory for Programmers, 顾名思义, 是一本关于范畴论的书, 但是偏向CS而非数学.

书的$\LaTeX$代码以GPL-3.0公布在GitHub, 有两个版本, 一个以C++作为辅助说明语言, 另一个是Scala.

作为一个蒟蒻OI党当然是选择C++版啦.

本文(如果不咕咕咕的话)会持续更新, 大概记录一些摘录或者感想或者我不知道的东西…

Preface

Category Theory – rather than dealing with particulars – deals with structure. It deals with the kind of structure that makes programs composable.

Functional programming is not only about composing functions and algebraic data structures — it makes concurrency composable — something that’s virtually impossible with other programming paradigms.

It’s not that side effects are inherently bad — it’s the fact that they are hidden from view that makes them impossible to manage at larger scales. Side effects don’t scale.

I hope future generations will be as admiring of the programming skills we’ve been displaying in building complex operating systems, web servers, and the internet infrastructure. (上文提到我们尽管中世纪的石头建筑在现在可以方便地用钢筋混凝土结构搭建, 但我们还是惊叹于中世纪的工匠们那将石质结构发挥到他们的极限的精巧工艺)

Part I - Category: The Essence of Composition

A category consists of objects and arrows that go between them.

Category的Wikipedia链接

我的误解…

Native的我, 一直把范畴当成一种特殊的有向图. 这本身没什么大毛病, 问题在于受OI题的影响, 我默认:

边与边之间唯一的区别就是起点与终点

但是, 范畴并不是这样的, 不同边在本质上就是不同的东西, 就算他们起点终点相同; 事实上, 存在一些许多范畴, 有无限多的自边, 比如下面很快被提到的Monoid范畴.

还有, 如果把morphism看作边, (对我来说)很难形象地构造出所谓的composition…

那范畴是什么呢?

说了这么多, 其实范畴$C$就是一个拥有:

对象集合, 即一堆对象组成的集合, 记作 $\operatorname{ob}(C)$
态射集合, 即一堆定义域和值域都是 $\operatorname{ob}(C)$ 里的函数, 记作 $\hom(C)$. 特别地, 给定$a, b \in \operatorname{ob}(C)$, 我们把定义域为$a$且值域为$b$的态射集合记为 $\hom(a, b)$
态射复合, 对于$a, b, c \in \operatorname{ob}(C)$, 态射复合$\circ$是一个函数$\hom(a, b) \times \hom(b, c) \rarr \hom(a, c)$

对于$f \in \hom(a, b)$, 我们顺带还把这句话记作: $f : a \rarr b$

并且 $C$ 和 $\circ$ 还要满足:

存在单位元: 即对任意$a, b \in \operatorname{ob}(C)$, 存在$\mathbf{id_a} : a \rarr a$和$\mathbf{id_b} : b \rarr b$, 对任意$f : a \rarr b$, 有: $$\mathbf{id_a} \circ f = f \circ \mathbf{id_b} = f$$
满足结合律: 即对任意$f : a \rarr b,\quad g: b \rarr c,\quad h: c \rarr d$ 有: $$(f \circ g) \circ h = f \circ (g \circ h) = f \circ g \circ h$$

~~态射(morphism)就是函数的好听的名字, 跟函数交错使用看起来特别错落有致(?).~~

Haskell小课堂: 声明函数 & 复合函数

在Haskell中我们可以通过:

f :: A -> B

来声明一个从类型A到类型B的函数, 以大写字母开头的类型名会被当成具体的类型.

而使用小写字母名开头的类型名会被当成泛化类型, 类似C++中的模板类型参数:

g :: b -> c

函数的复合记作.:

f . g

Part I - What Are Types?

The simplest intuition for types is that they are sets of values.

换句话讲, 类型定义等价于某个集合定义. 当我们说某个东西是什么类型的时候, 我们其实是在说:“看! 这个东西的值只能是这个这个这个这个和这个…!”

因此, 对programmer而言, 我们可以把类型当作对象, 把类型之间的函数当作态射来研究范畴.

我们先从最简单的类型开始看起, 那就是空集$\emptyset$对应的类型Void和只有一个元素的集合().

$\emptyset$ 和 `Void`

简而言之, Void在C++中没有对应类型, 而()对应于C++的void类型.

想象一下, 如果一个函数以Void为输入类型, 那你要怎么调用它呢 – 显然没有任何一个值是属于Void的, 所以你不可能调用它.

f :: Void -> a
f = blabla

f ????

同时, 这时候a是不受任何约束的–也就是说它的返回值是多态(polymorphic)的. 显然这样的函数只能有一个, 标准库(preinclude)里把它定义为:

absurd :: Void -> a

~~荒谬可还行~~

作者还提到在Curry-Howard isomorphism下这个函数代表恒假命题(falsity), 但是这可能要到很久之后了

单集(singleton set) 和 `()`

那么C++里的void对应的是什么呢? 每一个以空参数为输入的函数都是可以调用的, 而且仅能用一种方式调用, 那就是f(). 这说明C++里的void类型对应的集合其实是一个只有一个元素的集合, 简称单集(singleton set或unit set)~~(这个中文翻译我乱蒙的…)~~.

我们来看一些纯的C++函数:

// the answer to life, the universe, and everything
int f42() {
    return 42;
}

int square(int x) {
    return x * x; // 不要担心溢出什么鬼的啦! 
}

int add(int a, int b) {
    return a + b;
}

我们来研究一下他们的参数类型. square只有接受一个类型为int的参数, 它的参数类型显然就是int. 但是add呢? 难道我们要说它有两个参数类型吗? 回想一下我们对类型的"定义": 取值范围的集合. 那么把add的类型定义为两个int之间的类似"集合间的笛卡尔积“的形式是合理的.

有了这个认识, 那void对应的类型, 应该就是0个类型之间的"笛卡尔积"了.

相似地, 在Haskell, 我们也用类似的形式定义一种"复合"类型:

f42 :: () -> Integer
f42 () = 42

square_like_cpp :: (Integer) ->  Integer
square_like_cpp (x) = x * x

square_normal :: Integer -> Integer
square_normal x = x * x


add_like_cpp :: (Integer, Integer) -> Integer
add_like_cpp (x, y) = x + y

add_normal :: Integer -> Integer -> Integer
add_normal x y = x + y

其实我们从这里可以看到一件事实–一个接受多个参数的函数的可以被变成一个接受一个参数并且返回函数的高阶函数, 这叫做Currying(柯里化).

我们可以看到, 通过(类型1, 类型2, ...)可以通过类型间的笛卡尔积构造出新的复合类型, 类似于C++中的tuple(元组)

这时候C++中的void自然就对应于Haskell中的(); Haskell也有一个构造()的函数:

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

类似于absurd在输出类型上是多态的, unit在输入类型上也是多态的.

只有两个元素的集合(二元集): Bool

只要学会如何在Haskell中定义类型. 一种定义方法很简单, 直接枚举类型所能包含的值就好了:

data Bool = True | False

Categories Great and Small

从这里开始, 我们就要认识一些简单的范畴了.

空范畴

就是空的范畴.

如果你硬要一个数学定义的话, 那么一个范畴$C$是空范畴当且仅当其满足:

$$ \operatorname{ob}(C) = \emptyset \\ \hom(C) = \emptyset $$

其实没有对象自然就没有态射…后一条不是必须的

简单图

我们可以简单地从一张有向图及其中节点的可达性生成一个范畴.

更确切地, 对于一张有向图而言, 定义:

有向图中的节点定义为$\operatorname{ob}(C)$
若存在从节点$a$到节点$b$的路径, 那么就往$\hom(C)$里加入态射$a \rarr b$

显然我们的态射有单位元和结合性.

这种构建方法叫free construction, 构建出来的范畴叫free category.

为啥叫free我也不知道….

这种方法的特点就是从给定结构做出最小的扩展然后生成一个合法的范畴

序 Orders

首先来做点概念题. 请解析下面三个名词的区别:

预序(preorder)
偏序(partial order)
全序(total order)

以及严格序和非严格序

(⊙﹏⊙)

序是定义在某个集合上的二元关系; 一个关系就是是一个谓词.

首先我们来抽象出一个定义在集合$A$上的序关系$\backsim$能有什么关系. 令$a,; b,; c$为序上的对象,

自反性. $a \backsim b \lrArr b \backsim a$
传递性. $a \backsim b \land b \backsim c \rArr a \backsim c$