Haskell/Denotational semantics

介绍

本章解释如何将 Haskell 程序的意义形式化，即Denotational Semantics。正式指定程序 square x = x*x 与将每个数字映射到其平方的数学平方函数具有相同的意义，这似乎是在吹毛求疵，但程序 f x = f (x+1) 的意义如何？该程序会永远循环。在接下来的内容中，我们将举例说明 Scott 和 Strachey 首次采用的方法，并为推理一般函数式程序以及特别是递归定义的正确性奠定基础。当然，我们将集中于那些理解 Haskell 程序所需的主题。

本章的另一个目的是说明严格和惰性的概念，这些概念体现了函数是否需要或不需要计算其参数的思想。这是预测 Haskell 程序计算过程的基本要素，因此对程序员来说是最重要的。有趣的是，这些概念可以用 Denotational Semantics 本身简洁地表述，无需引用执行模型。它们将在图约简中得到很好的应用，但正是本章将使读者熟悉 Denotational 定义和相关概念，例如 ⊥（“Bottom”）。只对严格性感兴趣的读者可能希望浏览Bottom 和偏函数部分，并快速转到严格和非严格语义部分。

什么是Denotational Semantics，它有什么用？

Haskell 程序的意义是什么？Denotational Semantics 为这个问题提供了答案。通常，编程语言的 Denotational Semantics 将每个程序映射到一个数学对象（语义），该对象代表了所讨论程序的意义。例如，Haskell 程序 10、9+1、2*5 和 sum [1..4] 的数学对象可以用整数10来表示。我们说所有这些程序都表示整数10。这样的数学对象的集合称为语义域。

从程序代码到语义域的映射通常用程序代码周围的双方括号（“牛津括号”）来写下。例如，

$[\![{\texttt {2*5}}]\!]=10.$

语义是可组合的，也就是说，程序 1+9 的意义只取决于其组成部分的意义

$[\![{\texttt {a+b}}]\!]=[\![{\texttt {a}}]\!]+[\![{\texttt {b}}]\!].$

相同的符号用于类型，即

$[\![{\texttt {Integer}}]\!]=\mathbb {Z} .$

但是，为了简单起见，在后续章节中，我们将隐式地将表达式与其语义对象等同起来，并且仅在需要澄清时使用此符号。

Haskell 等纯粹函数式语言的一个关键属性是，像“1+9 代表 10”这样的直接数学解释也适用于函数：本质上，类型为 Integer -> Integer 的程序的语义是数学函数 $\mathbb {Z} \to \mathbb {Z}$，它在整数之间进行映射。虽然我们会看到这种表达方式通常需要改进，以包括非终止情况，但对于命令式语言来说情况明显更糟：具有该类型过程表示的是某种可能会以意外方式改变机器状态的东西。命令式语言与操作语义紧密相连，后者描述了它们在机器上的执行方式。可以为命令式程序定义一个语义语义，并用它来推理这些程序，但语义通常具有操作性质，有时与函数式语言的语义语义相比必须进行扩展。^[2] 相反，纯粹函数式语言的含义默认情况下完全独立于它们的执行方式。Haskell98 标准甚至只指定了 Haskell 的非严格语义语义，而没有规定如何实现它们。

最终，语义语义使我们能够开发出正式的证明，证明程序确实以数学方式执行了我们想要它们执行的操作。具有讽刺意味的是，为了在日常 Haskell 中证明程序属性，可以使用等式推理，它将程序转换为等效程序，而无需过多地查看我们在本章中关注的底层数学对象。但是，语义语义实际上出现在我们必须对非终止程序进行推理时，例如在无限列表中。

当然，因为它们只说明了程序是什么，所以语义语义无法回答有关程序运行多长时间或消耗多少内存的问题；这由求值策略控制，该策略规定计算机如何计算表达式的范式。另一方面，实现必须尊重语义，在一定程度上，语义决定了如何在机器上求值 Haskell 程序。我们将在严格和非严格语义中详细说明这一点。

选择什么作为语义域？

现在我们正在寻找合适的数学对象，我们可以将这些对象归因于每个 Haskell 程序。对于示例10、2*5 和 sum [1..4]，很明显所有表达式都应该表示整数 10。概括地说，类型为 Integer 的每个值 x 可能表示集合 $\mathbb {Z}$ 中的元素。对于像 f :: Integer -> Integer 这样的函数，我们可以诉诸于“函数”的数学定义，它是一组 (参数，值) 对，即其图。

但是，将函数解释为它们的图太快了，因为它不适用于递归定义。考虑以下定义

shaves :: Integer -> Integer -> Bool
1 `shaves` 1 = True
2 `shaves` 2 = False
0 `shaves` x = not (x `shaves` x)
_ `shaves` _ = False

我们可以将 0、1 和 2 视为长胡子的男性，问题是谁给谁刮胡子。人物 1 自己给自己刮胡子，但 2 由理发师 0 刮胡子，因为求值第三个等式得到 0 `shaves` 2 == True。一般来说，第三行说理发师 0 给所有不给自己刮胡子的人刮胡子。

那么理发师自己呢，0 `shaves` 0 是真还是假？如果它是真的，那么第三个等式说它不是真的。如果它不是真的，那么第三个等式说它是真的。我们感到困惑，我们看到我们无法将 True 或 False 归因于 0 `shaves` 0；我们用来解释函数 shaves 的图必须有一个空位。我们意识到我们的语义对象必须能够包含偏函数，这些函数对于其参数的某些值是未定义的（..否则参数类型允许）。

