使用依值类型编程

在大多数静态类型编程语言中，类型世界和程序世界之间有一个明确的界限。 类型和程序有不同的语法，并且它们在不同阶段起作用。 类型通常在编译阶段被使用，以检查程序是否遵守某些不变量。 程序在运行时阶段被使用，以实际执行计算。 当两者互动时，通常是以类型案例运算符的形式，例如instance-of检查或提供类型检查器无法获得的信息的转换运算符，以在运行时验证。 换句话说，这种交互一般是将类型插入程序世界，使得类型具有一些有限的运行时含义。

Lean 并不严格地区分类型和程序。 在 Lean 中，程序可以计算类型，类型可以包含程序。 允许程序出现在类型中使得编译阶段可以使用编程语言全部的计算能力。 允许函数返回类型则使得类型成为编程过程中的一等参与者。

依值类型（Dependent types） 是包含非类型表达式的类型。

def natOrStringThree (b : Bool) : if b then Nat else String :=
  match b with
  | true => (3 : Nat)
  | false => "three"

更多依值类型的例子包括：

• 多态的介绍性段落 中的 posOrNegThree，其中函数的返回类型取决于参数的值。
• OfNat 类型类 中取决于具体的自然数字面量。
• CheckedInput 结构 中依赖于验证发生年份的验证器的例子。
• 子类型 中包含引用特定值的命题。
• 几乎所有有趣的命题都是包含值的类型，因此是依值类型，包括判断 数组索引表示 的有效性的命题，。

依值类型大大增加了类型系统的能力。 根据参数的值的不同返回不同类型的灵活性使得其他类型系统中很难给出类型的程序可以被接受。 同时，依值类型使得类型签名可以表达“函数只能返回特定的值”等概念，使得编译阶段可以检查一些更加严格的不变量。

然而，使用依值类型进行编程是一个非常复杂的问题，需要一些一般函数式编程中不会用到的技能。 依值类型编程中很可能出现“设计了一个复杂类型以表达一个非常细致的规范，但是无法写出满足这个类型的程序”之类的问题。 当然，这些问题也经常会引发对问题的新的理解，从而得到一个更加细化且可以被满足的类型。 虽然本章只是简单介绍使用依值类型编程，但它是一个值得花一整本书专门讨论的深刻主题。