diff --git a/functional-programming-lean/src/dependent-types.md b/functional-programming-lean/src/dependent-types.md index b5e0550..0390765 100644 --- a/functional-programming-lean/src/dependent-types.md +++ b/functional-programming-lean/src/dependent-types.md @@ -1,35 +1,79 @@ + +# 使用依值类型编程 + + + +在大多数静态类型编程语言中,类型世界和程序世界之间有一个明确的界限。 类型和程序有不同的语法,并且它们在不同阶段起作用。 + 类型通常在编译阶段被使用,以检查程序是否遵守某些不变量。 程序在运行时阶段被使用,以实际执行计算。 + 当两者互动时,通常是以类型案例运算符的形式,例如`instance-of`检查或提供类型检查器无法获得的信息的转换运算符,以在运行时验证。 + 换句话说,这种交互一般是将类型插入程序世界,使得类型具有一些有限的运行时含义。 + -_Dependent types_ are types that contain non-type expressions. +Lean 并不严格地区分类型和程序。 +在 Lean 中,程序可以计算类型,类型可以包含程序。 +允许程序出现在类型中使得编译阶段可以使用编程语言全部的计算能力。 +允许函数返回类型则使得类型成为编程过程中的一等参与者。 + + + +**依值类型(Dependent types)** 是包含非类型表达式的类型。 + ```lean {{#example_decl Examples/DependentTypes.lean natOrStringThree}} ``` + + +更多依值类型的例子包括: + * [多态的介绍性段落](getting-to-know/polymorphism.md) 中的 `posOrNegThree`,其中函数的返回类型取决于参数的值。 + * [`OfNat` 类型类](type-classes/pos.md#literal-numbers) 中取决于具体的自然数字面量。 + * [`CheckedInput` 结构](functor-applicative-monad/applicative.md#validated-input) 中依赖于验证发生年份的验证器的例子。 + * [子类型](functor-applicative-monad/applicative.md#subtypes) 中包含引用特定值的命题。 + * 几乎所有有趣的命题都是包含值的类型,因此是依值类型,包括判断 [数组索引表示](props-proofs-indexing.md) 的有效性的命题,。 + +依值类型大大增加了类型系统的能力。 +根据参数的值的不同返回不同类型的灵活性使得其他类型系统中很难给出类型的程序可以被接受。 +同时,依值类型使得类型签名可以表达“函数只能返回特定的值”等概念,使得编译阶段可以检查一些更加严格的不变量。 + + + +然而,使用依值类型进行编程是一个非常复杂的问题,需要一些一般函数式编程中不会用到的技能。 +依值类型编程中很可能出现“设计了一个复杂类型以表达一个非常细致的规范,但是无法写出满足这个类型的程序”之类的问题。 +当然,这些问题也经常会引发对问题的新的理解,从而得到一个更加细化且可以被满足的类型。 +虽然本章只是简单介绍使用依值类型编程,但它是一个值得花一整本书专门讨论的深刻主题。 diff --git a/functional-programming-lean/src/dependent-types/indexed-families.md b/functional-programming-lean/src/dependent-types/indexed-families.md index cec32b0..b996845 100644 --- a/functional-programming-lean/src/dependent-types/indexed-families.md +++ b/functional-programming-lean/src/dependent-types/indexed-families.md @@ -1,36 +1,82 @@ + +# 索引族 + + + +多态归纳类型接受类型参数。 +例如,`List` 接受一个类型参数以决定列表中条目的类型,而 `Except` 接受两个类型参数以决定异常或值的类型。 +这些在数据类型的每个构造子中都一致的类型参数,被称为 **参量(parameters)**。 + + +然而,归纳类型中每个构造子的接受的类型参数并不一定要相同。这种不同构造子可以接受不同类型作为参数的归纳类型被称为 **索引族(indexed families)**,而这些不同的参数被称为 **索引(indices)**。 +索引族最为人熟知的例子是**向量(vectors)**类型:这个类型类似列表类型,但它除了包含列表中元素的类型,还包含列表的长度。这种类型在 Lean 中的定义如下: + ```lean {{#example_decl Examples/DependentTypes.lean Vect}} ``` + + +函数声明可以在冒号之前接受一些参数,表示这些参数在整个定义中都是可用的,也可以在冒号之后接受一些参数,函数会对它们进行模式匹配,并根据不同情形定义不同的函数体。 +归纳数据类型也有类似的原则:以 `Vect` 为例,在其顶部的数据类型声明中,参数 `α` 出现在冒号之前,表示它是一个必须提供的参量,而在冒号之后出现的 `Nat` 参数表示它是一个索引,(在不同的构造子中)可以变化。 +事实上,在 `nil` 和 `cons` 构造子的声明中,三个出现 `Vect` 的地方都将 `α` 作为第一个参数提供,而第二个参数在每种情形下都不同。 + + +`nil` 构造子的声明表明它的类型是 `Vect α 0`。 +这意味着在期望 `Vect String 3` 的上下文中使用 `Vect.nil` 会导致类型错误,就像在期望 `List String` 的上下文中使用 `[1, 2, 3]` 一样: + + ```lean {{#example_in Examples/DependentTypes.lean nilNotLengthThree}} ``` ```output error {{#example_out Examples/DependentTypes.lean nilNotLengthThree}} ``` -The mismatch between `0` and `3` in this example plays exactly the same role as any other type mismatch, even though `0` and `3` are not themselves types. + + +在这个例子中,`0` 和 `3` 之间的不匹配和其他例子中类型的不匹配是一模一样的情况,尽管 `0` 和 `3` 本身并不是类型。 + + + +类型族被称为 **族(families)**,因为不同的索引值意味着可以使用的构造子不同。 +在某种意义上,一个索引族并不是一个类型;它更像是一组相关的类型的集合,不同索引的值对应了这个集合中的一个类型。 +选择索引 `5` 作为 `Vect` 的索引意味着只有 `cons` 构造子可用,而选择索引 `0` 意味着只有 `nil` 构造子可用。 + + +如果索引是一个未知的量(例如,一个变量),那么在它变得已知之前,任何构造子都不能被使用。 +如果一个 `Vect` 的长度为 `n`,那么 `Vect.nil` 和 `Vect.cons` 都无法被用来构造这个类型,因为无法知道变量 `n` 作为一个 `Nat` 应该匹配 `0` 或 `n + 1`: + ```lean {{#example_in Examples/DependentTypes.lean nilNotLengthN}} ``` @@ -44,61 +90,133 @@ Using `n` for the length allows neither `Vect.nil` nor `Vect.cons`, because ther {{#example_out Examples/DependentTypes.lean consNotLengthN}} ``` + + +让列表的长度作为类型的一部分意味着类型具有更多的信息。 +例如 `Vect.replicate` 是一个创建包含某个值(`x`)的特定份数 (`n`) 副本的 `Vect` 的函数。 +可以精确地表示这一点的类型是: ```lean {{#example_in Examples/DependentTypes.lean replicateStart}} ``` + + + +参数 `n` 出现在结果的类型的长度中。 +以下消息描述了下划线占位符对应的任务: ```output error {{#example_out Examples/DependentTypes.lean replicateStart}} ``` + + +当编写使用索引族的程序时时,只有当 Lean 能够确定构造子的索引与期望类型中的索引匹配时,才能使用该构造子。 +然而,两个构造子的索引与 `n` 均不匹配——`nil` 匹配 `Nat.zero`,而 `cons` 匹配 `Nat.succ`。 +就像在上面的类型错误示例中的情况一样,变量 `n` 可能代表其中一个,取决于具体调用函数时 `Nat` 参数的值。 +解决这一问题的方案是利用模式匹配来同时考虑两种情形: + ```lean {{#example_in Examples/DependentTypes.lean replicateMatchOne}} ``` + + + +因为 `n` 出现在期望的类型中,对 `n` 进行模式匹配会在匹配的两种情形下 **细化(refine)** 期望的类型。 +在第一个下划线中,期望的类型变成了 `Vect α 0`: ```output error {{#example_out Examples/DependentTypes.lean replicateMatchOne}} ``` + + + +在第二个下划线中,它变成了 `Vect α (k + 1)`: + ```output error {{#example_out Examples/DependentTypes.lean replicateMatchTwo}} ``` + + + +当模式匹配不仅发现值的结构,还细化程序的类型时,这种模式匹配被称为 **依值模式匹配(dependent pattern matching)**。 + + +细化后的类型允许我们使用对应的构造子。 +第一个下划线匹配 `Vect.nil`,而第二个下划线匹配 `Vect.cons`: + ```lean {{#example_in Examples/DependentTypes.lean replicateMatchFour}} ``` + + +`.cons` 下的第一个下划线应该是一个具有类型 `α` 的值。 +恰好我们有这么一个值:`x`。 + ```output error {{#example_out Examples/DependentTypes.lean replicateMatchFour}} ``` + + + +第二个下划线应该是一个具有类型 `Vect α k` 的值。这个值可以通过对 `replicate` 的递归调用产生: + ```output error {{#example_out Examples/DependentTypes.lean replicateMatchFive}} ``` + + + +下面是 `replicate` 的最终定义: ```lean {{#example_decl Examples/DependentTypes.lean replicate}} ``` + + +除了在编写函数时提供帮助之外,`Vect.replicate` 的类型信息还允许调用方不必阅读源代码就明白它一定不是某些错误的实现。 +一个可能会产生错误长度的列表的 `replicate` 实现如下: + ```lean {{#example_decl Examples/DependentTypes.lean listReplicate}} ``` -However, making this mistake with `Vect.replicate` is a type error: + + + +然而,在实现 `Vect.replicate` 时犯下同样的错误会引发一个类型错误: + ```lean {{#example_in Examples/DependentTypes.lean replicateOops}} ``` @@ -106,9 +224,14 @@ However, making this mistake with `Vect.replicate` is a type error: {{#example_out Examples/DependentTypes.lean replicateOops}} ``` - + + +`List.zip` 函数通过将两个列表中对应的项配对(第一个列表中的第一项和第二个列表的第一项,第一个列表中的第二项和第二个列表的第二项, ……)来合并两个列表。 +这个函数可以用来将一个包含美国俄勒冈州前三座最高峰的列表和一个包含丹麦前三座最高峰的列表合并: + ```lean {{#example_in Examples/DependentTypes.lean zip1}} ``` @@ -116,20 +239,37 @@ The result is a list of three pairs: ```lean {{#example_out Examples/DependentTypes.lean zip1}} ``` + + + +当列表的长度不同时,结果应该如何呢? +与许多其他语言一样,Lean 选择忽略长的列表中的额外条目。 +例如,将一个具有俄勒冈州前五座最高峰的高度的列表与一个具有丹麦前三座最高峰的高度的列表合并会产生一个含有三个有序对的列表。 ```lean {{#example_in Examples/DependentTypes.lean zip2}} ``` + + + +求值结果为 ```lean {{#example_out Examples/DependentTypes.lean zip2}} ``` + + +这个函数总是返回一个结果,所以它非常易用。但当输入的两个列表意外地具有不同的长度时,一些数据会被悄悄地丢弃。 +F# 采用了不同的方法:它的 `List.zip` 函数在两个列表长度不匹配时抛出异常,如下面 `fsi` 会话中展示的那样: ```fsharp > List.zip [3428.8; 3201.0; 3158.5; 3075.0; 3064.0] [170.86; 170.77; 170.35];; ``` @@ -143,56 +283,129 @@ list2 is 2 elements shorter than list1 (Parameter 'list2') at .$FSI_0006.main@() Stopped due to error ``` + + +这种方法避免了数据的意外丢失,但一个输入不正确时直接崩溃的程序并不容易使用。 +在 Lean 中相似的实现可以在返回值中使用 `Option` 或 `Except` 单子,但是为了避免(可能不大的)数据丢失的风险而引入额外的(操作单子的)编程负担又并不太值得。 + + + +然而,如果使用 `Vect`,可以一个 `zip` 函数,其类型要求两个输入的列表一定具有相同的长度,如下所示: ```lean {{#example_decl Examples/DependentTypes.lean VectZip}} ``` + + +这个定义只需要考虑两个参数都是 `Vect.nil` 或都是 `Vect.cons` 的情形。Lean 接受这个定义,而不会像 `List` 的类似定义那样产生一个“存在缺失情形”的错误: ```lean {{#example_in Examples/DependentTypes.lean zipMissing}} ``` ```output error {{#example_out Examples/DependentTypes.lean zipMissing}} ``` + + + +这是因为第一个模式匹配中得到的两个构造子,`nil` 和 `cons`,**细化** 了类型检查器对长度 `n` 的知识。 +当它是 `nil` 时,类型检查器还可以确定长度是 `0`,因此第二个模式的唯一可能选择是 `nil`。 +当它是 `cons` 时,类型检查器可以确定长度是 `k+1`,因此第二个模式的唯一可能选择是 `cons`。 +事实上,添加一个同时使用 `nil` 和 `cons` 的情形会导致类型错误,因为长度不匹配: + ```lean {{#example_in Examples/DependentTypes.lean zipExtraCons}} ``` ```output error {{#example_out Examples/DependentTypes.lean zipExtraCons}} ``` + + + +长度的细化可以通过将 `n` 变成一个显式参数来观察: ```lean {{#example_decl Examples/DependentTypes.lean VectZipLen}} ``` + +## 练习 + + + +熟悉使用依值类型编程需要经验,本节的练习非常重要。 +对于每个练习,尝试看看类型检查器可以捕捉到哪些错误,哪些错误它无法捕捉。 +请通过实验代码来进行尝试。 这也是培养理解错误信息能力的好方法。 + + * 仔细检查 `Vect.zip` 在将俄勒冈州的三座最高峰与丹麦的三座最高峰组合时是否给出了正确的答案。 + 由于 `Vect` 没有 `List` 那样的语法糖,因此最好从定义 `oregonianPeaks : Vect String 3` 和 `danishPeaks : Vect String 3` 开始。 + + + + * 定义一个函数 `Vect.map`。它的类型为 `(α → β) → Vect α n → Vect β n`。 + + * 定义一个函数 `Vect.zipWith`,它将一个接受两个参数的函数依次作用在两个 `Vect` 中的每一项上。 + 它的类型应该是 `(α → β → γ) → Vect α n → Vect β n → Vect γ n`。 + + + + * 定义一个函数 `Vect.unzip`,它将一个包含有序对的 `Vect` 分割成两个 `Vect`。它的类型应该是 `Vect (α × β) n → Vect α n × Vect β n`。 - * Define a function `Vect.snoc` that adds an entry to the _end_ of a `Vect`. Its type should be `Vect α n → α → Vect α (n + 1)` and `{{#example_in Examples/DependentTypes.lean snocSnowy}}` should yield `{{#example_out Examples/DependentTypes.lean snocSnowy}}`. The name `snoc` is a traditional functional programming pun: it is `cons` backwards. + + * 定义一个函数 `Vect.snoc`,它将一个条目添加到 `Vect` 的 **末尾**。它的类型应该是 `Vect α n → α → Vect α (n + 1)`,`{{#example_in Examples/DependentTypes.lean snocSnowy}}` 应该输出 `{{#example_out Examples/ DependentTypes.lean snocSnowy}}`。`snoc` 这个名字是函数式编程常见的习语:将 `cons` 倒过来写。 + + + + * 定义一个函数 `Vect.reverse`,它反转一个 `Vect` 的顺序。 + + * 定义一个函数 `Vect.drop`。 它的类型 `(n : Nat) → Vect α (k + n) → Vect α k`。 + 通过检查 `{{#example_in Examples/DependentTypes.lean ejerBavnehoej}}` 输出 `{{#example_out Examples/DependentTypes.lean ejerBavnehoej}}` 来验证它是否正确。 + + + + * 定义一个函数 `Vect.take`。它的类型为 `(n : Nat) → Vect α (k + n) → Vect α n`。它返回 `Vect` 中的前 `n` 个条目。检查它在一个例子上的结果。 diff --git a/functional-programming-lean/src/dependent-types/indices-parameters-universes.md b/functional-programming-lean/src/dependent-types/indices-parameters-universes.md index 7cf3f24..857a243 100644 --- a/functional-programming-lean/src/dependent-types/indices-parameters-universes.md +++ b/functional-programming-lean/src/dependent-types/indices-parameters-universes.md @@ -1,53 +1,113 @@ + +# 索引、参量和宇宙层级 + +归纳类型的参量和索引的区别不仅仅是这些参数在构造子之间相同还是不同。 +当确定宇宙层级之间的关系时,归纳类型参数是参量还是索引也很重要: +归纳类型的宇宙层级可以与参量相同,但必须比其索引更大。 +这种限制是为了确保 Lean 除了作为编程语言还可以作为定理证明器——否则,Lean 的逻辑将是不一致的。 +我们将通过展示不同例子输出的错误信息来阐释决定以下两者的具体规则:宇宙层级和某个参数应该被视为参量还是索引。 + + + +通常来说,在归纳类型定义中出现在冒号之前的被当作参量,出现在冒号之后的被当作索引。 +参量像函数参数可以给出类型和名字,而索引只能给出类型。 +如 `Vect` 的定义所示: + ```lean {{#example_decl Examples/DependentTypes.lean Vect}} ``` + + + +在这个定义中,`α` 是一个参量,`Nat` 是一个索引。 +参量可以在整个定义中被使用(例如,`Vect.cons` 使用 `α` 作为其第一个参数的类型),但它们必须始终一致。 +因为索引可能会不同,所以它们在每个构造子中被分配单独的值,而不是作为参数出现在数据类型的顶部的定义中。 + + +一个非常简单的带有参量的数据类型是 `WithParameter`: + ```lean {{#example_decl Examples/DependentTypes/IndicesParameters.lean WithParameter}} ``` + + +宇宙层级 `u` 可以用于参量和归纳类型本身,说明参量不会增加数据类型的宇宙层级。 +同样,当有多个参量时,归纳类型的宇宙层级取决于这些参量的宇宙层级中最大的那个: + ```lean {{#example_decl Examples/DependentTypes/IndicesParameters.lean WithTwoParameters}} ``` + + + +由于参量不会增加数据类型的宇宙层级,使用它们很方便。 +Lean 会尝试识别像索引一样出现在冒号之后,但像参量一样使用的参数,并将它们转换为参量: +以下两个归纳数据类型的参量都出现在冒号之后: + ```lean {{#example_decl Examples/DependentTypes/IndicesParameters.lean WithParameterAfterColon}} {{#example_decl Examples/DependentTypes/IndicesParameters.lean WithParameterAfterColon2}} ``` + + +当一个参量在数据类型的声明中没有命名时,可以在每个构造子中使用不同的名称,只要它们的使用是一致的。 +以下声明被接受: + ```lean {{#example_decl Examples/DependentTypes/IndicesParameters.lean WithParameterAfterColonDifferentNames}} ``` + + + +然而,当参量的命名被指定时,这种灵活性就不被允许了: ```lean {{#example_in Examples/DependentTypes/IndicesParameters.lean WithParameterBeforeColonDifferentNames}} ``` ```output error {{#example_out Examples/DependentTypes/IndicesParameters.lean WithParameterBeforeColonDifferentNames}} ``` + + + +类似的,尝试命名一个索引会导致错误: ```lean {{#example_in Examples/DependentTypes/IndicesParameters.lean WithNamedIndex}} ``` @@ -55,14 +115,24 @@ Similarly, attempting to name an index results in an error: {{#example_out Examples/DependentTypes/IndicesParameters.lean WithNamedIndex}} ``` + + +使用适当的宇宙层级并将索引放在冒号之后会导致一个可接受的声明: + ```lean {{#example_decl Examples/DependentTypes/IndicesParameters.lean WithIndex}} ``` - + + +虽然 Lean 有时(即,在确定一个参数在所有构造子中的使用一致时)可以确定冒号后的参数是一个参量,但所有参量仍然需要出现在所有索引之前。 +试图在索引之后放置一个参量会导致该参量被视为一个索引,进而导致数据类型的宇宙层级必须增加: + ```lean {{#example_in Examples/DependentTypes/IndicesParameters.lean ParamAfterIndex}} ``` @@ -70,31 +140,54 @@ Attempting to place a parameter after an index results in the argument being con {{#example_out Examples/DependentTypes/IndicesParameters.lean ParamAfterIndex}} ``` + +参量不必是类型。这个例子显示了普通数据类型,如 `Nat` 也可以被用作参量: + ```lean {{#example_in Examples/DependentTypes/IndicesParameters.lean NatParamFour}} ``` ```output error {{#example_out Examples/DependentTypes/IndicesParameters.lean NatParamFour}} ``` + + + +按照错误信息的提示将 `4` 改成 `n` 会导致声明被接受: + ```lean {{#example_decl Examples/DependentTypes/IndicesParameters.lean NatParam}} ``` - - - + + +从以上结果中可以总结出什么? +参量和索引的规则如下: + 1. 参量在每个构造子的类型中的使用方式必须相同。 + 2. 所有参量必须在所有索引之前。 + 3. 正在定义的数据类型的宇宙层级必须至少与最大的参量宇宙层级一样大,并严格大于最大的索引宇宙层级。 + 4. 冒号前写的命名参数始终是参量,而冒号后的参数通常是索引。如果 Lean 发现冒号后的参数在所有构造子中使用一致且不在任何索引之后,则可能能够 + 这个参数是参量。 + + +当不确定时,可以使用 Lean 命令 `#print` 来检查数据类型参数中的多少是参量。 +例如,对于 `Vect`,它指出参量的数量是 1: + ```lean {{#example_in Examples/DependentTypes/IndicesParameters.lean printVect}} ``` @@ -102,9 +195,20 @@ For example, for `Vect`, it points out that the number of parameters is 1: {{#example_out Examples/DependentTypes/IndicesParameters.lean printVect}} ``` + +在选择数据类型的参数顺序时,应当考虑哪些参数应该是参量,哪些应该是索引。 +尽可能多地将参数作为参量有助于保持一个可控的宇宙层级,从而使复杂的程序的类型检查更容易进行。 +一种可能方法是确保参数列表中所有参量出现在所有索引之前。 + + + +同时,尽管 Lean 有时可以确定冒号后的参数仍然是参量,但最好使用显式命名编写参量。 +这使读者清晰的明白意图,并且 Lean 在这个参量在构造子之间有不一致的使用时会报告错误。 \ No newline at end of file diff --git a/functional-programming-lean/src/dependent-types/pitfalls.md b/functional-programming-lean/src/dependent-types/pitfalls.md index 7c302d4..efa607e 100644 --- a/functional-programming-lean/src/dependent-types/pitfalls.md +++ b/functional-programming-lean/src/dependent-types/pitfalls.md @@ -1,53 +1,129 @@ + +# 使用依值类型编程的陷阱 + + + +依值类型的灵活性允许类型检查器接受更多有用的程序,因为类型的语言足够表达那些一般类型系统不够表达的变化。 +同时,依值类型表达非常精细的规范的能力允许类型检查器拒绝更多有错误的程序。 +这种能力是有代价的。 + +返回类型的函数(如 `Row` )的实现与它的类型之间的紧密耦合是下列问题的一个具体案例: +当类型中包含函数时,接口和实现之间的区别开始瓦解。 +通常,只要重构不改变函数的类型签名或输入输出行为,它就不会导致问题。 +所以一个函数可以方便地进行下列重构而不会破坏客户端代码:使用更高效的算法和数据结构重写,修复错误,提高代码的清晰度。 +然而,当函数出现在类型中时,函数的内部实现成为类型的一部分,因此成为另一个程序的**接口**的一部分。 + + + +以 `Nat` 上的加法的两个实现为例。 +`Nat.plusL` 对第一个参数进行递归: ```lean {{#example_decl Examples/DependentTypes/Pitfalls.lean plusL}} ``` + + + +`Nat.plusR` 则对第二个参数进行递归: ```lean {{#example_decl Examples/DependentTypes/Pitfalls.lean plusR}} ``` + + +两种加法的实现都与数学概念一致,因此在给定相同参数时返回相同的结果。 + + + +然而,当这两种实现用于类型时,它们呈现出非常不同的接口。 +以一个将两个 `Vect` 连接起来的函数为例。 +这个函数应该返回一个长度为两个参数的长度之和的 `Vect`。 +因为 `Vect` 本质上是一个带有更多信息的`List`,所以写这个函数类似 `List.append`,对第一个参数进行模式匹配和递归。 + +让我们给定一个初始的类型签名然后进行模式匹配。占位符给出两条信息: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean appendL1}} ``` + + + +第一个信息:在 `nil` 的情形下,占位符应该被替换为一个长度为 `plusL 0 k` 的 `Vect`: ```output error {{#example_out Examples/DependentTypes/Pitfalls.lean appendL1}} ``` + + + +第二个信息:在`cons`的情形下,占位符应该被替换为一个长度为`plusL (n✝ + 1) k` 的 `Vect`: ```output error {{#example_out Examples/DependentTypes/Pitfalls.lean appendL2}} ``` + + + +`n` 后面的符号,称为**剑标(dagger)**,用于表示 Lean 内部生成的名称。 +对第一个 `Vect` 的模式匹配隐式导致第一个 `Nat` 的值也被细化,因为构造子`cons`的索引是`n + 1`,`Vect`的尾部长度为`n`。 +在这里,`n✝`表示比参数 `n` 小1的 `Nat`。 + +## 定义相等性 + + + +在 `plusL` 的定义中,有一个模式`0, k => k`。 +因此第一个下划线的类型 `Vect α (Nat.plusL 0 k)` 的另一个写法是 `Vect α k`。 +类似地,`plusL` 包含另一个模式 `n + 1, k => plusN n k + 1`。 +因此第二个下划线的类型可以等价地写为`Vect α (plusL n✝ k + 1)`。 + + +为了清楚到底发生了什么,第一步是显式地写出 `Nat` 参数。这一变化同时导致错误信息中的剑标消失了,因为此时程序已经显式给出了这个参数的名字: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean appendL3}} ``` @@ -57,7 +133,13 @@ To expose what is going on behind the scenes, the first step is to write the `Na ```output error {{#example_out Examples/DependentTypes/Pitfalls.lean appendL4}} ``` + + + +用简化版本的类型注释下划线不会导致类型错误,这意味着程序中写的类型与 Lean 自己找到的类型是等价的: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean appendL5}} ``` @@ -68,9 +150,16 @@ Annotating the underscores with the simplified versions of the types does not in {{#example_out Examples/DependentTypes/Pitfalls.lean appendL6}} ``` + + +第一个情形要求一个`Vect α k`,而 `ys` 有这种类型。 +这跟将一个列表附加到一个空列表时直接返回这个列表的情况相似。 +用 `ys` 替代第一个下划线后,只剩下一个下划线需要填充: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean appendL7}} ``` @@ -78,21 +167,44 @@ Refining the definition with `ys` instead of the first underscore yields a progr {{#example_out Examples/DependentTypes/Pitfalls.lean appendL7}} ``` + +这里发生了非常重要的事情。 +在 Lean 期望一个 `Vect α (Nat.plusL 0 k)` 的上下文中,它接受了一个 `Vect α k` 。 +然而,`Nat.plusL`不是一个 `abbrev`,所以似乎它不应该在类型检查期间运行。 +还有其他事情发生了。 + + + +理解发生了什么的关键在于 Lean 在类型检查期间不止展开所有 `abbrev` 的定义。 +它还可以在检查两个类型是否等价时执行计算,从而允许一个具有类型A的表达式可以在一个期待类型B的上下文中被使用。 +这种属性称为**定义相等性(definitional equality)**。这种相等性很微妙。 + + +当然,完全相同的两个类型被认为是定义相等的,例如`Nat`和`Nat`或`List String`和`List String`。 +任何两个由不同数据类型构造的具体类型都不相等,因此`List Nat`不等于`Int`。 +此外,两个只在内部名称上存在不同的类型(译者注:即α-等价)是相等的,例如`(n : Nat) → Vect String n`与`(k : Nat) → Vect String k`。 +因为类型可以包含普通数据,定义相等还必须描述何时数据是相等的。 +使用相同构造子的数据是相等的,因此`0`等于`0`,`[5, 3, 1]`等于`[5, 3, 1]`。 + + + +然而,类型不仅包含函数类型、数据类型和构造子。 +它们还包含**变量**和**函数**。 +变量的定义相等性相对简单:每个变量只等于自己,因此`(n k : Nat) → Vect Int n`不等于`(n k : Nat) → Vect Int k`。 +函数则复杂得多。数学上对函数相等的定义为两个函数具有相同的输入输出行为。但这种相等性无法被算法检查。 +这违背了而定义相等性的目的:通过算法自动检查两个类型是否相等。 +因此,Lean 认为函数只有在它们的函数体定义相等时才是定义相等的。 +换句话说,两个函数必须使用**相同的算法**,调用**相同的辅助函数**,才能被认为是定义相等的。 +这通常不是很有用,因此函数的定义相等一般只用于当两个类型中出现完全相同的函数时。 + + + +当函数在类型中被**调用**时,检查定义相等可能涉及规约这些调用。 +类型 `Vect String (1 + 4)` 与类型 `Vect String (3 + 2)` 是定义相等的,因为 `1 + 4` 与 `3 + 2` 是定义相等的。 +为了检查它们的相等性,两者都被规约为`5`,然后使用五次“构造子”规则。 + +检查函数应用于数据的定义相等性可以首先检查它们是否已经相同——例如,检查`["a", "b"] ++ ["c"]`是否等于`["a", "b"] ++ ["c"]`时没有必要进行规约。 +如果不同,调用函数并继续检查结果的定义相等性。 + +并非所有函数参数都是具体数据。 +例如,类型可能包含不是由 `zero` 和 `succ` 构造子构建的`Nat`。 +在类型`(n : Nat) → Vect String n`中,变量`n`是一个`Nat`,但在调用函数之前不可能知道它**哪个**`Nat`。 +实际上,函数可能首先用`0`调用,然后用`17`调用,然后再用`33`调用。 +如`appendL`的定义中所见,类型为`Nat`的变量也可以传递给`plusL`等函数。 +实际上,类型`(n : Nat) → Vect String n`和`(n : Nat) → Vect String (Nat.plusL 0 n)`定义相等。 + + + +`n` 和 `Nat.plusL 0 n` 是定义相等的原因是 `plusL` 对的**第一个**参数进行模式匹配。 +这在别的情况下会导致问题:`(n : Nat) → Vect String n` 与`(n : Nat) → Vect String (Nat.plusL n 0)` 并**不**定义相等,尽管0应该同时是加法的左和右单位元。 +这是因为模式匹配在遇到变量时会卡住。 +在 `n` 的实际值变得已知之前,没有办法知道应该选择 `Nat.plusL n 0` 的哪种情形。 + + +同样的问题出现在查询示例中的 `Row` 函数中。 +类型`Row (c :: cs)`不会规约到任何数据类型,因为 `Row` 的定义对单例列表和至少有两个条目的列表的处理方式不同。 +换句话说,当尝试将变量`cs`与具体的`List`构造子匹配时会卡住。 +这就是为什么几乎每个拆分或构造 `Row` 的函数都需要与 `Row` 本身对应的三种情形:为了获得模式匹配或构造子可以使用的具体类型。 + + +`appendL`中缺失的情形需要一个`Vect α (Nat.plusL n k + 1)`。 +索引中的`+ 1`表明下一步是使用`Vect.cons`: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean appendL8}} ``` ```output error {{#example_out Examples/DependentTypes/Pitfalls.lean appendL8}} ``` + + + +一个对 `appendL` 的递归调用可以构造一个具有所需长度的 `Vect` : + ```lean {{#example_decl Examples/DependentTypes/Pitfalls.lean appendL9}} ``` + + + +既然程序完成了,删除对 `n` 和 `k` 的显式匹配使得这个函数更容易阅读和调用: + ```lean {{#example_decl Examples/DependentTypes/Pitfalls.lean appendL}} ``` + + +比较类型使用定义相等意味着定义相等中涉及的所有内容,包括函数的内部定义,都成为使用依值类型和索引族的程序的**接口**的一部分。 +在类型中暴露函数的内部实现意味着重构暴露的函数可能导致使用它的程序无法通过类型检查。 +特别是,`plusL`在 `appendL` 的类型中使用的事实意味着 `plusL` 的使用不能被等价的 `plusR` 替换。 + + +## 在加法上卡住 + + +如果使用 `plusR` 定义 `append` 会发生什么? +让我们从头来过。使用显式长度并用占位符填充每种情形,会显示以下有用的错误消息: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean appendR1}} ``` @@ -159,21 +347,43 @@ Beginning in the same way, with explicit lengths and placeholder underscores in ```output error {{#example_out Examples/DependentTypes/Pitfalls.lean appendR2}} ``` + + + +然而,尝试在第一个占位符上添加一个`Vect α k`类型注释会导致类型不匹配错误: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean appendR3}} ``` ```output error {{#example_out Examples/DependentTypes/Pitfalls.lean appendR3}} ``` + + +这个错误指出 `plusR 0 k` 和 `k` **不**定义相等。 + + + +这是因为 `plusR` 有以下定义: ```lean {{#example_decl Examples/DependentTypes/Pitfalls.lean plusR}} ``` + + + +它的模式匹配发生在**第二**个参数上,而非第一个,这意味着该位置上的变量 `k` 阻止了它的规约。 +Lean 标准库中的 `Nat.add` 等价于 `plusR` ,而不是 `plusL` ,因此尝试在这个定义中使用它会导致完全相同的问题: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean appendR4}} ``` @@ -181,35 +391,78 @@ Its pattern matching occurs on the _second_ argument, not the first argument, wh {{#example_out Examples/DependentTypes/Pitfalls.lean appendR4}} ``` + + +加法在变量上**卡住**。 +解决它需要[命题相等](../type-classes/standard-classes.md#equality-and-ordering)。 + + +## 命题相等性 + +命题相等性是两个表达式相等的数学陈述。 +Lean 在需要时会自动检查定义相等性,但命题相等性需要显式证明。 +一旦一个相等命题被证明,它就可以在程序中被使用,从而将一个类型替换为等式另一侧的类型,从而解套卡住的类型检查器。 + + +定义相等性只规定了很有限的相等性,所以它可以被算法自动地检查。 +命题相等性要丰富得多,但计算机通常无法检查两个表达式是否命题相等,尽管它可以验证所谓的证明是否实际上是一个证明。 +定义相等和命题相等之间的分裂代表了人类和机器之间的分工:最无聊的相等性作为定义相等的一部分被自动检查,从而使人类思维可以处理命题相等中可用的有趣问题。 +同样,定义相等性由类型检查器自动调用,而命题相等必须明确地被调用。 + + +在[命题、证明和索引](../props-proofs-indexing.md)中,一些相等性命题使用 `simp` 证明。 +那里面的相等性命题实际上已经定义相等。 +通常,命题相等性的证明是通过首先将它们变成定义相等或接近现有证明的相等性的形式,然后使用像 `simp` 这样的策术来处理简化后的情形。 +`simp` 策术非常强大:它使用许多快速的自动化工具来构造证明。 +一个更简单的策术叫做 `rfl` ,它专门使用定义相等来证明命题相等。 +`rfl` 的名称来自**反射性(reflexivity)**的缩写,它是相等性的一个属性:一切都等于自己。 + + +解决`appendR`需要一个证明,即`k = Nat.plusR 0 k`。它们并不定义相等,因为`plusR`在第二个参数的变量上卡住了。 +为了让它计算,`k`必须是一个具体的构造子。 +这时,我们可以使用模式匹配。 + + +因为 `k` 可以是**任何** `Nat` ,所以我们需要一个对任何 `k` 都能返回 `k = Nat.plusR 0 k` 的证据的函数。 +它的类型应该为`(k : Nat) → k = Nat.plusR 0 k`。 +进行模式匹配并输入占位符后得到以下信息: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean plusR_zero_left1}} ``` @@ -219,15 +472,29 @@ Getting it started with initial patterns and placeholders yields the following m ```output error {{#example_out Examples/DependentTypes/Pitfalls.lean plusR_zero_left2}} ``` + + + +将 `k `通过模式匹配细化为 `0` 后,第一个占位符需要一个定义相等的命题的证据。 +使用 `rfl` 策术完成它,只留下第二个占位符: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean plusR_zero_left3}} ``` + + +第二个占位符有点棘手。 +表达式`{{#example_in Examples/DependentTypes/Pitfalls.lean plusRStep}}`定义相等于`{{#example_out Examples/DependentTypes/Pitfalls.lean plusRStep}}`。 +这意味着目标也可以写成`k + 1 = Nat.plusR 0 k + 1`: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean plusR_zero_left4}} ``` @@ -235,69 +502,148 @@ This means that the goal could also be written `k + 1 = Nat.plusR 0 k + 1`: {{#example_out Examples/DependentTypes/Pitfalls.lean plusR_zero_left4}} ``` + + +在等式命题两侧的 `+ 1` 下面是函数本身返回的另一个实例。 +换句话说,对 `k` 的递归调用将返回 `k = Nat.plusR 0 k` 的证据。 +如果相等性不适用于函数参数,那么它就不是相等性。 +换句话说,如果 `x = y` ,那么 `f x = f y` 。 +标准库包含一个函数`congrArg`,它接受一个函数和一个相等性证明,并返回一个新的证明,其中函数已经应用于等式的两侧。 +在这种情形下,函数是`(· + 1)`: + ```lean {{#example_decl Examples/DependentTypes/Pitfalls.lean plusR_zero_left_done}} ``` + + +命题相等性可以使用右三角运算符`▸`在程序中使用。 +给定一个相等性证明作为第一个参数,另一个表达式作为第二个参数,这个运算符将第二个参数类型中等式左侧的实例替换为等式的右侧的实例。 +换句话说,以下定义不会导致类型错误: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean appendRsubst}} ``` + + + +第一个占位符有预期的类型: + ```output error {{#example_out Examples/DependentTypes/Pitfalls.lean appendRsubst}} ``` + + + +现在可以用`ys`填充它: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean appendR5}} ``` + + +填充剩下的占位符需要解套另一个卡住的加法: + ```output error {{#example_out Examples/DependentTypes/Pitfalls.lean appendR5}} ``` + + +这里,要证明的命题是 `Nat.plusR (n + 1) k = Nat.plusR n k + 1`,可以使用`▸`将`+ 1`拉到表达式的顶部,使其与`cons`的索引匹配。 + + + +证明是一个递归函数,它对 `plusR` 的第二个参数 `k` 进行模式匹配。 +这是因为 `plusR` 自身也是对第二个参数进行模式匹配,所以证明可以相同的模式匹配解套它,将计算行为暴露出来。 +证明的框架与`plusR_zero_left`非常相似: + ```lean {{#example_in Examples/DependentTypes/Pitfalls.lean plusR_succ_left_0}} ``` + + +剩下的情形的类型在定义上等于 `Nat.plusR (n + 1) k + 1 = Nat.plusR n (k + 1) + 1`,因此可以像 `plusR_zero_left` 一样用 `congrArg` 解决: + ```output error {{#example_out Examples/DependentTypes/Pitfalls.lean plusR_succ_left_2}} ``` + + + +证明就此完成 ```lean {{#example_decl Examples/DependentTypes/Pitfalls.lean plusR_succ_left}} ``` + + +完成的证明可以用来解套`appendR`中的第二个情形: + ```lean {{#example_decl Examples/DependentTypes/Pitfalls.lean appendR}} ``` + + + +如果再次将 `appendR` 的长度参数改成隐式参数,它们在证明中也将不具有显示的名字。 +然而,Lean 的类型检查器有足够的信息自动填充它们,只有唯一的值可以使类型匹配: + ```lean {{#example_decl Examples/DependentTypes/Pitfalls.lean appendRImpl}} ``` + + +## 优势和劣势 + + +索引族有一个重要的特性:对它们进行模式匹配会影响定义相等性。 +例如,在`Vect`上的`match`表达式中的`nil`情形中,长度会直接**变成**`0`。 +定义相等非常好用,因为它从不需要显式调用。 + + + +然而,使用依赖类型和模式匹配的定义相等在软件工程上有严重的缺点。 +首先,在类型中使用的函数需要额外编写,同时在类型中方便使用的实现并不一定是一个高效的实现。 +一旦一个函数在类型中被使用,它的实现就成为接口的一部分,导致未来重构困难。 +其次,检查定义相等性可能会很慢。 +当检查两个表达式是否定义相等时,如果相关的函数复杂并且有许多抽象层,Lean 可能需要运行大量代码。 +第三,定义相等检查失败而报告的错误信息可能很难理解,因为它们通常包含了函数内部实现相关的信息。 +并不总是容易理解错误消息中表达式的来源。 +最后,在一组索引族和依赖类型函数中编码非平凡的不变性通常是脆弱的。 +当函数的规约行为不能方便地提供需要的定义相等性时,通常需要更改系统中的早期定义。 +另一种方法是在程序中的很多地方手动引入相等性的证明,但这样会变得非常麻烦。 + + +在惯用的 Lean 代码中,带有索引的数据类型并不经常使用。 +相反,子类型和显式命题通常用于保证重要的不变性。 +这种方法涉及许多显式证明,而很少直接使用定义相等。 +为了可以被用作一个交互式定理证明器,Lean 的很多设计是为了使显式证明方便。 +一般来说,在大多数情况下,应该优先考虑这种方法。 + + +然而,理解索引族是重要的。 +诸如 `plusR_zero_left` 和 `plusR_succ_left` 之类的递归函数实际上是**使用了数学归纳法的证明**。 +递归的基情形对应于归纳的基情形,递归调用则表示对归纳假设的使用。 +更一般地说,Lean 中的新命题通常被定义为证据的归纳类型,这些归纳类型通常具有索引。 +证明定理的过程实际上是在构造具有这些类型的表达式,这个过程与本节中的证明非常相似。 +此外,索引数据类型有时确实是最佳选择。熟练掌握它们的使用是知道何时使用它们的一个重要部分。 - + + +## 练习 + + + * 使用类似于`plusR_succ_left`的递归函数,证明对于所有的`Nat` `n` 和 `k`,`n.plusR k = n + k`。 + + + + * 写一个在 `Vect` 上的函数,其中 `plusR` 比 `plusL` 更自然:`plusL` 需要在定义中显示使用(命题相等性的)证明。 diff --git a/functional-programming-lean/src/dependent-types/summary.md b/functional-programming-lean/src/dependent-types/summary.md index 70f87e3..37c51c6 100644 --- a/functional-programming-lean/src/dependent-types/summary.md +++ b/functional-programming-lean/src/dependent-types/summary.md @@ -1,48 +1,119 @@ + +# 总结 + + + +## 依值类型 + + +依值类型允许类型包含非类型代码,如函数调用和数据构造子,使类型系统的表达能力大大增强。 +从参数的**值**中**计算**类型的能力意味着函数的返回类型可以根据提供的参数而变化。 +例如,可以使数据库查询的结果的类型依赖于数据库模式和具体的查询,而无需对查询结果进行任何可能失败的强制类型转换操作。 +当查询发生变化时,运行它得到的结果的类型也会发生变化,从而获得即时的编译时反馈。 + +当函数的返回类型取决于一个值时,使用模式匹配分析值可能导致类型被**细化**,因为代表值的变量被模式中的构造子替换。 +函数的类型签名记录了返回类型如何取依赖于参数的值, +所以模式匹配解释了返回类型如何根据不同的潜在参数变成一个更具体的类型。 + + + + +出现在类型中的普通代码在类型检查期间运行,其中可能导致无限循环的 `partial` 函数不会被调用。 +大多数情况下,这种计算遵循了[本书开头](../getting-to-know/evaluating.md)介绍的普通求值规则: +子表达式逐渐被其值替换,直到整个表达式变成了一个值。 +类型检查期间的计算与运行时计算有一个重要的区别:类型中的一些值可能是**变量**,意味着这些值还未知。 +在这些情况下,模式匹配会“卡住”,直到确定这个变量对应特定的构造子(例如通过对其进行模式匹配)。 +类型级别的计算可以看作是一种部分求值:只求值完全已知的程序部分,剩下的部分则保持不变。 + + + +# 宇宙设计模式 + +一个在使用依值类型时常见的设计模式是将类型系统的某个子集显示地划分出来。 +例如,数据库查询库可能能够返回可变长度的字符串、固定长度的字符串或某些范围内的数字,但它永远不会返回函数、用户定义的数据类型或`IO`操作。 +一个领域特定的类型子集的定义方式如下:首先定义一个具有与所需类型结构匹配的构造子的数据类型,然后定义将这个数据类型的值解释为真实的类型一个函数。 +这些构造子被称为所讨论类型的**编码(codes)**,整个设计模式有时被称为 **Tarski风格的宇宙**设计模式。当上下文清楚地表明此时宇宙不指代`Type 3`或`Prop`等时,可以简称为**宇宙**设计模式。 + + +自定义宇宙,相比于类型类,是另一种划定一组感兴趣的类型的方式。 +类型类是可扩展的,这种扩展性并非总是好的。 +定义自定义宇宙相对于直接使用类型具有许多优点: + * 可以通过对**编码**进行递归来实现对宇宙中包含的**任意**类型的通用操作,例如相等性测试和序列化。 + * 可以精确地表示外部系统接受的类型,并且编码的数据类型的定义相当于一个预期类型的文档。 + * Lean 的模式匹配完整性检查器确保没有遗漏对编码的处理, + 而基于类型类的解决方案则在客户端代码的实际调用才能检查某些类型的类型类实例是否遗漏。 + + +## 索引族 + +数据类型可以接受两种不同类型的参数:**参量(parameter)** 在每个构造子都是相同的,而 **索引(index)** 则可以在不同构造子间不同。 +特定的索引意味着只有特定的构造子可用。 +例如,`Vect.nil` 仅在长度索引为 `0` 时可用,而 `Vect.cons` 仅在长度索引为 `n+1` 时可用。 +虽然参量通常以命名参数写在数据类型声明中的冒号前,索引写在冒号后(作为某个函数类型的参数),但 Lean 可以推断冒号后的参数何时被用作参量。 + + + +索引族允许表达数据之间的复杂关系,所有这些关系都由编译器检查。 +数据类型的不变性可以直接通过索引族编码,从而保证这些不变性不会被(哪怕是暂时地)违反。 +向编译器提供关于数据类型不变性的信息带来了一个重大好处:编译器现在可以告诉程序员必须做什么才能满足这些不变性。 +通过刻意地触发编译期错误(特别是通过下划线占位符触发),可以将 “此时需要注意什么不变性” 的任务交给 Lean 思考 ,从而使程序员可以花更多心思担心其他事情。 + +使用索引族编码不变性有时会导致困难。 +首先,每个不变性都需要自己的数据类型,然后需要自己的支持库。 +毕竟,`List.append` 和 `Vect.append` 是不能互换的。这都会导致代码重复。 +其次,方便使用索引族需要类型中使用的函数的递归结构与被类型检查的程序的递归结构相匹配。 +使用索引族编程正是“正确安排这些匹配发生”的艺术。 +虽然可以通过手动引入相等性证明解决不匹配的巧合,但这件事并不容易,而且会导致程序中充斥着难懂的代码。 +第三,类型检查期间运行过于复杂的代码可能导致很长的编译时间。避免这些复杂程序带来的编译减速可能需要专门的技术。 + + + +## 定义相等性和命题相等性 + +Lean的类型检查器必须不时检查两个类型是否应该被视为可互换的。 +因为类型可以包含任意程序,所以它必须能够检查任意程序的相等性。 +然而,没有有效的算法可以检查任意两个程序在数学意义上的相等性。 +为了解决这个问题,Lean 引入了两种相等性的概念: + + + + * **定义相等性(Definitional equality)** 是一个对程序相等性的近似:定义相等的程序一定相等,但反之不然。它基本只上检查(在允许计算和绑定变量重命名的意义下)语法表示的相等性。Lean 在需要时会自动检查定义相等。 + + * **命题相等性(Propositional equality)** 必须由程序员显式证明和显式调用。Lean 会自动检查证明是否正确,并检查对这种相等性的调用是否使得证明目标被完成。 + + + +这两种相等性概念代表了程序员和 Lean 之间的分工。 +定义相等性简单但自动,命题相等性手动但表达力强。 +命题相等性可以用于解套类型中的一些卡住的程序 +(比如因为无法对变量求值)。 + + +然而过于频繁地使用命题相等性来解套类型层面的卡住的计算 +通常意味着代码是一段臭代码:这意味着没有很好地设计匹配。 +这时较好的方案是重新设计类型和索引, +或者使用其他的技术来保证程序不变性。 +当命题相等被用来证明程序满足规范, +或作为子类型的一部分时, +则是一种常见的模式。 diff --git a/functional-programming-lean/src/dependent-types/typed-queries.md b/functional-programming-lean/src/dependent-types/typed-queries.md index b7bb56c..e47fdde 100644 --- a/functional-programming-lean/src/dependent-types/typed-queries.md +++ b/functional-programming-lean/src/dependent-types/typed-queries.md @@ -1,21 +1,52 @@ + +# 实际案例:类型化查询 + + + +类型族在构建一个模仿其他语言的 API 时非常有用。 +它们可以用来编写一个保证生成合法页面的 HTML 生成器,或者编码某种文件格式的配置,或是用来建模复杂的业务约束。 +本节描述了如何在 Lean 中使用索引族对关系代数的一个子集进行编码,然而本节的展示的技术完全可以被用来构建一个更加强大的数据库查询语言。 + +这个子集使用类型系统来保证某些要求,比如字段名称的不相交性,并使用类型上的计算将数据库模式(Schema)反映到从查询返回的值的类型中。 +它并不是一个实际的数据库系统——数据库用链表的链表表示;类型系统比 SQL 的简单得多;关系代数的运算符与 SQL 的运算符并不完全匹配。 +然而,它足够用来展示使用索引族的一些有用的原则和技术。 + + + +## 一个数据的宇宙 + + + +在这个关系代数中,保存在列中的基本数据的类型包括 `Int`、`String` 和 `Bool`,并由宇宙 `DBType` 描述: + ```lean {{#example_decl Examples/DependentTypes/DB.lean DBType}} ``` + + +`asType` 将这些编码转化为类型: + ```lean {{#example_in Examples/DependentTypes/DB.lean mountHoodEval}} ``` @@ -23,309 +54,698 @@ For example: {{#example_out Examples/DependentTypes/DB.lean mountHoodEval}} ``` + + +可以对三种类型的任何两个值都判断是否相等。 +然而,向 Lean 解释这一点需要一些工作。 +直接使用 `BEq` 会失败: + ```lean {{#example_in Examples/DependentTypes/DB.lean dbEqNoSplit}} ``` ```output info {{#example_out Examples/DependentTypes/DB.lean dbEqNoSplit}} ``` + + + +就像在嵌套对的宇宙中一样,类型类搜索不会自动检查 `t` 的值的每种可能性。 +解决方案是使用模式匹配来细化 `x` 和 `y` 的类型: + ```lean {{#example_decl Examples/DependentTypes/DB.lean dbEq}} ``` + + + +在这个版本的函数中,`x` 和 `y` 在三种情形下的类型分别为 `Int`、`String` 和 `Bool`,这些类型都有 `BEq` 实例。 +`dbEq` 的定义可以用来为 `DBType` 编码的类型定义一个 `BEq` 实例: + ```lean {{#example_decl Examples/DependentTypes/DB.lean BEqDBType}} ``` + + + +这个实例与编码本身的实例不同: ```lean {{#example_decl Examples/DependentTypes/DB.lean BEqDBTypeCodes}} ``` + + + +前一个实例允许比较编码描述的类型中的值,而后一个实例允许比较编码本身。 + + +一个 `Repr` 实例可以使用相同的技术编写。 +`Repr` 类的方法被称为 `reprPrec`,因为它在显示值时考虑了操作符优先级等因素。 +通过依值模式匹配细化类型,可以使用 `Int`、`String` 和 `Bool` 的 `Repr` 实例的 `reprPrec` 方法: + ```lean {{#example_decl Examples/DependentTypes/DB.lean ReprAsType}} ``` + +## 数据库模式和表 + + + +一个数据库模式描述了数据库中每一列的名称和类型: + ```lean {{#example_decl Examples/DependentTypes/DB.lean Schema}} ``` + + + +事实上,数据库模式可以看作是描述表中行的宇宙。 +空数据库模式描述了 `Unit` 类型,具有单个列的数据库模式描述了那个值本身,具有至少两个列的数据库模式可以有由元组表示: + ```lean {{#example_decl Examples/DependentTypes/DB.lean Row}} ``` + + +正如在[积类型的起始节](../getting-to-know/polymorphism.md#prod)中描述的那样,Lean 的积类型和元组是右结合的。 +这意味着嵌套对等同于普通的展平元组。 + + +表是一个共享数据库模式的行的列表: + ```lean {{#example_decl Examples/DependentTypes/DB.lean Table}} ``` + + +例如,可以用数据库模式 `peak` 表示对山峰的拜访日记: + ```lean {{#example_decl Examples/DependentTypes/DB.lean peak}} ``` + + + +本书作者拜访过的部分山峰以元组的列表呈现: + ```lean {{#example_decl Examples/DependentTypes/DB.lean mountainDiary}} ``` + + + +另一个例子包括瀑布和对它们的拜访日记: + ```lean {{#example_decl Examples/DependentTypes/DB.lean waterfall}} {{#example_decl Examples/DependentTypes/DB.lean waterfallDiary}} ``` + + +### 回顾递归和宇宙 + + +将行结构化为元组的方便性是有代价的:`Row` 将其两个基情形的分开处理意味着在类型中使用 `Row` 和在编码(即数据库模式)上递归定义的函数需要做出相同的区分。 +一个具体的例子是一个通过对数据库模式递归检查行是否相等的函数。 +下面的实现无法通过 Lean 的类型检查: + ```lean {{#example_in Examples/DependentTypes/DB.lean RowBEqRecursion}} ``` ```output error {{#example_out Examples/DependentTypes/DB.lean RowBEqRecursion}} ``` + + + +问题在于模式 `col :: cols` 并没有足够细化行的类型。 +这是因为 Lean 无法确定到底是 `Row` 定义中的哪种模式被匹配上:单例模式 `[col]` 或是 `col1 :: col2 :: cols` 模式。因此对 `Row` 的调用不会计算到一个有序对类型。 +解决方案是在 `Row.bEq` 的定义中反映 `Row` 的结构: + ```lean {{#example_decl Examples/DependentTypes/DB.lean RowBEq}} ``` + +不同于其他上下文,出现在类型中的函数不能仅仅考虑其输入/输出行为。 +使用这些类型的程序将发现自己被迫镜像那些类型中使用到的函数所使用的算法,以便它们的结构与类型的模式匹配和递归行为相匹配。 +使用依赖类型编程的技巧的一个重要部分是在类型的计算中选择具有正确计算行为函数。 + + + +### 列指针 + + +如果数据库模式包含特定列,那么某些查询才有意义。 +例如,一个返回海拔高于 1000 米的山的查询只在包含整数的 `"elevation"` 列的数据库模式中才有意义。 +一种表示数据库模式包含某个列的方法是直接提供指向这个列的指针。将指针定义为一个索引族使得可以排除无效指针。 + +列可以出现在数据库模式的两个地方:要么在它的开头,要么在它的后面的某个地方。 +如果列出现在模式的后面的某个地方,那么它也必然是某一个尾数据库模式的开头。 + + + +索引族 `HasCol` 将这种规范表达为 Lean 的代码: + ```lean {{#example_decl Examples/DependentTypes/DB.lean HasCol}} ``` + + + +这个族的三个参数是数据库模式、列名和它的类型。 +所有三个参数都是索引,但重新排列参数,将数据库模式放在列名和类型之后,可以使列名和类型成为参量。 +当数据库模式以列 `⟨name, t⟩` 开头时,可以使用构造子 `here`:它是一个指向当前数据库模式的第一列的指针,只有当第一列具有所需的名称和类型时才能使用。 +构造子 `there` 将一个指向较小数据库模式的指针转换为一个指向在头部包含在一个额外列的数据库模式的指针。 + + +因为 `"elevation"` 是 `peak` 中的第三列,所以可以通过 `there` 跳过前两列然后使用 `here` 找到它。 +换句话说,要满足类型 `{{#example_out Examples/DependentTypes/DB.lean peakElevationInt}}`,使用表达式 `{{#example_in Examples/DependentTypes/DB.lean peakElevationInt}}`。 +`HasCol` 也可以理解为是一种带有修饰的 `Nat`——`zero` 对应于 `here`,`succ` 对应于 `there`。 +额外的类型信息使得不可能出现列序号偏差了一位之类的错误。 + + +指向数据库模式中的列的指针可以用来从行中提取该列的值: + ```lean {{#example_decl Examples/DependentTypes/DB.lean Rowget}} ``` + + + +第一步是对数据库模式进行模式匹配,因为这决定了行是元组还是单个值。 +空模式的情形不需要考虑,因为 `HasCol`的两个构造子都对应着非空的数据库模式。 +如果数据库模式只有一个列,那么指针必须指向它,因此只需要匹配 `HasCol` 的 `here` 构造子。 +如果数据库模式有两个或更多列,那么必须有一个 `here` 的情形,此时值是行中的第一个值,以及一个 `there` 的情形,此时需要进行递归调用。 +`HasCol` 类型保证了列存在于行中,所以 `Row.get` 不需要返回一个 `Option`。 + + +`HasCol` 扮演了两个角色: + + + 1. 它作为**证据**,证明模式中存在具有特定名称和类型的列。 + + + 2. 它作为**数据**,可以用来在行中找到与列关联的值。 + +第一个角色,即证据的角色,类似于命题的使用方式。 +索引族 `HasCol` 的定义可以被视为一个规范,说明什么样的证据可以证明给定的列存在。 +然而,与命题不同,使用 `HasCol` 的哪个构造子很重要。 +在第二个角色中,构造子起到类似 `Nat`的作用,用于在集合中查找数据。 +使用索引族编程通常需要能够流畅地使用它的这两个角色。 + + + +### 子数据库模式 + +关系代数中的一个重要操作是将表或行**投影**到一个较小的数据库模式中。 +不在这一数据库模式中的每一列都会被舍弃。 +为了使投影有意义,小数据库模式必须是大数据库模式的子数据库模式:小数据库模式中的每一列都必须存在于大数据库模式中。 +正如 `HasCol` 允许我们编写一个从行中提取某个列函数且这个函数一定不会失败一样, +将子模式关系表示为索引族允许我们编写一个不会失败的投影函数。 + + + +可以将“一个数据库模式是另一个数据库模式的子数据库模式”定义为一个索引族。 +基本思想是,如果小数据库模式中的每一列都出现在大数据库模式中,那么小数据库模式就是大数据库模式的子数据库模式。 +如果小数据库模式为空,则它肯定是大数据库模式的子数据库模式,由构造子 `nil` 表示。 +如果小数据库模式有一列,那么该列必须在大数据库模式中且子数据库模式中的其余列也必须是大数据库模式的子数据库模式。 +这由子 `cons` 表示。 + ```lean {{#example_decl Examples/DependentTypes/DB.lean Subschema}} ``` + + +换句话说,`Subschema` 为小数据库模式的每一列分配一个 `HasCol`,该 `HasCol` 指向大数据库模式中的位置。 + + +模式 `travelDiary` 表示 `peak` 和 `waterfall` 共有的字段: + ```lean {{#example_decl Examples/DependentTypes/DB.lean travelDiary}} ``` + + + +正如这个例子所示,它肯定是 `peak` 的子数据库模式: + ```lean {{#example_decl Examples/DependentTypes/DB.lean peakDiarySub}} ``` + + + +然而,这样的代码很难阅读和维护。 +改进的一种方法是指导 Lean 自动编写 `Subschema` 和 `HasCol` 构造子。 +这可以通过使用[关于命题和证明的插曲](../props-proofs-indexing.md)中介绍的策术特性来完成。 +该插曲使用 `by simp` 提供了各种命题的证据。 + +此时,两种策术是有用的: + * `constructor` 策术指示 Lean 使用数据类型的构造子解决问题。 + * `repeat` 策术指示 Lean 重复一个策术,直到它失败或证明完成。 + + + +下一个例子中,`by constructor` 的效果与直接写 `.nil` 是一样的: + ```leantac {{#example_decl Examples/DependentTypes/DB.lean emptySub}} ``` + + + +然而,在一个稍微复杂的类型下尝试相同的策术会失败: + ```leantac {{#example_in Examples/DependentTypes/DB.lean notDone}} ``` ```output error {{#example_out Examples/DependentTypes/DB.lean notDone}} ``` + + + +以 `unsolved goals` 开头的错误描述了策术未能完全构建它们应该构建的表达式。 +在 Lean 的策略语言中,**证明目标(goal)** 是策术需要通过构造适当的表达式来实现的类型。 +在这种情形下,`constructor` 导致应用 `Subschema.cons`,两个目标表示 `cons` 期望的两个参数。 +添加另一个 `constructor` 实例导致第一个目标(`HasCol peak \"location\" DBType.string`)被 `HasCol.there` 处理,因为 `peak` 的第一列不是 `"location"`: + ```leantac {{#example_in Examples/DependentTypes/DB.lean notDone2}} ``` ```output error {{#example_out Examples/DependentTypes/DB.lean notDone2}} ``` + + + +然而,添加第三个 `constructor` 解决了第一个证明目标,因为 `HasCol.here` 是适用的: + ```leantac {{#example_in Examples/DependentTypes/DB.lean notDone3}} ``` ```output error {{#example_out Examples/DependentTypes/DB.lean notDone3}} ``` + + + +第四个 `constructor` 实例解决了 `Subschema peak []` 目标: + ```leantac {{#example_decl Examples/DependentTypes/DB.lean notDone4}} ``` + + + +事实上,一个没有使用策术的版本有四个构造子: + ```lean {{#example_decl Examples/DependentTypes/DB.lean notDone5}} ``` + + +不要尝试找到写 `constructor` 的正确次数,可以使用 `repeat` 策术要求 Lean 只要取得进展就继续尝试 `constructor`: + ```leantac {{#example_decl Examples/DependentTypes/DB.lean notDone6}} ``` + + + +这个更灵活的版本也适用于更有趣的 `Subschema` 问题: + ```leantac {{#example_decl Examples/DependentTypes/DB.lean subschemata}} ``` + + +盲目尝试构造子直到某个符合预期类型的值被构造出来的方法对于 `Nat` 或 `List Bool` 这样的类型并不是很有用。 +毕竟,一个表达式的类型是 `Nat` 并不意味着它是 **正确的** `Nat`。 +但 `HasCol` 和 `Subschema` 这样的类型受到索引的约束, +只有一个构造子适用。 +这意味着程序本身是平凡的,计算机可以选择正确的构造子。 + + +如果一个数据库模式是另一个数据库模式的子数据库模式,那么它也是扩展了一个额外列的更大数据库模式的子数据库模式。 +这个事实被下列函数定义表示出来。 +`Subschema.addColumn` 接受 `smaller` 是 `bigger` 的子数据库模式的证据,然后返回 `smaller` 是 `c :: bigger` 的子数据库模式的证据,即,`bigger` 增加了一个额外列: + ```lean {{#example_decl Examples/DependentTypes/DB.lean SubschemaAdd}} ``` + + + +子数据库模式描述了在大数据库模式中找到小数据库模式的每一列的位置。 +`Subschema.addColumn` 必须将这些描述从指向原始的大数据库模式转换为指向扩展后的更大数据库模式。 +在 `nil` 的情形下,小数据库模式是 `[]`,`nil` 也是 `[]` 是 `c :: bigger` 的子数据库模式的证据。 +在 `cons` 的情形下,它描述了如何将 `smaller` 中的一列放入 `larger`,需要使用 `there` 调整列的放置位置以考虑新列 `c`,递归调用调整其余列。 + + +另一个思考 `Subschema` 的方式是它定义了两个数据库模式之间的 **关系** —— 存在一个类型为 `Subschema bigger smaller` 的表达式意味着 `(bigger, smaller)` 在这个关系中。 +这个关系是自反的,意味着每个数据库模式都是自己的子数据库模式: + ```lean {{#example_decl Examples/DependentTypes/DB.lean SubschemaSame}} ``` - + + +### 投影行 + +给定 `s'` 是 `s` 的子数据库模式的证据,可以将 `s` 中的行投影到 `s'` 中的行。 +这是通过分析 `s'` 是 `s` 的子数据库模式的证据完成的:它解释了 `s'` 的每一列在 `s` 中的位置。 +在 `s'` 中的新行是通过从旧行的适当位置检索值逐列构建的。 + + + +执行这种投影的函数 `Row.project` 有三种情形,分别对应于 `Row` 本身的三种情形。 +它使用 `Row.get` 与 `Subschema` 参数中的每个 `HasCol` 一起构造投影行: + ```lean {{#example_decl Examples/DependentTypes/DB.lean RowProj}} ``` - + + +## 条件和选取 + +投影从表中删除不需要的列,但查询也必须能够删除不需要的行。 +这个操作称为 **选择(selection)**。 +选择的前提是有一种表达“哪些行是需要的”的方式。 + + + +示例查询语言包含表达式,类似于 SQL 中可以写在 `WHERE` 子句中的内容。 +表达式由索引族 `DBExpr` 表示。 +表达式可以引用数据库中的列,但不同的子表达式都有相同的数据库模式。`DBExpr` 以数据库模式作为参量。 +此外,每个表达式都有一个类型,这些类型不同,所以这是一个索引: + ```lean {{#example_decl Examples/DependentTypes/DB.lean DBExpr}} ``` + + + +`col` 构造子表示对数据库中的列的引用。 +`eq` 构造子比较两个表达式是否相等,`lt` 检查一个是否小于另一个,`and` 是布尔合取,`const` 是某种类型的常量值。 + + +例如,在 `peak` 中检查 `elevation` 列的值大于 1000 并且位置等于 `"Denmark"` 的表达式可以写为: + ```leantac {{#example_decl Examples/DependentTypes/DB.lean tallDk}} ``` + + + +这有点复杂。 +特别是,对列的引用包含了重复的对 `by repeat constructor` 的调用。 +Lean 的一个特性叫做 **宏(macro)**,可以消除这些重复代码,使表达式更易于阅读: + ```leantac {{#example_decl Examples/DependentTypes/DB.lean cBang}} ``` + + + +这个声明为 Lean 添加了 `c!` 关键字,并指示 Lean 用相应的 `DBExpr.col` 构造替换后面跟着的任何 `c!` 实例。 +这里,`term` 代表 Lean 表达式,而不是命令、策术或语言的其他部分。 +Lean 宏有点像 C 预处理器宏,只是它们更好地集成到语言中,并且它们自动避免了 CPP 的一些陷阱。 +事实上,它们与 Scheme 和 Racket 中的宏非常密切相关。 + + +有了这个宏,表达式就容易阅读得多: + ```lean {{#example_decl Examples/DependentTypes/DB.lean tallDkBetter}} ``` + + +求某行在一个表达式下的值包括对表达式中的 `.col` 调用 `Row.get` 提取列引用,其他构造子则委托给 Lean 中对应的运算进行处理: + ```lean {{#example_decl Examples/DependentTypes/DB.lean DBExprEval}} ``` + + +对 Valby Bakke,哥本哈根地区最高的山,求值得到 `false`,因为 Valby Bakke 的海拔远低于 1 km: + ```lean {{#example_in Examples/DependentTypes/DB.lean valbybakke}} ``` ```output info {{#example_out Examples/DependentTypes/DB.lean valbybakke}} ``` + + + +对一个海拔 1230 米的虚构的山求值得到 `true`: + ```lean {{#example_in Examples/DependentTypes/DB.lean fakeDkBjerg}} ``` ```output info {{#example_out Examples/DependentTypes/DB.lean fakeDkBjerg}} ``` + + + +为美国爱达荷州最高峰求值得到 `false`,因为爱达荷州不是丹麦的一部分: + ```lean {{#example_in Examples/DependentTypes/DB.lean borah}} ``` @@ -333,8 +753,13 @@ Evaluating it for the highest peak in the US state of Idaho yields `false`, as I {{#example_out Examples/DependentTypes/DB.lean borah}} ``` + + +## 查询 + + +查询语言基于关系代数。 +除了表之外,它还包括以下运算符: + 1. 并,将两个具有相同数据库模式的表达式的查询的结果行合并 + 2. 差,定义在两个具有相同数据库模式的表达式,从第一个表达式的查询结果中删除同时存在于第二个表达式的查询结果的行 + 3. 选择,按照某些标准,根据表达式过滤查询的结果 + 4. 投影,从查询结果中删除列 + 5. 笛卡尔积,将一个查询的每一行与另一个查询的每一行组合 + 6. 重命名,修改查询结果中某一个列的名字 + 7. 添加前缀,为查询中的所有列名添加一个前缀 + + +最后一个运算符不是严格必要的,但它使语言更方便使用。 + + + +查询同样由一个索引族表示: + ```lean {{#example_decl Examples/DependentTypes/DB.lean Query}} ``` + + + +`select` 构造子要求用于选择的表达式返回一个布尔值。 +`product` 构造子的类型包含对 `disjoint` 的调用,它确保两个数据库模式没有相同的列名: + ```lean {{#example_decl Examples/DependentTypes/DB.lean disjoint}} ``` + + + +将 `Bool` 类型的表达式用在期望一个类型的位置会触发从 `Bool` 到 `Prop` 的强制转换。 + +正如可判定命题被视为一个布尔值:命题的证据被强制转换为 `true`,命题的反驳被强制转换为 `false`,布尔值也可以反过来被强制转换为表达式等于 `true` 的命题。 +因为预期所有库的使用将发生在数据库模式已经给定的场景下,所以这个命题可以用 `by simp` 证明。 +类似地,`renameColumn` 构造子检查新名称是否已经存在于数据库模式中。 +它使用辅助函数 `Schema.renameColumn` 来更改 `HasCol` 指向的列的名称: + ```lean {{#example_decl Examples/DependentTypes/DB.lean renameColumn}} ``` + + +## 执行查询 + +执行查询需要一些辅助函数。 +查询的结果是一个表。 +这意味着查询语言中的每个操作都需要一个可以与表一起工作的实现。 + + + +### 笛卡尔积 + + +取两个表的笛卡尔积是通过将第一个表的每一行附加到第二个表的每一行来完成的。 +首先,由于 `Row` 的结构,将一列添加到行中需要对数据库模式进行模式匹配,以确定结果是一个裸值还是一个元组。 +这是一个常见的操作,所以我们将模式匹配提取到一个辅助函数中方便复用: + ```lean {{#example_decl Examples/DependentTypes/DB.lean addVal}} ``` + + + +对两行进行附加需要同时对第一行和它的数据库模式进行递归,因为行的结构与模式的结构是绑定的。 +当第一行为空时,返回第二行。 +当第一行是一个单例时,将值添加到第二行。 +当第一行包含多列时,将第一列的值添加到其余列和第二行附加的递归调用的结果上。 + ```lean {{#example_decl Examples/DependentTypes/DB.lean RowAppend}} ``` + + +`List.flatMap` 接受两个一个函数参数和一个列表,函数对列表中的每一项均会返回一个列表,然后`List.flatMap`按将列表的列表含顺序依次附加: + ```lean {{#example_decl Examples/DependentTypes/DB.lean ListFlatMap}} ``` + + + +类型签名表明 `List.flatMap` 可以用来实现 `Monad List` 实例。 +实际上,与 `pure x := [x]` 一起,`List.flatMap` 确实实现了一个单子。 +然而,这不是一个非常有用的 `Monad` 实例。 +`List` 单子基本上是一个提前探索搜索空间中的 **每一条** 可能路径的 `Many` 单子,尽管用户可能只需要其中的某些值。 +由于这种性能陷阱,通常不建议为 `List` 定义 `Monad` 实例。 +然而查询语言没有限制返回的结果数量的运算符,因此返回所有的组合正是所需要的结果: + ```lean {{#example_decl Examples/DependentTypes/DB.lean TableCartProd}} ``` + + +正如 `List.product` 一样,这个函数也可以通过在恒等单子下使用带变更(mutation)的循环实现: + ```lean {{#example_decl Examples/DependentTypes/DB.lean TableCartProdOther}} ``` - + + +### 差 + + +从表中删除不需要的行可以使用 `List.filter` 完成,它接受一个列表和一个返回 `Bool` 的函数。 +返回一个新列表,这个新列表仅包含旧列表中函数值为 `true` 的条目。 +例如, + ```lean {{#example_in Examples/DependentTypes/DB.lean filterA}} ``` + + + +求值为 + ```lean {{#example_out Examples/DependentTypes/DB.lean filterA}} ``` + + + +因为 `"Columbia"` 和 `"Sandy"` 的长度小于或等于 `8`。 +可以使用辅助函数 `List.without` 删除表的条目: + ```lean {{#example_decl Examples/DependentTypes/DB.lean ListWithout}} ``` + + +这个将在执行查询时与 `Row` 的 `BEq` 实例一起使用。 + + + +### 重命名 + + +在一行数据中重命名一个列需要使用一个递归函数遍历整行直到找到需要重命名的列, +然后将用一个新名字指向该列,而值仍然为这列原有的值: + ```lean {{#example_decl Examples/DependentTypes/DB.lean renameRow}} ``` + + +这个函数改变了其参数的 **类型**,但实际返回的数据完全相同。 +从运行时的角度看,`renameRow` 只是一个拖慢运行的恒等函数。 +这暗示了使用索引族进行编程时的一个常见问题,当性能很重要时,这种操作可能会造成不必要的性能损失。 +需要非常小心,但通常很脆弱的设计来消除这种 **重新索引** 函数。 + + + +### 添加前缀 + + +添加前缀与重命名列非常相似。 +然而`prefixRow` 必须处理所有列,而非找到一个特定的列然后直接返回: + ```lean {{#example_decl Examples/DependentTypes/DB.lean prefixRow}} ``` + + + +这个可以与 `List.map` 一起使用,以便为表中的所有行添加前缀。 +和重命名函数一样,这个函数只改变一个值的类型,但不改变值本身。 + + +### 将所有东西组合在一起 + + +定义了所有这些辅助函数后,执行查询只需要一个简短的递归函数: + ```lean {{#example_decl Examples/DependentTypes/DB.lean QueryExec}} ``` + + +构造子的一些参数在执行过程中没有被用到。 +特别是,构造器 `project` 和函数 `Row.project` 都将较小的数据库模式作为显式参数,但表明这个数据库模式是较大数据库模式的子数据库模式的 **证据** 的类型包含足够的信息,以便 Lean 自动填充参数。 +类似地,`product` 构造子要求两个表具有不同的列名,但 `Table.cartesianProduct` 不需要。 +一般来说,依值类型编程中让 Lean 可以代替程序员自己填写很多参数。 + + + +对查询的结果使用点符号(dot notation)以调用在 `Table` 和 `List` 命名空间中定义的函数,如 `List.map`、`List.filter` 和 `Table.cartesianProduct`。 +因为 `Table` 是使用 `abbrev` 定义的,所以这样做是可行的。 +就像类型类搜索一样,点符号可以看穿使用 `abbrev` 创建的定义。 + + +`select`的实现也非常简洁。 +在执行查询 `q` 后,使用 `List.filter` 删除不满足表达式的行。 +`filter` 需要一个从 `Row s` 到 `Bool` 的函数作为参数,但 `DBExpr.evaluate` 的类型是 `Row s → DBExpr s t → t.asType`。 +但这并不会产生类型错误,因为 `select` 构造器的类型要求表达式的类型为 `DBExpr s .bool`,所以 `t.asType` 实际上就是 `Bool`。 + + +一个找到所有海拔高于 500 米的山峰的高度的查询可以写成: + ```leantac {{#example_decl Examples/DependentTypes/DB.lean Query1}} ``` + + +执行它返回预期的整数列表: + ```lean {{#example_in Examples/DependentTypes/DB.lean Query1Exec}} ``` @@ -478,12 +1096,24 @@ Executing it returns the expected list of integers: {{#example_out Examples/DependentTypes/DB.lean Query1Exec}} ``` + + +为了规划一个观光旅行,可能需要同一位置的所有山和瀑布的有序对。 +这可以通过取两个表的笛卡尔积,选择它们 `location` 相等的行,然后投影出山和瀑布的名称来完成: + ```leantac {{#example_decl Examples/DependentTypes/DB.lean Query2}} ``` + + + +因为示例数据只包括美国的瀑布,执行查询返回美国的山和瀑布有序对: + ```lean {{#example_in Examples/DependentTypes/DB.lean Query2Exec}} ``` @@ -491,41 +1121,94 @@ Because the example data includes only waterfalls in the USA, executing the quer {{#example_out Examples/DependentTypes/DB.lean Query2Exec}} ``` + +### 可能遇到的错误 + + + +很多潜在的错误都被 `Query` 的定义排除了。 +例如,忘记在 `"mountain.location"` 中添加限定符会导致编译时错误,突出显示列引用 `c! "location"`: + ```leantac {{#example_in Examples/DependentTypes/DB.lean QueryOops1}} ``` + + +这是一个很棒的反馈! +但是,很难从这个错误信息知道下面应该做什么: ```output error {{#example_out Examples/DependentTypes/DB.lean QueryOops1}} ``` + + +类似地,忘记为两个表的名称添加前缀会导致 `by simp` 上的错误,它应该提供证据表明数据库模式实际上是不同的; + ```leantac {{#example_in Examples/DependentTypes/DB.lean QueryOops2}} ``` + + + +然而,错误信息同样没有帮助: ```output error {{#example_out Examples/DependentTypes/DB.lean QueryOops2}} ``` + + +Lean 的宏系统不仅可以为查询提供方便的语法,还可以生成的错误信息变得有用。 +不幸的是,本书的范围不包括如何使用 Lean 的宏实现语言。 +像 `Query` 这样的索引族可能最适合作为一个有类型的数据库交互库的核心,直接暴露给用户的接口。 + +## 练习 + + + +### 日期 + + +定义一个用来表示日期的结构。将其添加到 `DBType` 宇宙中,并相应地更新其余代码。 +定义必要的额外的 `DBExpr` 构造子。 + +### 可空类型 + + + +通过以下结构表示数据库类型,为查询语言添加对可空列的支持: + ```lean structure NDBType where underlying : DBType @@ -538,11 +1221,23 @@ abbrev NDBType.asType (t : NDBType) : Type := t.underlying.asType ``` + +在 `Column` 和 `DBExpr` 中使用这种类型代替 `DBType`,并查找 SQL 的 `NULL` 和比较运算符的规则,以确定 `DBExpr` 构造子的类型。 + + + +### 尝试策术 + + +在 Lean 中使用 `by repeat constructor` 观察 Lean 为以下类型找到了什么值,并解释每个结果。 * `Nat` * `List Nat` * `Vect Nat 4` diff --git a/functional-programming-lean/src/dependent-types/universe-pattern.md b/functional-programming-lean/src/dependent-types/universe-pattern.md index e6adacf..4bc4e0e 100644 --- a/functional-programming-lean/src/dependent-types/universe-pattern.md +++ b/functional-programming-lean/src/dependent-types/universe-pattern.md @@ -1,152 +1,344 @@ -# The Universe Design Pattern + +# 宇宙设计模式 + + + +在 Lean 中,用于分类其他类型的类型被称为宇宙,如 `Type`、`Type 3` 和 `Prop` 等。 +然而, **宇宙(universe)** 也用于表示一种设计模式:使用数据类型来表示 Lean 类型的子集,并通过一个解释函数将数据类型的构造子映射为实际类型。 +这种数据类型的值被称为其映射到的类型的 **编码(codes)**。 + + +尽管实现方式不同。使用这种设计模式实现的宇宙是一组类型的类型,与 Lean 内置的宇宙具有相同的含义。 +在 Lean 中,`Type`、`Type 3` 和 `Prop` 等类型直接描述其他类型的类型。 +这种方式被称为 **Russell 风格的宇宙(universes à la Russell)**。 +本节中描述的用户定义的宇宙将所有其包含的类型表示为 **数据**,并用一个显式的函数将这些编码映射到实际的类型。 +这种方式被称为 **Tarski 风格的宇宙(universes à la Tarski)**。 +基于依值类型理论的语言(如 Lean)几乎总是使用 Russell 风格的宇宙,而 Tarski 风格的宇宙是这些语言中定义 API 的有用模式。 + + +自定义宇宙使得我们可以划分出一组可以与 API 一起使用的类型的封闭集合。 +因为这个集合是封闭的,因此只需要对编码的递归就能使程序适用于该宇宙中的 **任何** 类型。 +下面是一个自定义宇宙的例子。它包括具有编码 `nat` 和 `bool` 的数据类型,和一个解释函数将`nat` 映射到 `Nat`, `bool` 映射到 `Bool`: + ```lean {{#example_decl Examples/DependentTypes/Finite.lean NatOrBool}} ``` + + + +对编码进行模式匹配允许类型被细化,就像对 `Vect` 的值进行模式匹配会细化其长度一样。 +例如,一个从字符串反序列化此宇宙中的类型的值的程序如下: + ```lean {{#example_decl Examples/DependentTypes/Finite.lean decode}} ``` -Dependent pattern matching on `t` allows the expected result type `t.asType` to be respectively refined to `NatOrBool.nat.asType` and `NatOrBool.bool.asType`, and these compute to the actual types `Nat` and `Bool`. + + +对 `t` 进行依值模式匹配允许将期望的结果类型 `t.asType` 分别细化为 `NatOrBool.nat.asType` 和 `NatOrBool.bool.asType`,并且这些计算为实际的类型 `Nat` 和 `Bool`。 + + + +与任何其他数据一样,编码可能是递归的。 +类型 `NestedPairs` 编码了任意嵌套的自然数有序对: + ```lean {{#example_decl Examples/DependentTypes/Finite.lean NestedPairs}} ``` + + + +解释函数 `NestedPairs.asType` 是递归定义的。 +这意味着需要对编码进行递归才能实现该宇宙的 `BEq`: + ```lean {{#example_decl Examples/DependentTypes/Finite.lean NestedPairsbeq}} ``` + + +尽管 `NestedPairs` 宇宙中的每种类型已经有一个 `BEq` 实例,但类型类的搜索不会在实例声明中自动检查数据类型的所有情形,因为这样的情形可能有无限多种,就像 `NestedPairs` 一样。 +试图让 Lean 直接给出该类型的 `BEq` 实例会导致错误。需要通过对编码进行递归来向 Lean 解释如何找到这样的实例。 + ```lean {{#example_in Examples/DependentTypes/Finite.lean beqNoCases}} ``` ```output error {{#example_out Examples/DependentTypes/Finite.lean beqNoCases}} ``` -The `t` in the error message stands for an unknown value of type `NestedPairs`. -## Type Classes vs Universes + +错误信息中的 `t` 代表类型 `NestedPairs` 的未知值。 + + + +## 类型类 vs 宇宙 + + +类型类使得 API 可以被用在任何类型上,只要这些类型实现了必要的接口。 +在大多数情况下,这是更合适的做法,因为很难提前预测 API 的所有用例。 +类型类允许库代码被原始作者预期之外的更多类型使用。 + + + +Tarski 风格的宇宙使得 API 仅能用在实现决定好的一组类型上。在一些情况下,这是有用的: + * 当一个函数应该根据传递的类型不同而有非常不同的表现时—无法对类型本身进行模式匹配,但可以对类型的编码进行模式匹配; + * 当外部系统本身就限制了可能提供的数据类型,并且不需要额外的灵活性; + * 当实现某些操作需要类型的一些额外属性时。 -Type classes are useful in many of the same situations as interfaces in Java or C#, while a universe à la Tarski can be useful in cases where a sealed class might be used, but where an ordinary inductive datatype is not usable. + -## A Universe of Finite Types +类型类在 在类似 Java 或 C# 中适合使用接口的场景下更加有用,而 Tarski 风格的宇宙则在类似适合使用封闭类(sealed class)的场景下,且一般的归纳定义数据类型无法使用的情况下更加有用。 + + + +## 一个有限类型的宇宙 + + + +将 API 限制为只能用于给定的类型允许 API 实现通常情况下不可能的操作。 +例如,比较函数是否相等。两个函数相等定义为它们总是将相同的输入映射到相同的输出时。 +检查这一点可能需要无限长的时间,例如比较两个类型为 `Nat → Bool` 的函数需要检查函数对每个 `Nat` 返回相同的 `Bool`。 + + +换句话说,参数类型为无限类型的函数本身也是无限类型。 +函数可以被视为表格,参数类型为无限类型的函数需要无限多行来描述每种情形。 +但来参数类型为限类型的函数只需要有限行,意味着该函数类型也是有限类型。 +如果两个函数的参数类型均为有限类型,则可以通过枚举参数所有的可能性,然后比较它们在所有这些输入下的输出结果来检查它们是否相等。 +检查高阶函数是否相等需要生成给定类型的所有可能函数,此外还需要返回类型是有限的,以便将参数类型的每个元素映射到返回类型的每个元素。 +这不是一种**快速**的方法,但它确实在有限时间内完成。 + + + +表示有限类型的一种方法是定义一个宇宙: -One way to represent finite types is by a universe: ```lean {{#example_decl Examples/DependentTypes/Finite.lean Finite}} ``` -In this universe, the constructor `arr` stands for the function type, which is written with an `arr`ow. + + +在这个宇宙中,构造子 `arr` 表示函数类型(因为函数的箭头符号叫做 `arr` ow)。 + + + +比较这个宇宙中的两个值是否相等与 `NestedPairs` 宇宙中几乎相同。 +唯一重要的区别是增加了 `arr` 的情形,它使用一个名为 `Finite.enumerate` 的辅助函数来生成由 `t1` 编码的类型的每个值,然后检查两个函数对每个可能的输入返回相同的结果: + ```lean {{#example_decl Examples/DependentTypes/Finite.lean FiniteBeq}} ``` + + + +标准库函数 `List.all` 检查提供的函数在列表的每个条目上返回 `true`。 +这个函数可以用来比较布尔值上的函数是否相等: + ```lean {{#example_in Examples/DependentTypes/Finite.lean arrBoolBoolEq}} ``` ```output info {{#example_out Examples/DependentTypes/Finite.lean arrBoolBoolEq}} ``` -It can also be used to compare functions from the standard library: + + + +它也可以用来比较标准库中的函数: + ```lean {{#example_in Examples/DependentTypes/Finite.lean arrBoolBoolEq2}} ``` ```output info {{#example_out Examples/DependentTypes/Finite.lean arrBoolBoolEq2}} ``` -It can even compare functions built using tools such as function composition: + + + +它甚至可以比较使用函数复合等工具构建的函数: + ```lean {{#example_in Examples/DependentTypes/Finite.lean arrBoolBoolEq3}} ``` ```output info {{#example_out Examples/DependentTypes/Finite.lean arrBoolBoolEq3}} ``` -This is because the `Finite` universe codes for Lean's _actual_ function type, not a special analogue created by the library. -The implementation of `enumerate` is also by recursion on the codes from `Finite`. + + +这是因为 `Finite` 宇宙编码了 Lean 的**实际**函数类型,而非某些特殊的近似。 + + + +`enumerate` 的实现也是通过对 `Finite` 的编码进行递归。 + ```lean {{#include ../../../examples/Examples/DependentTypes/Finite.lean:FiniteAll}} ``` + + + +`Unit` 只有一个值。`Bool` 有两个值(`true` 和 `false`)。 +有序对的值则是 `t1` 编码的类型的值和 `t2` 编码的类型的值的笛卡尔积。换句话说,`t1` 的每个值都应该与 `t2` 的每个值配对。 辅助函数 `List.product` 可以用普通的递归函数编写,但这里恒等单子中定义`for`实现: + ```lean {{#example_decl Examples/DependentTypes/Finite.lean ListProduct}} ``` -Finally, the case of `Finite.enumerate` for functions delegates to a helper called `Finite.functions` that takes a list of all of the return values to target as an argument. + + +最后,`Finite.enumerate` 将对函数的情形的处理委托给一个名为 `Finite.functions` 的辅助函数,该函数将返回类型的所有值的列表作为参数。 + + + +简单来说,生成从某个有限类型到结果的值的所有函数可以被认为是生成函数的表格。 +每个函数将一个输出分配给每个输入,这意味着当有 \\( k \\) 个可能的参数时,给定函数的表格有 \\( k \\) 行。 +因为表格的每一行都可以选择 \\( n \\) 个可能的输出中的任何一个,所以有 \\( n ^ k \\) 个潜在的函数要生成。 + + + +与之前类似,生成从有限类型到一些值列表的函数是通过对描述有限类型的编码进行递归完成的: -Once again, generating the functions from a finite type to some list of values is recursive on the code that describes the finite type: ```lean {{#include ../../../examples/Examples/DependentTypes/Finite.lean:FiniteFunctionSigStart}} ``` + + +`Unit` 的函数表格包含一行,因为函数不能根据提供的输入选择不同的结果。 +这意味着为每个潜在的输入生成一个函数。 + + ```lean {{#include ../../../examples/Examples/DependentTypes/Finite.lean:FiniteFunctionUnit}} ``` -There are \\( n^2 \\) functions from `Bool` when there are \\( n \\) result values, because each individual function of type `Bool → α` uses the `Bool` to select between two particular `α`s: + + + +从 `Bool` 到 \\( n \\) 个结果值时,有 \\( n^2 \\) 个函数,因为类型 `Bool → α` 的每个函数根据 `Bool` 选择两个特定的 `α` : + ```lean {{#include ../../../examples/Examples/DependentTypes/Finite.lean:FiniteFunctionBool}} ``` + + + +从有序对中生成函数可以通过利用柯里化来实现:把这个函数转化为一个接受有序对的第一个元素并返回一个等待有序对的第二个元素的函数。 +这样做允许在这种情形下递归使用 `Finite.functions`: + ```lean {{#include ../../../examples/Examples/DependentTypes/Finite.lean:FiniteFunctionPair}} ``` + + +生成高阶函数有点烧脑。 +一个函数可以根据其输入/输出行为与其他函数区分开来。 +高阶函数的输入行为则又依赖于其函数参数的输入/输出行为: +因此高阶函数的所有行为可以表示为将函数参数应用于所有它所有可能的输入值,然后根据该函数应用的结果的不同产生不同的行为。 +这提供了一种构造高阶函数的方法: + * 构造参数函数 `t1 → t2` 的参数 `t1` 的所有可能值。 + * 对于每个可能的值,构造可以由应用参数函数到可能的参数的观察结果产生的所有可能行为。 + 这可以使用 `Finite.functions` 和对其余参数的递归来完成,因为递归的结果表示基于其余可能参数的观察的函数。`Finite.functions` 根据当前对参数的观察构造所有实现这些方式的方法。 + * 对基于每个观察结果的潜在行为,构造一个将函数参数应用于当前可能参数的高阶函数。然后将此结果传递给观察行为。 + * 递归的基情形是对每个结果值观察无事可做的高阶函数——它忽略函数参数,只是返回结果值。 + + + +直接定义这个递归函数导致 Lean 无法证明整个函数终止。 +然而,一种更简单的递归形式,**右折叠(right fold)**,可以让终止检查器明确地知道函数终止。 +右折叠接受三个参数:(1)步骤函数,它将列表的头与对尾部的递归得到的结果组合在一起;(2)列表为空时的默认值;(3)需要处理的列表。 +这个函数会分析列表,将列表中的每个 `::` 替换为对步骤函数的调用,并将 `[]` 替换为默认值: + ```lean {{#example_decl Examples/DependentTypes/Finite.lean foldr}} ``` -Finding the sum of the `Nat`s in a list can be done with `foldr`: + + + +可以使用 `foldr` 求出列表中 `Nat` 的和: + ```lean {{#example_eval Examples/DependentTypes/Finite.lean foldrSum}} ``` -With `foldr`, the higher-order functions can be created as follows: + + +使用 `foldr`,可以创建如下的高阶函数: + ```lean {{#include ../../../examples/Examples/DependentTypes/Finite.lean:FiniteFunctionArr}} ``` -The complete definition of `Finite.Functions` is: + + + +`Finite.Functions` 的完整定义是: + ```lean {{#include ../../../examples/Examples/DependentTypes/Finite.lean:FiniteFunctions}} ``` + +因为 `Finite.enumerate` 和 `Finite.functions` 互相调用,它们必须在一个 `mutual` 块中定义。 +换句话说,在 `Finite.enumerate` 的定义前需要加入 `mutual` 关键字: -Because `Finite.enumerate` and `Finite.functions` call each other, they must be defined in a `mutual` block. -In other words, right before the definition of `Finite.enumerate` is the `mutual` keyword: ```lean {{#include ../../../examples/Examples/DependentTypes/Finite.lean:MutualStart}} ``` @@ -190,6 +424,7 @@ and right after the definition of `Finite.functions` is the `end` keyword: {{#include ../../../examples/Examples/DependentTypes/Finite.lean:MutualEnd}} ``` + + +这种比较函数的算法并不特别实用。 +要检查的情形数量呈指数增长;即使是一个简单的类型,如 `((Bool × Bool) → Bool) → Bool`,也描述了 {{#example_out Examples/DependentTypes/Finite.lean nestedFunLength}} 个不同的函数。 +为什么会有这么多? +根据上面的推理,并使用 \\( \\left| T \\right| \\) 表示类型 \\( T \\) 描述的值的数量,那么上述函数的值的数量应该为 + +\\[ \\left| \\left( \\left( \\mathtt{Bool} \\times \\mathtt{Bool} \\right) \\rightarrow \\mathtt{Bool} \\right) \\rightarrow \\mathtt{Bool} \\right| \\]。 + +这个值可以一步步化简为 + +\\[ \\left|\\mathrm{Bool}\\right|^{\\left| \\left( \\mathtt{Bool} \\times \\mathtt{Bool} \\right) \\rightarrow \\mathtt{Bool} \\right| }, \\] + +\\[ 2^{2^{\\left| \\mathtt{Bool} \\times \\mathtt{Bool} \\right| }}, \\] + +\\[ 2^{2^4} \\] + +65536 + +指数的嵌套会很快地增长。这样的高阶函数还有很多。 + -## Exercises +## 练习 + + * 编写一个函数,将由 `Finite` 编码的类型的值转换为字符串。函数应该以表格的方式表示。 + * 将空类型 `Empty` 添加到 `Finite` 和 `Finite.beq`。 + * 将 `Option` 添加到 `Finite` 和 `Finite.beq`。