众所周知，这个著名的例子引发了集合论中严重的奠基问题。它是一个非预测性定义的例子，一个使用自身的定义，一个逻辑循环。不幸的是，对于递归定义来说，循环不是问题，而是特征。

底部和偏函数

⊥ 底部

为了定义偏函数，我们引入了一个特殊的值 ⊥，称为底部，通常用打字机字体写成 _|_。我们说 ⊥ 是完全“未定义”的值或函数。每个基本数据类型，例如 Integer 或 ()，除了其通常的元素外，还包含一个 ⊥。因此，类型 Integer 的可能值为

$\bot ,0,+1,-1,+2,-2,+3,-3,\dots$

将 ⊥ 添加到值集中也称为提升。这通常用下标表示，例如在 $\mathbb {Z} _{\bot }$ 中。虽然这是数学集合“提升的整数”的正确表示法，但我们更喜欢谈论“类型为 Integer 的值”。我们这样做是因为 $\mathbb {Z} _{\bot }$ 暗示存在“真实”整数 $\mathbb {Z}$，但在 Haskell 内部，“整数”是 Integer。

作为另一个例子，只有一个元素的类型 () 实际上有两个居民

$\bot ,()$

目前，我们将坚持使用Integer进行编程。任意代数数据类型将在代数数据类型部分进行处理，因为严格和非严格语言在这些类型如何包含⊥方面存在分歧。

在Haskell中，表达式undefined表示⊥。借助它，确实可以验证实际Haskell程序的一些语义属性。undefined具有多态类型forall a . a，当然可以将其专门化为undefined :: Integer，undefined :: ()，undefined :: Integer -> Integer等等。在Haskell Prelude中，它被定义为

undefined = error "Prelude.undefined"

作为旁注，从Curry-Howard 同构可以得出，任何多态类型forall a . a的值都必须表示⊥。

偏函数和语义近似顺序

现在，$\bot$使我们有可能拥有偏函数

$f(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\-2&{\mbox{ if }}n{\mbox{ is }}1\\\bot &{\mbox{ else }}\end{cases}}$

这里，$f(n)$为$n=0$和$n=1$产生明确定义的值，但对于所有其他$n$产生$\bot$。

类型Integer -> Integer也有其$\bot$，它使用来自Integer的$\bot$以这种方式定义

$\bot (n)=\bot$ 对于所有$n$

其中，左侧的$\bot$类型为Integer -> Integer，右侧的类型为Integer。

为了形式化，偏函数，比如类型为Integer -> Integer的函数，至少是从提升的整数$\mathbb {Z} _{\bot }=\{\bot ,0,\pm 1,\pm 2,\pm 3,\dots \}$到提升的整数的数学映射。但这还不够，因为它没有承认$\bot$的特殊作用。例如，定义

$g(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}\bot \\\bot &{\mbox{ else }}\end{cases}}$

是一个将无限循环转换为终止程序，反之亦然的函数，这解决了停机问题。当$g(1)$ 未定义时，$g(\bot )$ 如何产生一个定义值？直觉是，每个偏函数$g$ 应该对更确定的参数产生更多确定的答案。为了形式化，我们可以说每个具体数字都比$\bot$ **更确定**。

$\bot \sqsubset 1\ ,\ \bot \sqsubset 2\ ,\dots$

这里，$a\sqsubset b$ 表示$b$ 比$a$ 更确定。类似地，$a\sqsubseteq b$ 将表示$b$ 比$a$ 更确定，或者两者相等（因此具有相同的确定性）。$\sqsubset$ 也被称为 **语义近似序**，因为我们可以用更不确定的值来近似确定值，从而将“更确定”解释为“更好地近似”。当然，$\bot$ 被设计为数据类型的最小元素，我们总是有$\bot \sqsubset x$ 对于所有$x$，除了$x$ 恰好表示$\bot$ 本身的情况。

$\forall x\neq \bot \ \ \ \bot \sqsubset x$

由于没有一个数字比另一个数字更“定义明确”，因此数学关系 $\sqsubset$ 对任何一对数字都是假的。

$1\sqsubset 1$ 不成立。 无论是 $1\sqsubset 2$ 还是 $2\sqsubset 1$ 都不能成立。

这与普通的顺序谓词 $\leq$ 形成对比，后者可以比较任何两个数字。记住这一点的一个快速方法是这句话：“$1$ 和 $2$ 在“信息含量”方面不同，但在“信息量”方面相等”。这也是我们使用不同符号的原因：$\sqsubseteq$。

无论是 $1\sqsubseteq 2$ 还是 $2\sqsubseteq 1$ 都不能成立， 但 $1\sqsubseteq 1$ 成立。

人们说 $\sqsubseteq$ 指定了一个偏序，并且类型为Integer的值构成一个偏序集（简称poset）。偏序的特点是以下三个定律

• 自反性，任何事物都与其自身一样定义明确：$x\sqsubseteq x$ 对所有 $x$
• 传递性：如果 $x\sqsubseteq y$ 并且 $y\sqsubseteq z$，那么 $x\sqsubseteq z$
• 反对称性：如果 $x\sqsubseteq y$ 和 $y\sqsubseteq x$ 都成立，那么 $x$ 和 $y$ 必须相等：$x=y$。

练习
整数集关于 ≤ 序关系是否构成偏序集？

我们可以通过下面的图来描述 Integer 类型的值上的 ≤ 序关系：

其中每个节点之间的连线表示上面的节点比下面的节点定义更完整。因为只有一个层次（不包括 ⊥），所以我们说 Integer 是一个**扁平域**。这幅图也解释了 ⊥ 的名称：它被称为**底**，因为它总是位于最底部。

单调性

