Lean 函数式编程

7.6. 小结🔗

7.6.1. 依值类型

依值类型中，类型包含诸如函数调用和普通数据构造子之类的非类型代码；这会使类型系统的表达能力大幅提升。 根据一个参数的值来计算一个类型的能力，意味着函数的返回类型可以依所提供的参数而变化。 例如，这可用于使数据库查询的结果类型依赖于数据库的模式以及所发出的具体查询，而不需要对查询结果执行任何可能失败的强制转换操作。 当查询发生变化时，运行它所产生的类型也随之变化，从而能够立即提供编译期反馈。

当函数的返回类型依赖于某个值时，用模式匹配分析该值可能导致类型被细化，因为代表某个值的变量会被模式中的构造子替换。 函数的类型签名记录了返回类型依赖于参数值的方式，而模式匹配随后说明了对于每个可能的参数，返回类型如何得到满足。

出现在类型中的普通代码会在类型检查期间运行，不过可能无限循环的 partial 函数不会被调用。 在多数情况下，这种计算遵循 本书最开头 介绍的普通求值规则：表达式会逐步被其值替换，直到找到最终值。 类型检查期间的计算与运行时计算有一个重要区别：类型中的某些值可能是其值尚未知晓的变量。 在这些情况下，模式匹配会“停滞”，并且不会继续，直到或除非某个特定构造子被选择，例如通过模式匹配来选择。 类型层面的计算可以视为一种部分求值：只有程序中已知程度足够高的部分需要被求值，而其他部分则保持不变。

7.6.2. 宇宙模式

使用依值类型时，一种常见模式是将类型系统的某个子集划分出来。 例如，数据库查询库也许能够返回可变长度字符串、定长字符串或处于某些范围内的数，但它绝不会返回函数、用户定义的数据类型或 IO 动作。 可以先定义一个数据类型，其构造子与所期望类型的结构相匹配，然后定义一个函数，将该数据类型中的值解释为真正的类型，由此定义类型系统的一个领域特定子集。 这些构造子称为相关类型的码，而整个模式有时称为 Tarski 风格的宇宙，或者在上下文清楚表明并非指 Type 3 或 Prop 这样的宇宙时，简称为宇宙。

自定义宇宙是为每个相关类型定义带实例的类型类之外的另一种选择。 类型类是可扩展的，但可扩展性并不总是所期望的。 与直接使用类型相比，定义自定义宇宙有若干优点：

  • 可通过对码进行递归，实现适用于该宇宙中任意类型的泛型操作，例如相等性测试和序列化。

  • 外部系统所接受的类型可以被精确表示，而码数据类型的定义本身也可作为对预期内容的文档说明。

  • Lean 的模式匹配完备性检查器确保不会遗漏任何码，而基于类型类的解决方案会把缺失实例的错误推迟到客户代码中。

7.6.3. 带索引的族

数据类型可以接受两种不同的参数：参数在该数据类型的每个构造子中都相同，而索引可以在构造子之间变化。 对于给定的索引选择，只有该数据类型的某些构造子可用。 例如，Vect.nil 仅当长度索引为 0 时可用，而 Vect.cons 仅当长度索引对某个 n 为 n+1 时可用。 虽然参数通常在数据类型声明中写作冒号之前的具名实参，而索引写作冒号之后函数类型中的实参，但 Lean 能够推断冒号之后的某个实参何时被用作参数。

带索引的族允许表达数据之间的复杂关系，并且这些关系全都由编译器检查。 数据类型的不变式可以被直接编码，并且没有任何方式能够违反它们，哪怕是暂时违反也不行。 将数据类型的不变式告知编译器会带来一个重要益处：编译器现在可以告知程序员必须做什么才能满足这些不变式。 策略性地使用编译期错误，尤其是由下划线产生的错误，可以使得部分编程思考过程被转交给 Lean，从而让程序员的心智腾出来关心其他事情。

使用带索引的族编码不变式可能导致困难。 首先，每个不变式都需要自己的数据类型，而该数据类型随后又需要自己的支持库。 毕竟，List.zip 和 Vect.zip 并不能互换。 这可能导致代码重复。 其次，方便地使用带索引的族要求类型中所用函数的递归结构与正在被类型检查的程序的递归结构相匹配。 使用带索引的族进行编程，就是安排恰当巧合发生的技艺。 虽然可以通过诉诸相等性证明来绕过缺失的巧合，但这很困难，并且会导致程序中散布着晦涩的理由说明。 第三，在类型检查期间对大值运行复杂代码可能导致编译期变慢。 对复杂程序避免这些变慢可能需要专门的技术。

7.6.4. 定义相等性与命题相等性

Lean 的类型检查器必须不时检查两个类型是否应被视为可互换。 由于类型可以包含任意程序，因此它必须能够检查任意程序的相等性。 然而，并不存在高效算法能够检查任意程序是否满足完全一般的数学相等性。 为了解决这一问题，Lean 包含两种相等性概念：

  • 定义相等性是相等性的一种欠近似；它本质上检查在计算以及约束变量重命名意义下的语法表示是否相等。在需要定义相等性的情形中，Lean 会自动检查它。

  • 命题相等性必须由程序员显式证明，并且显式调用。作为回报，Lean 会自动检查这些证明是有效的，并且这些调用达成了正确的目标。

这两种相等性概念体现了程序员与 Lean 本身之间的分工。 定义相等性简单但自动，而命题相等性手动但富有表达力。 命题相等性可用于使类型中原本卡住的程序继续推进。

然而，频繁使用命题相等性来使类型层面的计算继续推进，通常是一种代码异味。 这通常意味着巧合没有被良好地工程化；通常更好的做法是重新设计类型和索引，或者使用另一种技术来强制所需的不变式。 相反，当命题相等性用于证明程序满足某个规约，或者作为子类型的一部分时，就不那么值得怀疑。