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 \}。 使用多重集合而非集合，是为了避免处理元素重复的情况而使代码过于复杂。

表示这种非确定性作用的单子必须能够处理没有答案的情况，以及至少有一个答案和其他答案的情况：

该数据类型看起来非常像 List。 不同之处在于，List.cons 存储列表的其余部分，而 more 存储一个函数，该函数应计算剩余的值。 这意味着 Many 的使用者可以在找到一定数量的结果后停止搜索。

单个结果由 more 构造子表示，该构造子不返回任何进一步的结果：

两个作为结果的多重集合的并集，可以通过检查第一个是否为空来计算。 如果第一个为空则第二个多重集合就是并集。 如果非空，则并集由第一个多重集合的第一个元素，紧跟着其余部分与第二个多重集的并集：

对值列表搜索会比手动构造多重集合更方便。 Many.fromList 将列表转换为结果的多重集合：

类似地，一旦搜索已经确定，就可以方便地提取固定数量的值或所有值：

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 取 Many.one 应用于 v 的每个元素的并集。 换句话说，如果 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ₙ}，则：

which means that

Similarly,

因此两边相等，所以 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]

让我们回到产生多重集合的算术求值器，choose 运算符可以用来非确定性地选择一个值，除以零会使之前的选择失效：

可以用这些运算符对前面的示例求值：

[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 用于运算符未知的情况。

要在Lean中定义reader单子，第一步是定义 Reader 类型，和用户获取环境的作用：

按照惯例，希腊字母 ρ（发音为“rho”）用于表示环境。

算术表达式中的常量映射为常量函数这一事实表明，Reader 的 pure 的适当定义是一个常量函数：

另一方面，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:ρ⊢ ρ

先处理第一条下划线，注意到上下文中只有一个东西可以产生 α，即 result：

现在两条下划线都有一样的报错了：

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

值得高兴的是，两条下划线都可以被 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 actions 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的上下文对象可以解决类似的问题，但根本上是一种自动传递函数参数的方式，因此更像是作为reader单子的编码，而不是语言中实现的作用。

4.3.3.4. 练习🔗

练习

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