我们对偏函数的直觉现在可以表述如下：每个偏函数 f 都是偏序集之间的**单调**映射。定义更完整的参数将产生定义更完整的值

$x\sqsubseteq y\Rightarrow f(x)\sqsubseteq f(y)$

特别是，一个单调函数 h 满足 h(⊥) = 1，它是一个常数函数：对于所有 n，都有 h(n) = 1。请注意，这里至关重要的是 1 ≤ 2 等等不成立。

翻译成 Haskell，单调性意味着我们不能使用 ⊥ 作为条件，即我们不能对 ⊥ 或其等价物 undefined 进行模式匹配。否则，上面提到的 g 的例子就可以用 Haskell 程序来表达。正如我们将在后面看到的那样，⊥ 也表示非终止程序，因此在 Haskell 中无法观察到 ⊥ 与停机问题有关。

当然，"定义更完整"的概念可以通过以下方式扩展到偏函数：如果一个函数在每个可能的参数上都比另一个函数定义更完整，那么它就比另一个函数定义更完整

$f\sqsubseteq g{\mbox{ if }}\forall x.f(x)\sqsubseteq g(x)$

因此，偏函数也构成一个偏序集，其中未定义函数 ⊥(x) = ⊥ 是最小元素。

递归定义作为不动点迭代

阶乘函数的近似值

现在我们有了描述偏函数的方法，可以对递归定义进行解释。让我们以阶乘函数 $f(n)=n!$ 为例，其递归定义为

