7.3.2.1. 递归与宇宙再探🔗

将行方便地组织为元组是有代价的：Row 分别处理其两个基本情形这一事实意味着，在类型中使用 Row 且通过对码（也就是模式）递归来定义的函数，也需要作出相同区分。 一个会受此影响的例子是相等性检查，它通过对模式递归来定义一个检查行是否相等的函数。 此例不能通过 Lean 的类型检查器：

Type mismatch
  (v1, r1')
has type
  ?m.10 × ?m.11
but is expected to have type
  Row (col :: cols)

问题在于模式 col :: cols 没有充分细化这些行的类型。 这是因为 Lean 此时尚无法判断匹配到的是 Row 定义中的单元素模式 [col]，还是 col1 :: col2 :: cols 模式，因此对 Row 的调用不会计算归约到有序对类型。 解决方案是在 Row.bEq 的定义中镜像 Row 的结构：

不同于其他语境，出现在类型中的函数不能仅按其输入/输出行为来理解。 使用这些类型的程序会发现自己被迫镜像类型层面函数所使用的算法，使其结构与该类型的模式匹配和递归行为相一致。 使用依值类型编程的一项重要技能，就是选择具有恰当计算行为的适当类型层面函数。

7.3.2.2. 列指针🔗

有些查询只有在某个模式包含特定列时才有意义。 例如，返回海拔高于 1000 米的山峰的查询，只有在具有一个包含整数的 "elevation" 列的模式语境中才有意义。 表明某列包含在某个模式中的一种方式，是直接提供指向它的指针；而将该指针定义为带索引的族，则可以排除无效指针。

一列可以通过两种方式出现在模式中：要么它位于模式的开头，要么它位于模式中较后的某处。 最终，如果一列位于某个模式中较后的地方，那么它将成为该模式某个尾部的开头。

带索引的族 HasCol 是将该规约翻译为 Lean 代码的结果：

该族的三个参数分别是模式、列名以及列的类型。 这三者都是指标，但若将参数重新排序，把模式放在列名和类型之后，就可以使名称和类型成为参数。 当模式以列 ⟨name, t⟩ 开头时，可以使用构造子 here；因此，它是指向模式中第一列的指针，并且只能在第一列具有所需名称和类型时使用。 构造子 there 将指向较小模式的指针转换为指向在其上多了一列的模式的指针。

因为 "elevation" 是 peak 中的第三列，所以可以用 there 跳过前两列来找到它，此后它就是第一列。 换言之，要满足类型 HasCol peak "elevation" .int，可使用表达式 .there (.there .here)。 理解 HasCol 的一种方式是将其看作某种带有装饰的 Nat：zero 对应于 here，而 succ 对应于 there。 额外的类型信息使得出现差一错误成为不可能。

指向模式中特定列的指针可用于从行中提取该列的值：

第一步是对模式进行模式匹配，因为这决定了行是元组还是单个值。 不需要为空模式提供情形，因为有一个 HasCol 可用，并且 HasCol 的两个构造子都指定了非空模式。 如果模式只有一列，那么指针必须指向它，因此只需匹配 HasCol 的 here 构造子。 如果模式有两列或更多列，那么必须有一个对应 here 的情形，此时值就是行中的第一个值；还要有一个对应 there 的情形，此时使用递归调用。 因为 HasCol 类型保证该列存在于行中，所以 Row.get 不需要返回 Option。

HasCol 扮演两个角色：

1. 它充当某个具有特定名称和类型的列存在于模式中的证据。

2. 它充当可用于在行中找到与该列关联的值的数据。

第一个角色，即证据的角色，类似于命题的使用方式。 指标族 HasCol 的定义可以被解读为：什么算作给定列存在的证据这一规范。 然而，与命题不同，使用了 HasCol 的哪一个构造子是重要的。 在第二个角色中，构造子像 Nat 一样用于在集合中查找数据。 使用指标族编程通常要求能够熟练地在这两种视角之间切换。

7.3.2.3. 子模式🔗

关系代数中的一个重要操作是将表或行投影到一个较小的模式。 所有不存在于较小模式中的列都会被遗忘。 为了使投影有意义，较小的模式必须是较大模式的子模式，这意味着较小模式中的每一列都必须存在于较大模式中。 正如 HasCol 使得可以在行中编写不会失败的单列查找一样，将子模式关系表示为指标族，也使得可以编写不会失败的投影函数。

一个模式作为另一个模式的子模式的各种方式，可以定义为一个指标族。 基本思想是：若较小模式中的每一列都出现在较大模式中，则较小模式就是较大模式的子模式。 如果较小模式为空，那么它当然是较大模式的子模式，这由构造子 nil 表示。 如果较小模式有一列，那么该列必须在较大模式中，并且该子模式中的所有其余列也必须构成较大模式的子模式。 这由构造子 cons 表示。

换言之，Subschema 为较小模式的每一列分配一个 HasCol，该 HasCol 指向它在较大模式中的位置。

模式 travelDiary 表示 peak 和 waterfall 共有的字段：

它当然是 peak 的子模式，如下例所示：

然而，像这样的代码难以阅读，也难以维护。 一种改进方式是指示 Lean 自动写出 Subschema 和 HasCol 构造子。 这可以使用在 关于命题与证明的插曲中介绍的策略功能来完成。 该插曲使用 by decide 和 by simp 为各种命题提供证据。

在此语境中，有两个策略是有用的：

• constructor 策略指示 Lean 使用某个数据类型的构造子来解决问题。

• repeat 策略指示 Lean 反复重复某个策略，直到该策略失败或证明完成为止。

在下一个例子中，by constructor 的效果与直接写 .nil 相同：

然而，对一个稍微复杂一些的类型尝试同样的策略会失败：

unsolved goals
a⊢ HasCol peak "location" DBType.string

a⊢ Subschema [] peak

以 unsolved goals 开头的错误描述的是未能完全构造出其本应构造的表达式的策略。 在 Lean 的策略语言中，目标是一个类型，策略要在幕后构造适当的表达式来满足它。 在此情形中，constructor 导致 Subschema.cons 被应用，而这两个目标表示 cons 所期望的两个参数。 再添加一个 constructor 实例会使第一个目标（HasCol peak "location" DBType.string）由 HasCol.there 来处理，因为 peak 的第一列不是 "location"：

unsolved goals
a.a⊢ HasCol
  [{ name := "location", contains := DBType.string }, { name := "elevation", contains := DBType.int },
    { name := "lastVisited", contains := DBType.int }]
  "location" DBType.string

a⊢ Subschema [] peak

然而，添加第三个 constructor 会使第一个目标得到解决，因为 HasCol.here 是适用的：

unsolved goals
a⊢ Subschema [] peak

第四个 constructor 实例解决了 Subschema peak [] 目标：

事实上，不使用策略写出的版本有四个构造子：

与其通过试验来找出应该写多少次 constructor，不如使用 repeat 策略来要求 Lean 只要 constructor 持续取得进展就不断尝试它：

这个更灵活的版本也适用于更有意思的 Subschema 问题：

盲目尝试构造子直到某个构造子奏效的方法，对于 Nat 或 List Bool 这样的类型并不十分有用。 毕竟，一个表达式具有类型 Nat 并不意味着它就是正确的 Nat。 但是像 HasCol 和 Subschema 这样的类型受到其指标的充分约束，以至于永远只有一个构造子适用；这意味着程序本身的内容不那么有意思，而计算机可以选出正确的那个。

如果一个模式是另一个模式的子模式，那么它也是在该较大模式上扩展一个额外列之后所得模式的子模式。 这一事实可以用函数定义来刻画。 Subschema.addColumn 接受 smaller 是 bigger 的子模式这一证据，然后返回 smaller 是 c :: bigger 的子模式这一证据，也就是说，返回 bigger 加上一个额外列后的证据：

子模式描述了在较大模式中何处找到较小模式中的每一列。 Subschema.addColumn 必须将这些描述从原来的较大模式转换到扩展后的较大模式。 在 nil 情形中，较小模式是 []，而 nil 也是 [] 是 c :: bigger 的子模式的证据。 在 cons 情形中，它描述了如何把 smaller 中的一列放入 bigger；该列的位置需要用 there 调整，以考虑新增列 c，并且递归调用会调整其余列。

理解 Subschema 的另一种方式是：它定义了两个模式之间的一个关系——存在类型为 Subschema smaller bigger 的表达式，意味着 (smaller, bigger) 处于该关系中。 该关系是自反的，意思是每个模式都是其自身的子模式：

7.3.2.4. 投影行🔗

给定 s' 是 s 的子模式这一证据，s 中的一行可以被投影为 s' 中的一行。 这是通过使用 s' 是 s 的子模式这一证据完成的，该证据说明了 s' 的每一列在 s 中何处找到。 s' 中的新行通过从旧行中的适当位置取回值，逐列构造出来。

执行此投影的函数 Row.project 有三个情形，对应于 Row 本身的每个情形。 它将 Row.get 与 Subschema 参数中的每个 HasCol 一起使用，以构造投影后的行：

7.3.5.1. 笛卡儿积🔗

取两张表的笛卡儿积，是通过将第一张表中的每一行追加到第二张表中的每一行来完成的。 首先，由于 Row 的结构，向一行添加单列需要对其模式进行模式匹配，以确定结果将是一个裸值还是一个元组。 因为这是常见操作，将该模式匹配分解到一个辅助函数中会很方便：

追加两行同时按第一个模式和第一行的结构递归，因为行的结构与模式的结构同步推进。 当第一行为空时，追加返回第二行。 当第一行是单元素行时，将该值添加到第二行。 当第一行包含多列时，将第一列的值添加到对该行其余部分递归所得的结果中。

标准库中的 List.flatMap 会把一个自身返回列表的函数应用于输入列表中的每个条目，并返回按顺序追加所得列表后的结果：

其类型签名表明 List.flatMap 可用于实现一个 Monad List 实例。 事实上，List.flatMap 与 pure x := [x] 一起确实实现了一个单子。 然而，它并不是一个很有用的 Monad 实例。 List 单子基本上是 Many 的一个版本，它会在用户有机会请求某个数量的值之前，预先探索搜索空间中的每一条可能路径。 由于这个性能陷阱，通常不宜为 List 定义 Monad 实例。 然而在这里，查询语言没有用于限制返回结果数量的运算符，因此组合所有可能性正是所期望的行为：

正如 List.product 一样，身份单子中带有可变状态的循环也可用作另一种实现技术：

7.3.5.2. 差集🔗

从表中移除不需要的行可以使用 List.filter 完成，它接受一个列表和一个返回 Bool 的函数。 返回的新列表只包含使该函数返回 true 的条目。 例如，

求值得到

因为 "Columbia" 和 "Sandy" 的长度小于或等于 8。 可以使用辅助函数 List.without 来移除表中的条目：

在解释查询时，这将与 Row 的 BEq 实例一起使用。

7.3.5.3. 重命名列🔗

重命名一行中的列，是用一个递归函数遍历该行，直到找到所讨论的列；此时，具有新名称的列获得与具有旧名称的列相同的值：

虽然此函数改变了其参数的类型，但实际返回值所包含的数据与原参数完全相同。 从运行时角度看，Row.rename 不过是一个缓慢的恒等函数。 使用索引族编程的一个困难在于，当性能很重要时，这类操作可能会造成妨碍。 要消除这些“重新索引”函数，需要非常谨慎且常常较为脆弱的设计。

7.3.5.4. 给列名加前缀🔗

给列名添加前缀与重命名列非常相似。 不同的是，prefixRow 不能前进到某个目标列后就返回，而必须处理所有列：

这可以与 List.map 一起使用，以便给表中的所有行添加前缀。 同样，此函数的存在只是为了改变一个值的类型。

7.3.5.5. 组合各个部分🔗

定义完所有这些辅助函数后，执行查询只需要一个简短的递归函数：

构造子的某些参数在执行期间不会使用。 特别是，构造子 project 和函数 Row.project 都将较小的模式作为显式参数，但该模式是较大模式的子模式这一证据的类型包含了足够信息，使 Lean 能够自动填充该参数。 类似地，product 构造子所要求的两张表具有互不相交的列名这一事实，对于 Table.cartesianProduct 并不需要。 一般而言，依值类型提供了许多机会，使 Lean 能够代表程序员填充参数。

对查询结果使用点记法，可以调用在 Table 和 List 命名空间中定义的函数，例如 List.map、List.filter 和 Table.cartesianProduct。 这之所以可行，是因为 Table 是使用 abbrev 定义的。 就像类型类搜索一样，点记法可以穿透由 abbrev 创建的定义。

select 的实现也相当简洁。 执行查询 q 后，使用 List.filter 移除不满足该表达式的行。 List.filter 期望一个从 Row s 到 Bool 的函数，但 DBExpr.evaluate 的类型是 Row s → DBExpr s t → t.asType。 由于 select 构造子的类型要求该表达式具有类型 DBExpr s .bool，在此上下文中 t.asType 实际上就是 Bool。

一个查找所有海拔超过 500 米的山峰高度的查询可以写为：

执行它会返回预期的整数列表：

[3637, 1519, 2549]

为了规划观光游览，将同一地点的所有山峰和瀑布配对可能是有意义的。 这可以通过取两张表的笛卡儿积、只选择其中位置相等的行，然后投影出名称来完成：

由于示例数据只包含美国的瀑布，执行该查询会返回美国境内的山峰和瀑布配对：

[("Mount Nebo", "Multnomah Falls"), ("Mount Nebo", "Shoshone Falls"), ("Moscow Mountain", "Multnomah Falls"),
  ("Moscow Mountain", "Shoshone Falls"), ("Mount St. Helens", "Multnomah Falls"),
  ("Mount St. Helens", "Shoshone Falls")]

7.3.5.6. 你可能遇到的错误🔗

许多潜在错误都被 Query 的定义排除了。 例如，若忘记 "mountain.location" 中添加的限定符，会产生一个编译时错误，并高亮显示列引用 c! "location"：