# 翻译-DaoFP-教材01-Clean Slate

{{< ctxset prefix="1" >}}

$$
{\rm \LaTeX}\text{ Definitions are here.}
\let\ph=\phantom
\let\hph=\hphantom
\let\vph=\vphantom
\let\mrel=\mathrel
\let\mbin=\mathbin
\let\mop=\mathop
\let\mclap=\mathclap
\let\mllap=\mathllap
\let\mrlap=\mathrlap
\newcommand{\pla}[1]{\vph{fg}\smash{#1}}                % 打印，限制行高
\newcommand{\vpla}[3][]{\bbox[#2]{\pla{#1 #3}}}         % 打印变量
\newcommand{\cpla}[3][]{\pla{\color{#2}#1 #3}}          % 打印常量
\def\prs#1{\pla{\texttt{(}#1\texttt{)}}}                % 打印括号
\def\bks#1{\pla{\texttt{[}#1\texttt{]}}}                % 打印中括号
\def\brs#1{\pla{\texttt{\{}#1\texttt{\}}}}              % 打印大括号
\def\hole{\pla{\texttt{\_}}}                            % 打印下划线
\def\oprB#1#2{\mbin{\pla{%                              % 打印二元运算符：中缀
  \underset{\mclap{#2}}{#1}%
}}}
\def\oprBhom#1{\mbin{\pla{\cfun{%                       % 打印二元运算符：中缀带箭头
  \xrightarrow[{{\color{black}#1}}]%
}}}}
\def\oprUs#1#2{\mop{\pla{%                              % 打印一元运算符：前缀
  {}_{:\pla{#2}}{#1}
}}}
\newcommand{\vobj}[1][c]{\vpla[\sf]{pink}{#1}}          % 变量：对象
\newcommand{\vcat}[1][C]{\vpla[\sf]{magenta}{#1}}       % 变量：范畴
\newcommand{\varr}[1][f]{\vpla{LightGreen}{#1}}         % 变量：箭头
\newcommand{\vfun}[1][F]{\vpla{LimeGreen}{#1}}          % 变量：函子
\newcommand{\vnat}[1][\eta]{\vpla{LightBlue}{#1}}       % 变量：自然变换
\newcommand{\cobj}[1]{\cpla[\sf]{red}{#1}}              % 常量：对象
\newcommand{\ccat}[1]{\cpla[\sf]{magenta}{#1}}          % 常量：范畴
\newcommand{\carr}[1]{\cpla{Green}{#1}}                 % 常量：箭头
\newcommand{\cfun}[1]{\cpla{ForestGreen}{#1}}           % 常量：函子
\newcommand{\cnat}[1]{\cpla{Cerulean}{#1}}              % 常量：自然变换
\def\objbot{\cobj 0}                                    % 常量：对象 0
\def\objtop{\cobj 1}                                    % 常量：对象 1
\def\catCat{{\ccat{Cat}}}                               % 常量：范畴 Cat
\def\catSet{{\ccat{Set}}}                               % 常量：范畴 Set
\newcommand{\arridt}[1][\vobj]{%                        % 常量：箭头 id
  \oprUs{\carr{\rm id}}{#1}%
}
\newcommand{\funidt}[1][\vcat]{%                        % 常量：函子 Id
  \oprUs{\cfun{\rm Id}}{#1}%
}
\newcommand{\natidt}[1][\vfun]{%                        % 常量：自然变换 id
  \oprUs{\cnat{\iota}}{#1}%
}
\newcommand{\arrabs}[1][\vobj]{%                        % 常量：箭头 ¡
  \oprUs{\carr{\rm\Large¡\hspace{-5px}}}{#1}%
}
\newcommand{\arrbng}[1][\vobj]{%                        % 常量：箭头 !
  \oprUs{\carr{\rm!}}{#1}%
}
\newcommand{\funhom}[1][\vcat]{\oprBhom{#1}}            % 常量：函子 ⇒
\newcommand{\funmul}[1][\vcat]{\oprB{\cfun{\times}}{#1}}% 常量：函子 ×
\newcommand{\funadd}[1][\vcat]{\oprB{\cfun{+}}{#1}}     % 常量：函子 +
\newcommand{\apU}[3][\prs]{%                            % 函数完全应用：一元函数
  \bbox[border: 1px solid gray]{#1{{{#3}\mop{#2}}}}     % #2函数 #3实参
}
\newcommand{\apUN}[3][\prs]{%                           % 函数完全应用：自然变换
  \bbox[border: 1px solid gray]{#1{{{#3}^{#2}}}}        % #2函数 #3实参
}
\newcommand{\apBIa}[4][\prs]{%                          % 函数完全应用：二元函数中缀
  \bbox[border: 1px solid gray]{#1{%                    % #2函数 #3实参a #4实参b
    \bbox[border: 1px solid gray]{{#3}#2{}}{#4}}}       % 先应用实参 a 再应用实参 b
}
\newcommand{\apBIb}[4][\prs]{%                          % 函数完全应用：二元函数中缀
  \bbox[border: 1px solid gray]{#1{{#3}%                % #2函数 #3实参a #4实参b
    \bbox[border: 1px solid gray]{{}#2{#4}}}}           % 先应用实参 b 再应用实参 a
}
\newcommand{\apBIpa}[3][\prs]{%                         % 函数部分应用：二元函数中缀
  \bbox[border: 1px solid gray]{#1{%                    % #2函数 #3实参a
    {#3}#2\hole%
}}}
\newcommand{\apBIpb}[3][\prs]{%                         % 函数部分应用：二元函数中缀
  \bbox[border: 1px solid gray]{#1{%                    % #2函数 #3实参b
    \hole#2{#3}%
}}}
\newcommand{\apBXa}[4][\prs]{%                          % 函数完全应用：二元函数中缀
  \bbox[border: 1px solid gray]{#1{%                    % #2函数 #3实参a #4实参b
    \bbox[border: 1px solid gray]{{}_{#3#2{}}}{#4}}}    % 先应用实参 a 再应用实参 b
}
\newcommand{\apBXb}[4][\prs]{%                          % 函数完全应用：二元函数中缀
  \bbox[border: 1px solid gray]{#1{{}_{#3}%             % #2函数 #3实参a #4实参b
    \bbox[border: 1px solid gray]{{}_{{}#2}{#4}}}}      % 先应用实参 b 再应用实参 a
}
\newcommand{\apBXpa}[3][\prs]{%                         % 函数部分应用：二元函数中缀
  \bbox[border: 1px solid gray]{#1{%                    % #2函数 #3实参a
    {}_{{#3}#2{}}\hole%
}}}
\newcommand{\apBXpb}[3][\prs]{%                         % 函数部分应用：二元函数中缀
  \bbox[border: 1px solid gray]{#1{%                    % #2函数 #3实参b
    {{}_{\hole#2{}}}{#3}%
}}}
$$

$\vobj[c_1], \vcat, \varr, \vfun, \vnat$\
$\catCat, \catSet, \objbot, \objtop, \carr{f}, \cfun{F}, \cnat{\eta}$\
$\vobj[c_1]\funmul\vobj[c_2], \vobj[c_1]\funhom\vobj[c_2]$\
$\arrabs, \arrbng, \arridt$\
$\natidt[\funidt] : \apBIa[]{\funhom[{\apBIa[]{\funhom[\catCat]}\vcat\vcat}]}\funidt\funidt$\
$\begin{aligned}[t]
&\apUN[]{\natidt[\funidt]}\vobj =\\
&\arridt[\apU\funidt\vobj] =\\
&\arridt
\end{aligned}$

$\apU\varr{\vobj[c_1]}, \apUN\vnat{\vobj[c_1]}$\
$\apBIa{\funhom[\vcat]}{\vobj[c_1]}{\vobj[c_2]},
 \apBIb{\funhom[\vcat]}{\vobj[c_1]}{\vobj[c_2]}$\
$\apBIpa{\funhom[\vcat]}{\vobj[c_1]},
 \apBIpb{\funhom[\vcat]}{\vobj[c_2]}$\
$\apBXa{\funhom[\vcat]}{\vobj[c_1]}{\vobj[c_2]},
 \apBXb{\funhom[\vcat]}{\vobj[c_1]}{\vobj[c_2]}$\
$\apU{\apBXpa{\funhom[\vcat]}{\vobj[c_1]}}{\vobj[c_2]},
 \apU{\apBXpb{\funhom[\vcat]}{\vobj[c_2]}}{\vobj[c_1]}$

编程始于类型和函数。
你或许对类型和函数有一些先入为主的看法：
请抛弃它们！它们只会让你的思维变得混乱。
不要去思考计算机在硬件层面上是如何实现的：
计算机只是众多计算模型中的一种，我们不应该对它产生依恋。
你可以在脑海中进行计算，也可以用笔和纸进行计算。
物理基础对于编程的概念来说是无关紧要的。

## 1.1. 类型和函数 Types and Functions {#S1-1}
{{< ctx level="2" >}}

借用老子的名言：“道（类型）可道（如果可被描述），非常道（那它就不是永恒的类型）”。
换句话说，类型是一个原始概念，它无法被定义。

与其称其为**类型 Type**，不如称其为**对象 Object** 或**命题 Proposition** ——
这是不同数学领域（类型理论、范畴理论、逻辑学）对它的称呼。

类型可能存在不止一种，因此我们需要一种方式来命名它们。
我们可以用手指指向它们，但为了能与他人有效沟通，通常会给它们起名字：
我们后面可能会讨论到类型 $\vobj[c_1]$、$\vobj[c_2]$、$\vobj[c_3]$ 或者是 `Int`、`Bool`、`Double` 等。
这些不过是些名称罢了。

类型本身没有意义，它们的特殊之处在于自己与其他类型之间的联系。
这些联系通过箭头来描述。一个箭头以一个类型作为其**源头 Source**，并以另一个类型作为其**目标 Target**。
目标类型可以与源头类型相同，这种情况下箭头会形成一个回环。

类型之间的箭头被称为**函数 Function**。
对象之间的箭头被称为**态射 Morphism**。
命题之间的箭头被称为**蕴涵命题的证明 Entailment**。
这些术语不过是不同数学领域对箭头的不同称呼罢了，你可以将它们互换使用。

命题是可能为真的事物。在逻辑学中，
我们将两个对象之间的箭头解释为 $\vobj[c_1]$ 蕴涵 $\vobj[c_2]$，
或者说 $\vobj[c_2]$ 可以从 $\vobj[c_1]$ 中推导出来。

由于两个类型之间可能存在不止一个箭头，
因此我们需要给它们命名。比方说这里有一个名为 $\varr$ 的箭头，
它从类型 $\vobj[c_1]$ 指向类型 $\vobj[c_2]$：

$\qquad\xymatrix{
\vobj[c_1] \ar[r]^{\varr} & \vobj[c_2]
}$

一种解释是说 $\varr$ 是一个函数，
接收一个类型为 $\vobj[c_1]$ 的实参，
输出一个类型为 $\vobj[c_2]$ 的结果；
或者也可以说 $\varr$ 是一个证明：
如果 $\vobj[c_1]$ 存在证明，
那么 $\vobj[c_2]$ 也存在证明。

注：类型理论、Lambda 演算（编程理论的基础）、逻辑学和范畴理论之间的联系被称为 **Curry-Howard-Lambek 对应 Curry-Howard-Lambek correspondence**，又称**命题即类型 Proposition as Type**。

## 1.2. 阴和阳 Yin and Yang {#S1-2}

一个对象是由它们之间的联系所定义的。
一个箭头代表了一个证明，一个证据，证明两个对象之间是有联系的。证明
可以不存在——此时两个对象是断开的；也可以
存在很多个；或者也可以
只存在一个——此时两个对象间只有唯一的箭头。

那么**唯一 Unique** 意味着什么呢？它意味着：
如果能找到两个这样的箭头，那么它们必须是相等的。

如果一个对象对其他任意对象 $\vobj$ 都只存在唯一的从自身射入 $\vobj$ 的箭头，
那么这个对象就称作是**始对象 Initial Object**。

始对象的对偶是一个对象，满足对其他任意对象 $\vobj$ 都只存在唯一的从 $\vobj$ 射入自身的箭头。
这个对象称作是**终对象 Terminal Object**。

始对象在范畴理论中通常用 $\objbot$ 表示，而终对象则用 $\objtop$ 表示。

从 $\objbot$ 射向任意对象 $\vobj$ 的箭头记作 $\arrabs$，
通常只用 $\arrabs$ 来表示。

从任意对象 $\vobj$ 射向 $\objtop$ 的箭头记作 $\arrbng$，
通常只用 $\arrbng$ 来表示。

始对象是一切的源头。
作为一个 Haskell 中的类型，它被称为 `Void`，象征着一切事物的混沌起源。
由于存在着从 `Void` 到一切对象的箭头，
因此也存在从 `Void` 到 `Void` 自身的箭头。

$\qquad\xymatrix{
  \objbot\ar@`{p+/ul+5pc/,p+/ur+5pc/}[]^{\arridt[\objbot] = \arrabs[\objbot]}
}$

尼采可能会说：“虚无凝视着你。”

终对象则统一了一切。作为一个类型，它被称为 `()`。

终对象在逻辑学中象征着终极真理，
它可以用 T 或 $\top$ 来表示。
由于对任意对象 $\vobj$ 都存在着从 $\vobj$ 指向终对象的箭头，
因此这意味着无论你的假设是什么 $\top$ 都是恒为真的。

与前者对偶，始对象则象征着逻辑学中的虚假、矛盾或反事实。
它被写作 False 并且可以用倒置的 T（即 $\bot$）来表示。
由于对任意对象 $\vobj$ 都存在从始对象指向 $\vobj$ 的箭头，
因此这意味着你可以从错误的前提中推出一切。

英语中存在着一种特殊的语法结构可以用于表达反事实的蕴涵。
当我们说 “If wishes were horses, beggars would ride” 时，
我们想表达的是：愿望与马之间的相等意味着乞丐应该能够骑马。但我们知道这个前提是错误的。

一门编程语言让我们能够与彼此以及计算机进行交流。
某些语言对于计算机来说会更容易理解，而其他语言则更接近理论。
我们将使用 Haskell 作为一种妥协。

在 Haskell 中，终对象的名称是 `()`，一对空括号，读作 Unit。
这个符号在后面会有更深入的解释。

在 Haskell 中存在着许多类型，并且
从 `Void` 到每一个类型都存在着唯一的函数/箭头。
这些箭头都有着相同的名称，即 `absurd`。

| Haskell          | 范畴理论                    | 逻辑学               |
| ---------------- | -------------------------- | ------------------- |
| 类型 Type         | 对象 Object                | 命题 Proposition     |
| 函数 Function     | 态射 Morphism / 箭头 Arrow  | 蕴含命题的证明 Implication |
| 底类型 `Void`     | 始对象 $\objbot$            | 假命题 False         |
| 顶类型 `()`       | 终对象 $\objtop$            | 真命题 True          |

## 1.3. 元素 Elements {#S1-3}
{{< ctx level="2" >}}

一个对象可能没有组成部分，但是它可能具有结构。
对象的结构由指向该对象的箭头所定义。我们可以用箭头来**探测**这个对象。

在编程和逻辑学中，我们希望始对象没有任何结构；因此我们假设：
除了从它自身出发的箭头之外，不存在其他任何以始对象为目标的箭头。因此 `Void` 没有结构。

而终对象则具有最简单的结构：对于其他任何对象，
以自身为源头并以终对象为目标的箭头只能有一个——这意味着
从其他任意对象出发只有唯一一种探测终对象的方式。
从这个意义上来说，终对象就像是一个不可分割的点：
其仅有的属性就是其存在性，而其存在性则由所有
以其为目标的箭头所证明。

终对象是如此简单，以至于它可被用来探测其他更复杂的对象。

如果对于某个对象 $\vobj$ 存在着不止一条从终对象出发并射向它的箭头，
那么 $\vobj$ 便具有某种结构，探测它的方式便有不止一种。
由于终对象的行为就像一个点，因此一个从终对象射出的箭头
就可以被视作是一个从箭头的目标对象中挑选出的元素。

在范畴理论中，我们将满足下述条件的 $\varr[c]$ 称作是
$\vobj$ 的一个**全局元素 Global Element**：

$\qquad\xymatrix{
  \objtop \ar[r]^{\varr[c]} & \vobj
}$

我们通常会直接将全局元素称作是元素（即省略“全局”一词）。
终对象是一个**原型 Archetypal** 元素。通常数学家们
会将这样的原型称作**行走的 Walking** 东西。
在这里 $\objtop$ 就是一个“行走的元素”。

> 据说“行走的”这种用法来自于
> 称呼某人为“行走的眉毛”（意味着这个人的大眉毛非常显眼）；或者是
> 称呼某人为“行走的字典”（意味着这个人的词汇量非常丰富）

在类型理论中，$\varr[c] : \vobj$ 表示
$\varr[c]$ 是一个类型为 $\vobj$ 的元素。

在 Haskell 中我们则会使用双冒号，即 `c :: C`（Haskell
的惯例是具体类型用大写字母表示，类型变量用小写字母表示）。

在类型理论中我们会说 `c` 是一个类型为 `C` 的项，但是
在范畴理论中我们会将其解释为一个箭头 $\varr[c] : \apBIa[]\funhom\objtop\vobj$，
也就是 `C` 的一个全局元素。

> 在 Haskell 的类型系统中会对
> `c :: C` 和 `c :: () -> C` 进行区分。
> 尽管如此，它们在范畴语义中的含义是相同的。

在逻辑学中像 $\varr[c]$ 这样的箭头会被解释为是 $\vobj$ 的一个证明，
因为其对应于蕴涵 $\top \Rightarrow \vobj$（若 $\top$ 为真则 $\vobj$ 也为真）。
注意到 $\vobj$ 可能存在着不止一个证明。

由于前面已经假设以其他对象为源头并以 `Void` 为目标的箭头不存在，
因此 `Void` 没有任何元素。正因如此，`Void` 被认为是**空的 Empty**。

由于终对象只存在着唯一的一条从自身出发并射向自身的箭头，
即 $\arridt[\objtop]: \apBIa[]\funhom\objtop\objtop$；
因此它只有一个元素。正因如此，终对象有时也会被称作是**单元素集 Singleton**。

注意：范畴理论并没有规定以始对象为目标的箭头不存在，
然而这在我们所研究的笛卡尔闭范畴中是不被允许的。

### 1.3.1. The Foundations {#S1-3-1}
{{< ctx level="3" >}}

Programming is engineering and as such it necessarily involves some mathematics. But unlike other branches of engineering, 
it can actually be used to encode mathematics from first principles.
But where does mathematics start?

There is no consensus among mathematicians about 
what constitutes the foundations of mathematics. 
The interpretation of programs as mathematical objects depends on this choice.

The traditional approach is to start with set theory. 
Types are interpreted as sets of elements. 
The declaration `c :: C` can be interpreted in set-theoretical language as 
“$\varr[c]$ is an element of the set $\vobj$”:

$\qquad \varr[c] \in \vobj$

The problem with this interpretation is that 
it introduces spurious degrees of freedom. 
In set theory, $\varr[c] \in \vobj$ is a predicate, which can be true or false. 
In programming, this would allow us to write nonsensical code, like:

```haskell {wrapper=false, lineNos=false}
if c :: C then ...
```

The alternative foundation of mathematics 
is based on Martin-Löf type theory. In it,
$\varr[c] : \vobj$ is a **judgement** — a statement of fact. 
You cannot define a value without specifying its type, and
the type is permanently affixed to it.

There are rules for building new types, and
ruiles for constructing values of these types.

Let's see how they work for the two types we've introduced so far.

The set-theoretical interpretation of `Void` 
is an empty set denoted by $\varnothing$. 
The interpretation of the unit type `()` 
is a singleton set $\objtop$.

In type theory we postulate 
the existence of the corresponding types $\objbot$ and $\objtop$.

To make sure that the type $\objbot$ is not inhabited,
we provide no rule for constructing values of this type.
It has no data constructor or, as it's called in type theory,
no **Introduction Rule**.

But if that wasn't enough, we also provide an impossible to 
satisfy elimination rule. The **Elimination Rule** tells us
what we can do with an input of the type in question.
Since we are guaranteed that nobody can create an element of $\objbot$,
we are free to promise **anything** if somebody comes up with one (they can't!).
Give me an element $\vobj: \objbot$ and I will give you back any value of any type.
In category theory, this corresponds to the arrow $\arrabs$ we have seen before.

The $\objtop$ type has a single data constructor,
corresponding to the Haskell value `()`, which in type theory
is often depicted as $*$. The introduction rule is simply:

$\qquad *: \objtop$

The construction of $*$ requires no assumptions.
It can be created by flat whenever the need arises. 

The elimination rule states that any function 
$\apBIa[]\funhom\objtop\vobj$ is fully determined by its value at $*$:
In category theory this is the definition of the global element of $\vobj$.
It makes perfect sense if $*$ is the only element of $\objtop$.

---

> 作者: [Bartosz Milewski](https://bartoszmilewski.com/)  
> URL: https://ych817.github.io/posts/f28061e/