Haskell/Denotational 语义

介绍

本章解释了如何将 Haskell 程序的含义形式化，即Denotational 语义。从形式上指定程序 square x = x*x 与将每个数字映射到其平方的数学平方函数相同，这似乎是吹毛求疵，但像 f x = f (x+1) 这样无限循环的程序的含义呢？在以下内容中，我们将举例说明 Scott 和 Strachey 最初提出的方法，并获得一个基础，可以用来推理功能程序的正确性，尤其是递归定义的正确性。当然，我们将专注于理解 Haskell 程序所需的那些主题。^[1]

本章的另一个目的是说明严格和惰性的概念，这些概念反映了函数是否需要或不需要计算其参数。这是预测 Haskell 程序评估过程的基本要素，因此对程序员至关重要。有趣的是，这些概念可以用 Denotational 语义单独简洁地表达，不需要参考执行模型。它们将在 图约简 中得到很好的利用，但本章将使读者熟悉 Denotational 定义和涉及的概念，如 ⊥（“底部”）。只对严格性感兴趣的读者可能希望浏览 底部和偏函数 部分，并快速前往 严格和非严格语义 部分。

什么是 Denotational 语义，它有什么用？

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

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

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

denotations 是组合的，即程序 1+9 的含义只取决于其组成部分的含义

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

同样的符号也用于类型，即

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

为了简化，在后续章节中我们将默默地将表达式与其语义对象识别起来，并且只在需要澄清时使用这种符号。

Haskell 等纯粹函数式语言的关键特性之一是，像“1+9 表示 10”这样的直接数学解释也适用于函数：本质上，类型为 Integer -> Integer 的程序的语义是一个数学函数$\mathbb {Z} \to \mathbb {Z}$，在整数之间。虽然我们将看到这个表达式通常需要细化，以包括非终止，但对于命令式语言来说情况明显更糟：具有该类型的过程表示会以可能意想不到的方式改变机器状态的东西。命令式语言与操作语义紧密相连，操作语义描述了它们在机器上的执行方式。可以为命令式程序定义一个语义解释，并使用它来推理这些程序，但语义通常具有操作性质，有时必须扩展与函数式语言的语义解释相比。 相反，纯粹函数式语言的含义默认情况下完全独立于它们的执行方式。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，而右手边的$\bot$ 的类型是 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$。

练习
整数在顺序 $\leq$ 方面是否形成偏序集？

我们可以通过以下图形描述类型 Integer 的值上的顺序 $\sqsubseteq$

其中，两个节点之间的每条连接都指定了上方的节点比下方的节点更精确。因为只有一个层次（不包括 $\bot$），因此可以说 Integer 是一个扁平域。此图还解释了 $\bot$ 的名称：它被称为底部，因为它的位置始终在最底部。

单调性

我们对偏函数的直觉现在可以表述为：每个偏函数 $f$ 都是偏序集之间的单调映射。更精确的自变量将产生更精确的值

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

特别是，一个具有 $h(\bot )=1$ 的单调函数 $h$ 是常数：对于所有 $n$，$h(n)=1$。请注意，这里至关重要的是 $1\sqsubseteq 2$ 等关系不成立。

翻译成 Haskell，单调性意味着我们不能使用 $\bot$ 作为条件，即我们不能对 $\bot$ 或其等效项 undefined 进行模式匹配。否则，上述示例 $g$ 可以用 Haskell 程序表示。正如我们将在后面看到，$\bot$ 还表示非终止程序，因此无法在 Haskell 中观察到 $\bot$ 与停机问题有关。

当然，更精确的概念可以通过说一个函数在所有可能的自变量上都比另一个函数更精确，从而扩展到偏函数。

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

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

递归定义作为不动点迭代

阶乘函数的近似值

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

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

虽然我们看到直接将这个递归函数解释为集合描述可能会导致问题，但我们直觉地知道，为了计算对于每个给定的 $n$ 的 $f(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 是否真的对所有参数都是未定义的。

收敛

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

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

如果对于语义近似顺序情况也是如此，我们可以明确地确定近似阶乘函数的单调函数序列确实有一个极限。对于我们的指称语义，我们将只遇到具有最小元素 $\bot$ 的 dcpo，它们被称为 **完备偏序集** (**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 也应该不会停止。^[3] 它表明，人们可以自由选择这种或另一种函数式编程语言的设计。人们称语言为严格或非严格，具体取决于函数默认情况下是严格还是非严格。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 也是如此。显然，cond 如果 x 和 y 都是 ⊥，则肯定为 ⊥，但如果它们中至少有一个是定义的，则不一定为 ⊥。这种行为称为联合严格性。

显然，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 时会评估两个分支，这使得它几乎没有用。这让我们了解了非严格性比严格性为代码重用提供更多灵活性的普遍观察结果。有关此主题的更多信息，请参阅惰性 ^[4] 一章。

代数数据类型

在处理了 Integer 之间的偏函数的动机情况之后，我们现在希望将语义语义的范围扩展到 Haskell 中的任意代数数据类型。

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

构造函数

让我们以示例类型为例

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

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

请记住，⊥ 作为最小元素添加到值 True 和 False 的集合中，我们说该类型是提升 ^[5] 的。其偏序图只包含一个级别的域称为扁平域。我们已经知道 $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 中是严格的。请注意，虽然通配符是 non-strictness 的一个普遍标志，但这取决于它们相对于构造函数模式匹配的位置。

练习
对逻辑 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 语言定义 中，详细介绍了 模式匹配的语义，现在你应该能够理解它。所以继续看看吧！ 考虑一个带有两个 Boolean 参数的函数 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 表示什么？ 在前面的练习中，有时可以将 filter 替换为 takeWhile。为什么只有有时可以，如果这样做会发生什么？

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

Haskell 特性：严格性注释和新类型

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 ⊥ 的匹配不会失败。

Newtype 也可用于定义递归类型。例如，列表类型 [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 实际上在二阶多态 λ 演算中构造了 U 的等价物。在那里，所有项都具有范式，即当我们不包含原始递归运算符 fix :: (a -> a) -> a 时，只存在总函数。因此，实际上不需要偏函数和 ⊥，但朴素的集合论语义失败了。我们只能推测这与并非所有数学函数都是可计算的这一事实有关。特别是，可计算函数的集合 Nat -> Bool 的基数不应该大于 Nat。

外部链接

关于语义学的在线书籍

• Schmidt, David A. (1986). 语义学。一种语言开发方法. Allyn 和 Bacon。