4.3.3.1. 无效果🔗

类型 Empty 没有构造子，因此也没有值，类似于 Scala 或 Kotlin 中的 Nothing 类型。 在 Scala 和 Kotlin 中，Nothing 可以表示永远不返回结果的计算，例如使程序崩溃、抛出异常，或总是陷入无限循环的函数。 类型为 Nothing 的函数或方法参数表示死代码，因为永远不会有合适的参数值。 Lean 不支持无限循环和异常，但 Empty 仍然有用，它向类型系统表明某个函数不可能被调用。 当 E 是一个其类型没有构造子的表达式时，使用语法 nomatch E 会向 Lean 表明当前表达式不必返回结果，因为它本不可能被调用。

使用 Empty 作为 Prim 的参数表明，除了 Prim.plus、Prim.minus 和 Prim.times 之外没有额外情形，因为不可能构造出类型为 Empty 的值来放入 Prim.other 构造子中。 由于一个把类型为 Empty 的算子应用到两个整数上的函数永远不可能被调用，它不需要返回结果。 因此，它可以用于任意单子中：

这可以与 Id（恒等单子）一起使用，以求值完全没有任何效应的表达式：

-9

4.3.3.2. 非确定性搜索🔗

在遇到除以零时，与其只是失败，回溯并尝试不同的输入也是合理的。 给定合适的单子，同一个 evaluateM 就可以对不导致失败的一组答案执行非确定性搜索。 除法之外，这还需要某种指定结果选择的手段。 做到这一点的一种方式，是向表达式语言中添加一个函数 choose，它指示求值器在搜索不会失败的结果时，选择它的任一参数。

求值器的结果现在是一个值的多重集，而不是单个值。 求值为多重集的规则如下：

• 常量 n 求值为单元素集合 \{n\}。

• 除除法以外的算术算子会在算子笛卡尔积中的每一对上被调用，因此 X + Y 求值为 \{ x + y \mid x ∈ X, y ∈ Y \}。

• 除法 X / Y 求值为 \{ x / y \mid x ∈ X, y ∈ Y, y ≠ 0\}。换言之，Y 中所有 0 值都会被舍去。

• 选择 \mathrm{choose}(x, y) 求值为 \{ x, y \}。

例如，1 + \mathrm{choose}(2, 5) 求值为 \{ 3, 6 \}，1 + 2 / 0 求值为 \{\}，而 90 / (\mathrm{choose}(-5, 5) + 5) 求值为 \{ 9 \}。 使用多重集而不是真正的集合，可以避免检查元素唯一性，从而简化代码。

一个 Monad Many 实例需要一个 bind 运算符。 在非确定性搜索中，将两个操作顺序组合起来，就是取第一步中的所有可能性，并在每一种可能性上运行程序的其余部分，然后取结果的并集。 换言之，如果第一步返回三个可能答案，那么第二步就需要对这三个答案全部尝试。 由于第二步可以为每个输入返回任意数量的答案，取它们的并集就表示整个搜索空间。

Many.one 和 Many.bind 遵守单子约定。 要检查 Many.bind (Many.one v) f 与 f v 相同，首先尽可能对表达式求值：

空多重集是 union 的右单位元，因此答案等价于 f v。 要检查 Many.bind v Many.one 与 v 相同，考虑 Many.bind 会对 v 的每个元素应用 Many.one，并取其并集。 换言之，如果 v 具有形式 {v₁, v₂, v₃, …, vₙ}，那么 Many.bind v Many.one 就是 {v₁} ∪ {v₂} ∪ {v₃} ∪ … ∪ {vₙ}，也就是 {v₁, v₂, v₃, …, vₙ}。

最后，为了检查 Many.bind 是结合的，需要检查 Many.bind (Many.bind v f) g 与 Many.bind v (fun x => Many.bind (f x) g) 相同。 如果 v 具有形式 {v₁, v₂, v₃, …, vₙ}，则：

这意味着

类似地，

因此，两边相等，所以 Many.bind 是结合的。

所得的单子实例为：

使用这个单子进行的一个示例搜索会找出列表中所有和为 15 的数字组合：

搜索过程在列表上递归进行。 当目标为 0 时，空列表是一次成功的搜索；否则，它失败。 当列表非空时，有两种可能：要么列表的头部大于目标，在这种情况下它不可能参与任何成功的搜索；要么不是这样，在这种情况下它可以参与。 如果列表的头部不是候选项，则搜索继续处理列表的尾部。 如果头部是候选项，则有两种可能需要与 Many.union 组合：找到的解要么包含该头部，要么不包含。 不包含该头部的解通过对尾部进行递归调用得到；而包含该头部的解则通过从目标中减去该头部，然后将该头部附加到递归调用所得的解上得到。

辅助函数 printList 确保每行显示一个结果：

[7, 8]
[6, 9]
[5, 10]
[4, 5, 6]
[3, 5, 7]
[3, 4, 8]
[2, 6, 7]
[2, 5, 8]
[2, 4, 9]
[2, 3, 10]
[2, 3, 4, 6]
[1, 6, 8]
[1, 5, 9]
[1, 4, 10]
[1, 3, 5, 6]
[1, 3, 4, 7]
[1, 2, 5, 7]
[1, 2, 4, 8]
[1, 2, 3, 9]
[1, 2, 3, 4, 5]

[3, 6]

[]

[9]

4.3.3.3. 自定义环境🔗

通过允许字符串作为算子使用，并提供从字符串到实现这些算子的函数的映射，可以使求值器能够由用户扩展。 例如，用户可以用一个取余算子，或一个返回其两个参数最大值的算子来扩展求值器。 从函数名到函数实现的映射称为一个环境。

