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 跳过前两列然后使用 here 找到它。 换句话说，要满足类型 HasCol peak "elevation" .int，使用表达式 .there (.there .here)。 HasCol 也可以理解为是一种带有修饰的 Nat——zero 对应于 here，succ 对应于 there。 额外的类型信息使得不可能出现列序号偏差了一位之类的错误。

指向数据库模式中的列的指针可以用来从行中提取该列的值：

第一步是对数据库模式进行模式匹配，因为这决定了行是元组还是单个值。 空模式的情形不需要考虑，因为 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 的策略语言中，证明目标（goal） 是策略需要通过构造适当的表达式来实现的类型。 在这种情形下，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 实例。 实际上，与 pure x := [x] 一起，List.flatMap 确实实现了一个单子。 然而，它不是一个非常有用的 Monad 实例。 List 单子基本上是 Many 的一个版本，它在用户有机会请求一定数量的值之前，预先探索搜索空间中的 每条 可能路径。 由于这种性能陷阱，为 List 定义 Monad 实例通常不是一个好主意。 然而，在这里，查询语言没有用于限制返回结果数量的运算符，因此组合所有可能性正是我们想要的：

就像 List.product 一样，恒等单子（Identity Monad）中带有可变状态的循环可以用作替代实现技术：

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"：