$f(n)={\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n\cdot f(n-1)$

虽然我们看到将这个递归函数直接解释为集合描述可能会导致问题，但我们直观地知道，为了计算 $f(n)$ 对于给定的每一个 $n$，我们必须迭代右手边。这个迭代可以形式化如下：我们计算一个函数序列 $f_{k}$，每个函数都由右手边应用于前面的函数组成，即

$f_{k+1}(n)={\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n\cdot f_{k}(n-1)$

我们从未定义函数 $f_{0}(n)=\bot$ 开始，得到的偏函数序列如下

$f_{1}(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\\bot &{\mbox{ else }}\end{cases}}\ ,\ f_{2}(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\1&{\mbox{ if }}n{\mbox{ is }}1\\\bot &{\mbox{ else }}\end{cases}}\ ,\ f_{3}(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\1&{\mbox{ if }}n{\mbox{ is }}1\\2&{\mbox{ if }}n{\mbox{ is }}2\\\bot &{\mbox{ else }}\end{cases}}$

等等。显然，

$\bot =f_{0}\sqsubseteq f_{1}\sqsubseteq f_{2}\sqsubseteq \dots$

我们期望这个序列收敛于阶乘函数。

迭代遵循着著名的不动点迭代方案

$x_{0},g(x_{0}),g(g(x_{0})),g(g(g(x_{0}))),\dots$

在本例中，$x_{0}$ 是一个函数，而 $g$ 是一个 泛函，它将函数映射到另一个函数。我们有

$x_{0}=\bot$ 以及

$g(x)=n\mapsto {\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n*x(n-1)\,$

如果我们从 $x_{0}=\bot$ 开始，迭代将产生越来越接近阶乘函数的定义

$\bot \sqsubseteq g(\bot )\sqsubseteq g(g(\bot ))\sqsubseteq g(g(g(\bot )))\sqsubseteq \dots$

(证明序列递增：第一个不等式 $\bot \sqsubseteq g(\bot )$ 来自于 $\bot$ 比任何其他东西都少定义。第二个不等式来自第一个不等式，通过将 $g$ 应用于两边并注意到 $g$ 是单调的。第三个来自第二个，以同样的方式，等等。）

用 Haskell 表达这种迭代方案非常具有说明性。由于泛函只是普通的更高阶函数，所以我们有

g :: (Integer -> Integer) -> (Integer -> Integer)
g x = \n -> if n == 0 then 1 else n * x (n-1)

x0 :: Integer -> Integer
x0 = undefined

(f0:f1:f2:f3:f4:fs) = iterate g x0

现在我们可以对函数 f0,f1,... 进行示例参数评估，并查看它们是否产生 undefined。

 > f3 0
 1
 > f3 1
 1
 > f3 2
 2
 > f3 5
 *** Exception: Prelude.undefined
 > map f3 [0..]
 [1,1,2,*** Exception: Prelude.undefined
 > map f4 [0..]
 [1,1,2,6,*** Exception: Prelude.undefined
 > map f1 [0..]
 [1,*** Exception: Prelude.undefined

当然，我们不能用它来检查 f4 是否真的对所有参数都是 undefined。

收敛

对于数学家来说，这个问题是这个逼近序列是否收敛仍然需要解答。为此，我们说一个偏序集是一个 有向完全偏序集 (dcpo) 当且仅当每个单调序列 $x_{0}\sqsubseteq x_{1}\sqsubseteq \dots$ （也称为 链）都有一个最小上界（上确界）

$\sup _{\sqsubseteq }\{x_{0}\sqsubseteq x_{1}\sqsubseteq \dots \}=x$.

如果是这样的话，对于语义逼近顺序，我们可以清楚地确定，逼近阶乘函数的单调函数序列确实有一个极限。对于我们的语义解释，我们将只遇到具有最小元素 $\bot$ 的 dcpos，它们被称为 完全偏序集 (cpo)。

Integers 明显构成一个 (d)cpo，因为由两个以上元素组成的单调序列必须是以下形式

$\bot \sqsubseteq \dots \sqsubseteq \ \bot \sqsubseteq n\sqsubseteq n\sqsubseteq \dots \sqsubseteq n$

其中 $n$ 是一个普通数字。因此，$n$ 已经是最小上界。

对于函数 Integer -> Integer，这个论据不成立，因为单调序列可能具有无限长度。但由于 Integer 是一个 (d)cpo，我们知道对于每个点 $n$，存在一个最小上界

$\sup _{\sqsubseteq }\{\bot =f_{0}(n)\sqsubseteq f_{1}(n)\sqsubseteq f_{2}(n)\sqsubseteq \dots \}=:f(n)$.

由于语义近似顺序是逐点定义的，函数 $f$ 是我们寻找的最小上界。

这些是我们将阶乘函数的非谓词定义转化为一个定义明确的构造的目标的最后几步。当然，还需要证明 $f(n)$ 实际上对于每个 $n$ 都能产生一个定义的值，但这并不难，而且比一个完全形式错误的定义更合理。

底部包含非终止

尝试将我们新获得的对递归定义的洞察应用于一个不终止的例子，这是很有启发性的。

$f(n)=f(n+1)$

近似序列如下

$f_{0}=\bot ,f_{1}=\bot ,\dots$

并且只包含 $\bot$。显然，得到的极限是 $\bot$。从操作的角度来看，执行此程序的机器将无限循环。因此，我们看到 $\bot$ 也可能表示一个 **非终止** 函数或值。因此，鉴于停机问题，在 Haskell 中对 $\bot$ 进行模式匹配是不可能的。

最小不动点的解释

早些时候，我们将近似序列称为众所周知的“不动点迭代”方案的一个例子。当然，阶乘函数的定义$f$也可以被认为是泛函$g$的不动点规范。

$f=g(f)=n\mapsto {\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n\cdot f(n-1)$

然而，可能存在多个不动点。例如，存在多个$f$满足规范

$f=n\mapsto {\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}f(n+1)$,

当然，当执行这样的程序时，机器将在$f(1)$或$f(2)$上无限循环，因此不会产生关于$f(1)$值的有价值信息。这对应于选择最不确定的不动点作为语义对象$f$，这实际上是一个规范选择。因此，我们说

$f=g(f)$,

定义了$g$的最小不动点$f$。显然，最小是相对于我们的语义近似顺序$\sqsubseteq$。

如果我们添加一个条件，即$g$必须是连续的（有时也称为“链连续”），那么我们就可以保证最小不动点的存在。这意味着$g$尊重单调序列的上确界

$\sup _{\sqsubseteq }\{g(x_{0})\sqsubseteq g(x_{1})\sqsubseteq \dots \}=g\left(\sup _{\sqsubseteq }\{x_{0}\sqsubseteq x_{1}\sqsubseteq \dots \}\right)$

然后我们可以争论，用

$f=\sup _{\sqsubseteq }\{x_{0}\sqsubseteq g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}$

我们有

${\begin{array}{lcl}g(f)&=&g\left(\sup _{\sqsubseteq }\{x_{0}\sqsubseteq g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}\right)\\&=&\sup _{\sqsubseteq }\{g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}\\&=&\sup _{\sqsubseteq }\{x_{0}\sqsubseteq g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}\\&=&f\end{array}}$

并且迭代极限确实是 $g$ 的一个不动点。你可能也想要说服自己，不动点迭代产生的不动点是 *最小的* 不动点。

练习
证明由以 $x_{0}=\bot$ 为起点的不动点迭代获得的不动点也是最小的不动点，即它小于任何其他不动点。(提示：$\bot$ 是我们 cpo 的最小元素，而 $g$ 是单调的)

顺便说一句，我们怎么知道我们写下的每个 Haskell 函数确实是连续的？就像单调性一样，这必须由编程语言强制执行。诚然，这些属性可以在一定程度上随意地强制执行或破坏，所以这个问题感觉有点空洞。但直观地说，单调性通过不允许对 $\bot$ 进行模式匹配来保证。对于连续性，我们注意到对于任意类型 a，每个简单函数 a -> Integer 自动是连续的，因为 Integer 的单调序列是有限长度的。任何类型 a 的无限链都映射到 Integer 的有限链，对上确界的尊重成为单调性的结果。因此，Integer -> Integer 特殊情况的所有函数都必须是连续的。对于像 $g$::(Integer -> Integer) -> (Integer -> Integer) 这样的泛函，连续性则是由于柯里化而实现的，因为该类型与 ::((Integer -> Integer), Integer) -> Integer 同构，我们可以取 a=((Integer -> Integer), Integer)。

在 Haskell 中，阶乘函数的固定解释可以编码为

factorial = fix g

借助于不动点组合子

fix :: (a -> a) -> a.

我们可以通过以下方式定义它

fix f = let x = f x in x

这让我们有点困惑，因为当展开 $factorial$ 时，结果与我们在 Haskell 中第一次定义阶乘函数的方式没有什么不同。但当然，这整个部分所讨论的构造在运行真正的 Haskell 程序时根本不存在。它只是一种将 Haskell 程序的数学解释放在牢固基础上的方法。然而，我们可以借助于 undefined 在 Haskell 本身中探索这些语义，这非常棒。

严格语义和非严格语义

在详细阐述了 Haskell 程序的语义解释之后，我们将放弃用于语义对象的数学函数符号 $f(n)$，而采用现在等效的 Haskell 符号 f n。

严格函数

一个只有一个参数的函数 f 被称为 **严格** 函数，当且仅当

f ⊥ = ⊥.

以下是一些严格函数的例子

id     x = x
succ   x = x + 1
power2 0 = 1
power2 n = 2 * power2 (n-1)

它们没有什么出奇之处。但为什么它们是严格的呢？证明这些函数确实是严格的很有启发性。对于 id，这来自定义。对于 succ，我们必须思考 ⊥ + 1 是 ⊥ 还是不是。如果不是，那么例如我们应该有 ⊥ + 1 = 2 或者更一般地 ⊥ + 1 = k，其中 k 是某个具体数字。我们记得每个函数都是 *单调* 的，所以例如我们应该有

2 = ⊥ + 1 ⊑ 4 + 1 = 5

因为 ⊥ ⊑ 4。但 2 ⊑ 5、2 = 5 或者 2 ⊒ 5 都不成立，所以 k 不能是 2。一般来说，我们得到矛盾

k = ⊥ + 1 ⊑ k + 1 = k + 1.

因此，唯一可能的选择是

succ ⊥ = ⊥ + 1 = ⊥

所以 succ 是严格的。

练习
证明 power2 是严格的。虽然可以基于“显而易见”的事实，即 power2 n 等于 $2^{n}$，但最好使用不动点迭代法来证明。

非严格和严格语言

寻找非严格函数时，发现只有一种类型为 Integer -> Integer 的非严格函数原型。

one x = 1

它的变体是 const k x = k，对于每个具体数字 k。为什么这些是唯一可能的？记住，one n 的定义不能少于 one ⊥。由于 Integer 是一个扁平域，两者必须相等。

为什么 one 是非严格的？为了证明它是，我们使用一个 Haskell 解释器并尝试

> one (undefined :: Integer)
1

它不是 ⊥。这是合理的，因为 one 完全忽略了它的参数。在操作意义上将 ⊥ 解释为“非终止”，可以说 one 的非严格性意味着它不会强制评估它的参数，因此在评估参数 ⊥ 时避免了无限循环。但也可以说，每个函数都必须在计算结果之前评估它的参数，这意味着 one ⊥ 也应该等于 ⊥。也就是说，如果计算参数的程序没有停止，one 也应该不会停止。 ^{这表明，可以自由选择函数式编程语言的这种设计或另一种设计。如果函数默认情况下是严格的或非严格的，则称该语言是严格的或非严格的。Haskell 选择的是非严格语言。相反，函数式语言 ML 和 Lisp 选择了严格语义。}

具有多个参数的函数

严格性的概念扩展到具有多个变量的函数。例如，如果一个函数 f 具有两个参数，当且仅当

f x ⊥ = ⊥

对于所有 x 成立时，该函数在第二个参数上是严格的。但对于多个参数，严格性取决于其他参数给定值的混合形式更为常见。一个例子是条件表达式

cond b x y = if b then x else y

我们可以看到，它在 y 上是严格的，取决于测试 b 是 True 还是 False

cond True  x ⊥ = x
cond False x ⊥ = ⊥

同样，对于 x 也是如此。显然，如果 x 和 y 都是 ⊥，那么 cond 肯定等于 ⊥，但当它们中至少有一个是定义的时，它不一定等于 ⊥。这种行为称为联合严格性。

显然，cond 的行为类似于 if-then-else 语句，在该语句中，不评估 then 和 else 分支至关重要。

if null xs then 'a' else head xs
if n == 0  then  1  else 5 / n

在这里，当条件满足时，else 部分等于 ⊥。因此，在非严格语言中，我们有可能将 if-then-else 等原始控制语句封装到 cond 这样的函数中。这样，我们可以定义自己的控制运算符。在严格语言中，这是不可能的，因为在调用 cond 时，两个分支都会被评估，这使得它相当无用。这让我们瞥见了这样一个普遍观察结果：与严格性相比，非严格性为代码重用提供了更大的灵活性。有关此主题的更多信息，请参见章节 惰性。

代数数据类型

在处理 Integer 之间的偏函数的动机案例后，我们现在想将语义学范围扩展到 Haskell 中的任意代数数据类型。

关于命名法的一句话：特定类型的语义对象集合通常称为域。这个术语更像是一个通用名称，而不是一个特定的定义，我们决定我们的域是 cpos（完全偏序集），即值集合以及满足某些条件的更定义关系，以允许不动点迭代。通常，人们会向 cpos 添加额外的条件，以确保我们的域的值可以在计算机上以某种有限的方式表示，从而避免考虑不可数无限集的扭曲方式。但由于我们不打算证明一般的域理论定理，因此这些条件只是通过构造而偶然成立。

构造函数

让我们以示例类型为例

data Bool    = True | False
data Maybe a = Just a | Nothing

这里，True、False 和 Nothing 是零元构造函数，而 Just 是一个一元构造函数。Bool 的成员形成以下域

记住，⊥ 作为最小元素被添加到 True 和 False 的值集中，我们说该类型是提升的。 ^{偏序图只有一个层次的域称为扁平域。我们已经知道 $Integer$ 也是一个扁平域，只是 ⊥ 上方层次的元素数量是无限的。}

Maybe Bool 可能有哪些成员？它们是

⊥, Nothing, Just ⊥, Just True, Just False

因此，一般规则是将所有可能的值插入一元（二元、三元……）构造函数中，就像往常一样，但不要忘记 ⊥。关于偏序，我们记得构造函数应该像其他任何函数一样单调。因此，偏序如下所示

但有一点值得思考：为什么 Just ⊥ = ⊥ 不成立？我的意思是，“Just 未定义”和“未定义”一样未定义！答案是，这取决于语言是严格的还是非严格的。在严格语言中，所有构造函数默认情况下都是严格的，即 Just ⊥ = ⊥，并且该图将简化为

因此，严格语言的所有域都是扁平的。

但在像 Haskell 这样的非严格语言中，构造函数默认情况下是非严格的，Just ⊥ 是一个与 ⊥ 不同的新元素，因为我们可以编写一个对它们做出不同反应的函数

f (Just _) = 4
f Nothing  = 7

由于 f 忽略了 Just 构造函数的内容，f (Just ⊥) 为 4，但 f ⊥ 为 ⊥（直观地说，如果将 ⊥ 传递给 f，则无法确定是使用 Just 分支还是 Nothing 分支，因此将返回 ⊥）。

这产生了非扁平域，如前图所示。这些有什么用？在图约简的上下文中，我们也可以将 ⊥ 视为一个未评估的表达式。因此，值 x = Just ⊥ 可能会告诉我们，一个计算（例如查找）成功了，并且不是 Nothing，但实际值尚未评估。如果我们只关心 x 是否成功，这实际上可以节省我们不必要的计算工作，以确定 x 是 Just True 还是 Just False，就像在扁平域中那样。非扁平域的全部影响将在章节 惰性 中探讨，但其中一个突出的例子是在递归数据类型和无限列表部分处理的无限列表。

模式匹配

在严格函数部分，我们通过检查不同输入上的结果并坚持单调性，证明了一些函数是严格的。但是，从代数数据类型的角度来看，在现实生活中的 Haskell 中，只有一个严格性的来源：模式匹配，即 case 表达式。一般规则是，对 data 类型构造函数进行模式匹配将强制函数变得严格，即，将 ⊥ 与构造函数进行匹配始终会导致 ⊥。为了说明，考虑

const1 _ = 1

const1' True  = 1
const1' False = 1

第一个函数 const1 是非严格的，而 const1' 是严格的，因为它会确定参数是 True 还是 False，尽管它的结果不依赖于此。函数参数中的模式匹配等效于 case 表达式

const1' x = case x of
   True  -> 1
   False -> 1

同样，它们对 x 强加了严格性：如果 case 表达式的参数表示 ⊥，那么整个 case 也将表示 ⊥。然而，case 表达式的参数可能更复杂，例如

foo k table = case lookup ("Foo." ++ k) table of
  Nothing -> ...
  Just x  -> ...

并且很难追踪这对 foo 的严格性意味着什么。

在等式风格中，多个模式匹配的例子是逻辑 or

or True _ = True
or _ True = True
or _ _    = False

请注意，方程是从上到下匹配的。or 的第一个方程将第一个参数与 True 进行匹配，因此 or 在第一个参数上是严格的。同一个方程还告诉我们 or True x 在 x 上是非严格的。如果第一个参数是 False，那么第二个参数将与 True 进行匹配，并且 or False x 在 x 上是严格的。请注意，虽然通配符通常是非严格性的标志，但这取决于它们相对于构造函数模式匹配的位置。

练习
对逻辑 and 进行类似的讨论 如果我们知道另一个参数，逻辑“异或”（xor）是否可以在一个参数上是非严格的？

还有另一种形式的模式匹配，即不可否认模式，用波浪号 ~ 表示。它们的使用示例如下

f ~(Just x) = 1
f Nothing   = 2

不可否认模式总是会成功（因此得名），导致 f ⊥ = 1。但当将 f 的定义改为

f ~(Just x) = x + 1
f Nothing   = 2      -- this line may as well be left away

我们有

f ⊥       = ⊥ + 1 = ⊥
f (Just 1) = 1 + 1 = 2

如果参数与模式匹配，x 将被绑定到相应的值。否则，任何类似 x 的变量都将被绑定到 ⊥。

默认情况下，let 和 where 绑定也是非严格的

foo key map = let Just x = lookup key map in ...

等效于

foo key map = case (lookup key map) of ~(Just x) -> ...

练习
Haskell 语言定义详细介绍了模式匹配的语义，你现在应该能够理解它了。所以继续看看吧！ 考虑一个有两个 Bool 类型的参数的函数 or，它具有以下性质: or ⊥ ⊥ = ⊥ or True ⊥ = True or ⊥ True = True or False y = y or x False = x 这个函数是联合严格性的另一个例子，但它更尖锐: 只有当两个参数都为 ⊥ 时，结果才为 ⊥ (至少当我们限制参数为 True 和 ⊥ 时)。这样的函数可以在 Haskell 中实现吗？

递归数据类型和无限列表

递归数据结构的情况与基本情况并没有太大区别。考虑一个单元值的列表

data List = [] | () : List

虽然这看起来像一个简单的类型，但实际上，你可以用$\bot$ 填入各种位置，因此对应的图很复杂。这个图的底部显示在下面。省略号表示图在这个方向上继续。一个元素后面的红色椭圆表示这是一个链的末端；该元素处于范式。

等等。但现在，也有无限长的链，比如

⊥ $\sqsubseteq$ ():⊥ $\sqsubseteq$ ():():⊥ $\sqsubseteq$ ...

这给我们带来了一些麻烦，正如我们在收敛部分指出的那样，每个单调序列都必须有一个最小上界。只有当我们允许使用无限列表时，这才是可能的。无限列表 (有时也称为流) 被证明非常有用，它们的多方面用例在延迟计算章节中得到了详细介绍。在这里，我们将展示它们的语义应该是什么以及如何对它们进行推理。请注意，虽然下面的讨论仅限于列表，但它很容易推广到任意递归数据结构，例如树。

在下面，我们将切换回标准的列表类型

data [a] = [] | a : [a]

以缩小与 Haskell 中使用无限列表的实际编程之间的语法差距。

练习
绘制与 [Bool] 对应的非扁平域。 对于 [Integer]，图形如何改变？

用无限列表计算最好用例子来说明。为此，我们需要一个无限列表

ones :: [Integer]
ones = 1 : ones

当将不动点迭代应用于这个递归定义时，我们看到 ones 应该是

⊥ $\sqsubseteq$ 1:⊥ $\sqsubseteq$ 1:1:⊥ $\sqsubseteq$ 1:1:1:⊥ $\sqsubseteq$...,

这是一个由 1 组成的无限列表。让我们尝试理解 take 2 ones 应该是什么。根据 take 的定义

take 0 _      = []
take n (x:xs) = x : take (n-1) xs
take n []     = []

我们可以将 take 应用于 ones 的近似序列的元素

take 2 ⊥       ==>  ⊥
take 2 (1:⊥)   ==>  1 : take 1 ⊥      ==>  1 : ⊥
take 2 (1:1:⊥) ==>  1 : take 1 (1:⊥)  ==>  1 : 1 : take 0 ⊥
               ==>  1 : 1 : []

我们看到 take 2 (1:1:1:⊥) 等等必须与 take 2 (1:1:⊥) = 1:1:[] 相同，因为 1:1:[] 是完全定义的。在输入列表序列和结果输出列表序列上都取上界，我们可以得出结论

take 2 ones = 1:1:[]

因此，取 ones 的前两个元素的行为完全符合预期。

从这个例子推广，我们看到关于无限列表的推理涉及考虑近似序列并传递到上界，即真正的无限列表。不过，我们还没有给它一个坚实的基础。解决方案是将无限列表与整个链本身等同起来，并将其正式地作为新元素添加到我们的域中：无限列表就是其近似序列。当然，任何无限列表，比如 ones，都可以简明地描述为

ones = 1 : 1 : 1 : 1 : ...

这仅仅意味着

ones = (⊥ $\sqsubseteq$ 1:⊥ $\sqsubseteq$ 1:1:⊥ $\sqsubseteq$ ...)

练习
当然，除了 ones 之外，还有更多有趣的无限列表。你能在 Haskell 中写出递归定义吗？ 自然数 nats = 1:2:3:4:... 循环 cycle123 = 1:2:3: 1:2:3 : ... 看看 Prelude 函数 repeat 和 iterate，并尝试借助它们来解决前面的练习。 使用文本中的示例来找到表达式 drop 3 nats 表示的值。 假设在严格环境中工作，即 [Integer] 的域是扁平的。域是什么样的？无限列表呢？ones 表示什么值？

那么计算机如何用无限列表进行计算呢？毕竟这需要无限的时间？好吧，这是真的。但诀窍在于，如果计算机只考虑无限列表的有限部分，它可能在有限的时间内完成。所以，无限列表应该被认为是潜在的无限列表。一般来说，中间结果的形式是无限列表，而最终值是有限的。语义解释的优点之一是可以将中间无限数据结构视为真正无限的，以便在推理程序正确性时可以这样做。

练习
为了演示无限列表作为中间结果的用法，请证明 take 3 (map (+1) nats) = take 3 (tail nats) 首先计算与 map (+1) nats 相对应的无限序列。 当然，我们应该举一个最终结果确实需要无限时间的例子。那么 filter (< 5) nats 表示什么？ 有时，可以在前面的练习中用 takeWhile 代替 filter。为什么只有有时，以及如果这样做会发生什么？

最后要注意的是，递归域的构造可以通过类似于函数递归定义的不动点迭代来完成。然而，必须明确解决无限链的问题。有关形式构造，请参见外部链接中的文献。

Haskell 特性：严格性注释和 Newtypes

Haskell 提供了一种方法来更改数据类型构造函数的默认非严格行为，即通过严格性注释。在像

data Maybe' a = Just' !a | Nothing'

这样的数据声明中，构造函数参数前面的感叹号 ! 指定它应该对这个参数严格。因此，在我们的例子中，我们有 Just' ⊥ = ⊥。更多信息可以在严格性章节中找到。

在某些情况下，人们想要重命名数据类型，例如

data Couldbe a = Couldbe (Maybe a)

但是，Couldbe a 包含 ⊥ 和 Couldbe ⊥ 两个元素。借助 newtype 定义

newtype Couldbe a = Couldbe (Maybe a)

我们可以安排 Couldbe a 在语义上等同于 Maybe a，但在类型检查时不同。特别是，构造函数 Couldbe 是严格的。然而，这个定义与

data Couldbe' a = Couldbe' !(Maybe a)

略有不同。为了解释其中的区别，请考虑函数

f  (Couldbe  m) = 42
f' (Couldbe' m) = 42

这里，f' ⊥ 将导致对构造函数 Couldbe' 的模式匹配失败，导致 f' ⊥ = ⊥。但对于 newtype，对 Couldbe 的匹配永远不会失败，我们会得到 f ⊥ = 42。从某种意义上说，这种差异可以表述为

• 对于严格情况，Couldbe' ⊥ 是 ⊥ 的同义词
• 对于 newtype，⊥ 是 Couldbe ⊥ 的同义词

并约定对 ⊥ 的模式匹配会失败，而对 Constructor ⊥ 的匹配不会失败。

Newtypes 也可用于定义递归类型。一个例子是列表类型 [a] 的备用定义

 newtype List a = In (Maybe (a, List a))

同样，重点是构造函数 In 不会引入额外的提升，带有 ⊥。

以下是一些更多示例，用于区分 newtype 与非严格和严格的 data 声明 (在交互式提示符中)

 Prelude> data D = D Int
 Prelude> data SD = SD !Int
 Prelude> newtype NT = NT Int
 Prelude> (\(D _) -> 42) (D undefined)
 42
 Prelude> (\(SD _) -> 42) (SD undefined)
 *** Exception: Prelude.undefined
 [...]
 Prelude> (\(NT _) -> 42) (NT undefined)
 42
 Prelude> (\(D _) -> 42) undefined
 *** Exception: Prelude.undefined
 [...]
 Prelude> (\(SD _) -> 42) undefined
 *** Exception: Prelude.undefined
 [...]
 Prelude> (\(NT _) -> 42) undefined
 42

其他选定主题

抽象解释和严格性分析

由于惰性求值意味着恒定的计算开销，Haskell 编译器可能希望发现根本不需要固有非严格性的位置，这使其能够在这些特定位置删除开销。为此，编译器执行 **严格性分析**，就像我们在某些函数中证明为严格一样，参见部分 严格函数。当然，严格性细节取决于参数的精确值，例如我们示例中的 cond，不在讨论范围之内（这通常是不可判定的）。但编译器可能会尝试查找近似的严格性信息，这在许多常见情况下都有效，例如 power2。

现在，**抽象解释** 是一个强大的思想，用于推理严格性：...

有关严格性分析的更多信息，请参阅 Haskell wiki 上关于严格性分析的研究论文。

幂集解释

到目前为止，我们已经通过指定其属性抽象地介绍了 ⊥ 和语义近似顺序 $\sqsubseteq$。然而，无论是 ⊥ 还是任何数据类型的成员，例如 Just ⊥，都可以解释为普通集合。这被称为 **幂集构造**。

注意：我不确定这是否真的正确。知道的人请更正。

我对更正的可能更正如下，您对底部的表示不是幂集，它只是一个集合，这导致了我的更正。阅读更多之后，我不得不撤回更正，但我怀疑在第一个示例中 undefined = { {}, {()} }，我不确定它在 Haskell 表示法中是否有任何意义，所以我想称之为 ⊥ 应该是正确的。 原始更正：这是不正确的，考虑 ()，它会导致 undefined = ()，这在 Haskell 中是不正确的。 {()} \ \ ⊥ = {()} 此外 {Just True} {Just False} \ / \ / {Nothing} {Just True, Just False} \ / \ / ⊥ = {Nothing, Just True, Just False} 排除 Just ⊥ 但也许如果我们能说 data powerset Writer a b = Writer a b 并得到 ∀x y.Writer x y / \ / \ ∀x.Writer x ⊥ ∀y.Writer ⊥ y \ / \ / Writer ⊥ ⊥ 其中 undefined = Writer ⊥ ⊥ 是最不确定的成员。

这个想法是将 ⊥ 视为 *所有可能值的集合*，并且计算通过选择子集来检索更多信息。从某种意义上说，值的指代从所有值的集合开始，这些集合将通过计算进行缩减，直到只剩下一个包含单个元素的集合。

举个例子，考虑 Bool，其中域看起来像

{True}  {False}
   \      /
    \    /
   ⊥ = {True, False}

值 True 和 False 被编码为单例集合 {True} 和 {False}，而 ⊥ 是所有可能值的集合。

另一个例子是 Maybe Bool

 {Just True}   {Just False}
         \     /
          \   /
{Nothing} {Just True, Just False}
     \      /
      \    /
 ⊥ = {Nothing, Just True, Just False}

我们看到语义近似顺序等效于集合包含，但参数已切换

$x\sqsubseteq y\iff x\supseteq y$

这种方法可以用于为 Haskell 中的异常提供语义 。

朴素集合不适合递归数据类型

在部分 选择什么作为语义域？ 中，我们认为将简单集合作为类型的指代对于偏函数来说效果不佳。在递归数据类型的背景下，情况变得更糟，正如 John C. Reynolds 在其论文 *多态性不是集合论的* 中所表明的那样。

Reynolds 实际上考虑了递归类型

newtype U = In ((U -> Bool) -> Bool)

将 Bool 解释为集合 {True,False}，并将函数类型 A -> B 解释为从 A 到 B 的函数集合，类型 U 不能表示集合。这是因为 (A -> Bool) 是 A 的子集集合（幂集），由于类似于 Cantor 的论证的对角论证，即存在比自然数更多的实数，它总是比 A 具有更大的基数。因此，(U -> Bool) -> Bool 具有比 U 更大的基数，并且它没有办法与 U 同构。因此，集合 U 不应该存在，这是一个矛盾。

在我们的偏函数世界中，这个论证失败了。在这里，U 的一个元素由从域序列中提取的一系列近似值给出

⊥, (⊥ -> Bool) -> Bool, (((⊥ -> Bool) -> Bool) -> Bool) -> Bool 等等

其中 ⊥ 表示具有单个成员 ⊥ 的域。虽然本文作者坦率地说不知道这样的东西应该意味着什么，但构造函数为 U 给出了一个完全定义良好的对象。我们看到类型 (U -> Bool) -> Bool 仅仅包含移位的近似序列，这意味着它与 U 同构。

最后一点，Reynolds 实际上在二阶多态 lambda 演算中构造了 U 的等效项。在那里，恰好所有项都具有范式，即当我们不包含原始递归运算符 fix :: (a -> a) -> a 时，只存在总函数。因此，对于偏函数和 ⊥，没有真正的需要，然而，朴素的集合论语义失败了。我们只能推测这与并非所有数学函数都是可计算的事实有关。特别是，可计算函数的集合 Nat -> Bool 不应该具有比 Nat 更大的基数。

外部链接

关于语义学的在线书籍

• Schmidt, David A. (1986). 语义学。语言开发的方法论. Allyn and Bacon.