环境需要在每次递归调用中传递。 起初，可能看起来 evaluateM 需要一个额外参数来保存环境，并且该参数应当传递给每次递归调用。 然而，像这样传递参数是单子的另一种形式，因此适当的 Monad 实例允许求值器保持不变地使用。

将函数用作单子通常称为 reader 单子。 在 reader 单子中求值表达式时，使用如下规则：

• 常量 n 求值为常量函数 λ e . n，

• 算术运算符求值为会传递其参数的函数，因此 f + g 求值为 λ e . f(e) + g(e)，并且

• 自定义运算符求值为将该自定义运算符应用于参数所得的结果，因此 f \ \mathrm{OP}\ g 求值为 λ e . \begin{cases} h(f(e), g(e)) & \mathrm{if}\ e\ \mathrm{contains}\ (\mathrm{OP}, h) \\ 0 & \mathrm{otherwise} \end{cases} 其中 0 作为应用未知算子时的后备值。

另一方面，bind 要稍微棘手一些。 它的类型是 Reader ρ α → (α → Reader ρ β) → Reader ρ β。 展开 Reader 的定义可以使这个类型更容易理解，展开后得到 (ρ → α) → (α → ρ → β) → (ρ → β)。 它应当以一个接受环境的函数作为第一个参数，而第二个参数应当将这个接受环境的函数的结果转换为另一个接受环境的函数。 将二者组合得到的结果本身也是一个函数，正在等待一个环境。

可以交互式地使用 Lean 来获得编写此函数的帮助。 第一步是写下参数和返回类型，并尽可能显式，以便获得尽可能多的帮助，同时用一个下划线作为定义的主体：

Lean 会提供一条消息，描述当前作用域中有哪些变量可用，以及结果所期望的类型。 ⊢ 符号由于形似地铁入口而称为 turnstile，它将局部变量与目标类型分隔开来；在这条消息中，目标类型是 ρ → β：

don't know how to synthesize placeholder
context:
ρ α β:Typeresult:ρ → αnext:α → ρ → β⊢ ρ → β

由于返回类型是一个函数，一个好的第一步是在下划线外包上一层 fun：

所得消息现在将该函数的实参显示为局部变量：

don't know how to synthesize placeholder
context:
ρ α β:Typeresult:ρ → αnext:α → ρ → βenv:ρ⊢ β

上下文中唯一能够产生 β 的东西是 next，而它需要两个参数才能做到这一点。 每个参数本身都可以是一个下划线：

这两个下划线分别关联着以下消息：

don't know how to synthesize placeholder
context:
ρ α β:Typeresult:ρ → αnext:α → ρ → βenv:ρ⊢ α

don't know how to synthesize placeholder
context:
ρ α β:Typeresult:ρ → αnext:α → ρ → βenv:ρ⊢ ρ

don't know how to synthesize placeholder
context:
ρ α β:Typeresult:ρ → αnext:α → ρ → βenv:ρ⊢ ρ

最终版本可以通过撤销 Reader 的展开并清理显式细节而得到：

并非总是能够仅仅通过“跟随类型”来写出正确的函数，而且这样做还带有不理解所得程序的风险。 然而，理解一个已经写出的程序，也可能比理解一个尚未写出的程序更容易；而填写下划线的过程也可能带来洞见。 在这个例子中，Reader.bind 对于 Id 的作用正如 bind 一样，只是它接受一个额外的参数，然后将该参数向下传递给它的各个参数；这种直觉有助于理解它的工作方式。

Reader.pure（它生成常量函数）和 Reader.bind 满足单子契约。 要检查 Reader.bind (Reader.pure v) f 与 f v 相同，只需不断替换定义，直到最后一步：

对于每个函数 f，fun x => f x 与 f 相同，因此约定的第一部分得到满足。 要检查 Reader.bind r Reader.pure 与 r 相同，可以使用类似的技巧：

因为 reader 动作 r 本身就是函数，这与 r 相同。 要检查结合律，可以对 Reader.bind (Reader.bind r f) g 和 Reader.bind r (fun x => Reader.bind (f x) g) 都做同样的事情：

Reader.bind r (fun x => Reader.bind (f x) g) 化简为相同的表达式：

因此，一个 Monad (Reader ρ) 实例是有根据的：

将传递给表达式求值器的自定义环境可以表示为由对组成的列表：

例如，exampleEnv 包含最大值函数和取模函数：

Lean 已经有一个函数 List.lookup，可在由成对元素组成的列表中查找与某个键关联的值，因此 applyPrimReader 只需检查自定义函数是否存在于环境中。如果该函数未知，它返回 0：

将 evaluateM 与 applyPrimReader 和一个表达式一起使用，会得到一个期望环境的函数。 幸运的是，exampleEnv 是可用的：

9

与 Many 类似，Reader 是一种在大多数语言中难以编码的效应示例，但类型类和单子使它与任何其他效应一样方便。 Common Lisp、Clojure 和 Emacs Lisp 中的动态变量或特殊变量可以像 Reader 一样使用。 类似地，Scheme 和 Racket 的参数对象是一种与 Reader 精确对应的效应。 Kotlin 中上下文对象的惯用法可以解决类似的问题，但它们本质上是一种自动传递函数参数的手段，因此这种惯用法更像是读者单子的编码，而不是语言中的一种效应。

4.3.3.4. 练习🔗

{ log := [(Prim.plus, 1, 2), (Prim.minus, 3, 4), (Prim.times, 3, -1)], val := -3 }