索引族

多态归纳类型接受类型参数。例如，List 接受一个类型参数以决定列表中条目的类型，而 Except 接受两个类型参数以决定异常或值的类型。这些在数据类型的每个构造子中都一致的类型参数，被称为 参量（parameters)。

然而，归纳类型中每个构造子的接受的类型参数并不一定要相同。这种不同构造子可以接受不同类型作为参数的归纳类型被称为 索引族（indexed families)，而这些不同的参数被称为 索引（indices)。索引族最为人熟知的例子是**向量（vectors)**类型：这个类型类似列表类型，但它除了包含列表中元素的类型，还包含列表的长度。这种类型在 Lean 中的定义如下：

inductive Vect (α : Type u) : Nat → Type u where
   | nil : Vect α 0
   | cons : α → Vect α n → Vect α (n + 1)

函数声明可以在冒号之前接受一些参数，表示这些参数在整个定义中都是可用的，也可以在冒号之后接受一些参数，函数会对它们进行模式匹配，并根据不同情形定义不同的函数体。归纳数据类型也有类似的原则：以 Vect 为例，在其顶部的数据类型声明中，参数 α 出现在冒号之前，表示它是一个必须提供的参量，而在冒号之后出现的 Nat 参数表示它是一个索引，（在不同的构造子中）可以变化。事实上，在 nil 和 cons 构造子的声明中，三个出现 Vect 的地方都将 α 作为第一个参数提供，而第二个参数在每种情形下都不同。

nil 构造子的声明表明它的类型是 Vect α 0。这意味着在期望 Vect String 3 的上下文中使用 Vect.nil 会导致类型错误，就像在期望 List String 的上下文中使用 [1, 2, 3] 一样：

example : Vect String 3 := Vect.nil

type mismatch
  Vect.nil
has type
  Vect String 0 : Type
but is expected to have type
  Vect String 3 : Type

在这个例子中，0 和 3 之间的不匹配和其他例子中类型的不匹配是一模一样的情况，尽管 0 和 3 本身并不是类型。

类型族被称为 族（families)，因为不同的索引值意味着可以使用的构造子不同。在某种意义上，一个索引族并不是一个类型；它更像是一组相关的类型的集合，不同索引的值对应了这个集合中的一个类型。选择索引 5 作为 Vect 的索引意味着只有 cons 构造子可用，而选择索引 0 意味着只有 nil 构造子可用。

如果索引是一个未知的量（例如，一个变量），那么在它变得已知之前，任何构造子都不能被使用。如果一个 Vect 的长度为 n，那么 Vect.nil 和 Vect.cons 都无法被用来构造这个类型，因为无法知道变量 n 作为一个 Nat 应该匹配 0 或 n + 1：

example : Vect String n := Vect.nil

type mismatch
  Vect.nil
has type
  Vect String 0 : Type
but is expected to have type
  Vect String n : Type

example : Vect String n := Vect.cons "Hello" (Vect.cons "world" Vect.nil)

type mismatch
  Vect.cons "Hello" (Vect.cons "world" Vect.nil)
has type
  Vect String (0 + 1 + 1) : Type
but is expected to have type
  Vect String n : Type

让列表的长度作为类型的一部分意味着类型具有更多的信息。例如 Vect.replicate 是一个创建包含某个值（x）的特定份数 (n) 副本的 Vect 的函数。可以精确地表示这一点的类型是：

def Vect.replicate (n : Nat) (x : α) : Vect α n := _

参数 n 出现在结果的类型的长度中。以下消息描述了下划线占位符对应的任务：

don't know how to synthesize placeholder
context:
α : Type u_1
n : Nat
x : α
⊢ Vect α n

当编写使用索引族的程序时时，只有当 Lean 能够确定构造子的索引与期望类型中的索引匹配时，才能使用该构造子。然而，两个构造子的索引与 n 均不匹配——nil 匹配 Nat.zero，而 cons 匹配 Nat.succ。就像在上面的类型错误示例中的情况一样，变量 n 可能代表其中一个，取决于具体调用函数时 Nat 参数的值。解决这一问题的方案是利用模式匹配来同时考虑两种情形：

def Vect.replicate (n : Nat) (x : α) : Vect α n :=
  match n with
  | 0 => _
  | k + 1 => _

因为 n 出现在期望的类型中，对 n 进行模式匹配会在匹配的两种情形下 细化（refine) 期望的类型。在第一个下划线中，期望的类型变成了 Vect α 0：

don't know how to synthesize placeholder
context:
α : Type u_1
n : Nat
x : α
⊢ Vect α 0

在第二个下划线中，它变成了 Vect α (k + 1)：

don't know how to synthesize placeholder
context:
α : Type u_1
n : Nat
x : α
k : Nat
⊢ Vect α (k + 1)

当模式匹配不仅发现值的结构，还细化程序的类型时，这种模式匹配被称为 依值模式匹配（dependent pattern matching)。

细化后的类型允许我们使用对应的构造子。第一个下划线匹配 Vect.nil，而第二个下划线匹配 Vect.cons：

def Vect.replicate (n : Nat) (x : α) : Vect α n :=
  match n with
  | 0 => .nil
  | k + 1 => .cons _ _

.cons 下的第一个下划线应该是一个具有类型 α 的值。恰好我们有这么一个值：x。

don't know how to synthesize placeholder
context:
α : Type u_1
n : Nat
x : α
k : Nat
⊢ α

第二个下划线应该是一个具有类型 Vect α k 的值。这个值可以通过对 replicate 的递归调用产生：

don't know how to synthesize placeholder
context:
α : Type u_1
n : Nat
x : α
k : Nat
⊢ Vect α k

下面是 replicate 的最终定义：

def Vect.replicate (n : Nat) (x : α) : Vect α n :=
  match n with
  | 0 => .nil
  | k + 1 => .cons x (replicate k x)

除了在编写函数时提供帮助之外，Vect.replicate 的类型信息还允许调用方不必阅读源代码就明白它一定不是某些错误的实现。一个可能会产生错误长度的列表的 replicate 实现如下：

def List.replicate (n : Nat) (x : α) : List α :=
  match n with
  | 0 => []
  | k + 1 => x :: x :: replicate k x

然而，在实现 Vect.replicate 时犯下同样的错误会引发一个类型错误：

def Vect.replicate (n : Nat) (x : α) : Vect α n :=
  match n with
  | 0 => .nil
  | k + 1 => .cons x (.cons x (replicate k x))

application type mismatch
  cons x (cons x (replicate k x))
argument
  cons x (replicate k x)
has type
  Vect α (k + 1) : Type ?u.1998
but is expected to have type
  Vect α k : Type ?u.1998

List.zip 函数通过将两个列表中对应的项配对（第一个列表中的第一项和第二个列表的第一项，第一个列表中的第二项和第二个列表的第二项, ……）来合并两个列表。这个函数可以用来将一个包含美国俄勒冈州前三座最高峰的列表和一个包含丹麦前三座最高峰的列表合并：

["Mount Hood",
 "Mount Jefferson",
 "South Sister"].zip ["Møllehøj", "Yding Skovhøj", "Ejer Bavnehøj"]

The result is a list of three pairs:

[("Mount Hood", "Møllehøj"),
 ("Mount Jefferson", "Yding Skovhøj"),
 ("South Sister", "Ejer Bavnehøj")]

当列表的长度不同时，结果应该如何呢？与许多其他语言一样，Lean 选择忽略长的列表中的额外条目。例如，将一个具有俄勒冈州前五座最高峰的高度的列表与一个具有丹麦前三座最高峰的高度的列表合并会产生一个含有三个有序对的列表。

[3428.8, 3201, 3158.5, 3075, 3064].zip [170.86, 170.77, 170.35]

求值结果为

[(3428.8, 170.86), (3201, 170.77), (3158.5, 170.35)]

这个函数总是返回一个结果，所以它非常易用。但当输入的两个列表意外地具有不同的长度时，一些数据会被悄悄地丢弃。 F# 采用了不同的方法：它的 List.zip 函数在两个列表长度不匹配时抛出异常，如下面 fsi 会话中展示的那样：

> List.zip [3428.8; 3201.0; 3158.5; 3075.0; 3064.0] [170.86; 170.77; 170.35];;

System.ArgumentException: The lists had different lengths.
list2 is 2 elements shorter than list1 (Parameter 'list2')
   at Microsoft.FSharp.Core.DetailedExceptions.invalidArgDifferentListLength[?](String arg1, String arg2, Int32 diff) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/local.fs:line 24
   at Microsoft.FSharp.Primitives.Basics.List.zipToFreshConsTail[a,b](FSharpList`1 cons, FSharpList`1 xs1, FSharpList`1 xs2) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/local.fs:line 918
   at Microsoft.FSharp.Primitives.Basics.List.zip[T1,T2](FSharpList`1 xs1, FSharpList`1 xs2) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/local.fs:line 929
   at Microsoft.FSharp.Collections.ListModule.Zip[T1,T2](FSharpList`1 list1, FSharpList`1 list2) in /builddir/build/BUILD/dotnet-v3.1.424-SDK/src/fsharp.3ef6f0b514198c0bfa6c2c09fefe41a740b024d5/src/fsharp/FSharp.Core/list.fs:line 466
   at <StartupCode$FSI_0006>.$FSI_0006.main@()
Stopped due to error

这种方法避免了数据的意外丢失，但一个输入不正确时直接崩溃的程序并不容易使用。在 Lean 中相似的实现可以在返回值中使用 Option 或 Except 单子，但是为了避免（可能不大的）数据丢失的风险而引入额外的（操作单子的）编程负担又并不太值得。

然而，如果使用 Vect，可以一个 zip 函数，其类型要求两个输入的列表一定具有相同的长度，如下所示：

def Vect.zip : Vect α n → Vect β n → Vect (α × β) n
  | .nil, .nil => .nil
  | .cons x xs, .cons y ys => .cons (x, y) (zip xs ys)

这个定义只需要考虑两个参数都是 Vect.nil 或都是 Vect.cons 的情形。Lean 接受这个定义，而不会像 List 的类似定义那样产生一个“存在缺失情形”的错误：

def List.zip : List α → List β → List (α × β)
  | [], [] => []
  | x :: xs, y :: ys => (x, y) :: zip xs ys

missing cases:
(List.cons _ _), []
[], (List.cons _ _)

这是因为第一个模式匹配中得到的两个构造子，nil 和 cons，细化了类型检查器对长度 n 的知识。当它是 nil 时，类型检查器还可以确定长度是 0，因此第二个模式的唯一可能选择是 nil。当它是 cons 时，类型检查器可以确定长度是 k+1，因此第二个模式的唯一可能选择是 cons。事实上，添加一个同时使用 nil 和 cons 的情形会导致类型错误，因为长度不匹配：

def Vect.zip : Vect α n → Vect β n → Vect (α × β) n
  | .nil, .nil => .nil
  | .nil, .cons y ys => .nil
  | .cons x xs, .cons y ys => .cons (x, y) (zip xs ys)

type mismatch
  Vect.cons y ys
has type
  Vect β (?m.4718 + 1) : Type ?u.4530
but is expected to have type
  Vect β 0 : Type ?u.4530

长度的细化可以通过将 n 变成一个显式参数来观察：

def Vect.zip : (n : Nat) → Vect α n → Vect β n → Vect (α × β) n
  | 0, .nil, .nil => .nil
  | k + 1, .cons x xs, .cons y ys => .cons (x, y) (zip k xs ys)

练习

熟悉使用依值类型编程需要经验，本节的练习非常重要。对于每个练习，尝试看看类型检查器可以捕捉到哪些错误，哪些错误它无法捕捉。请通过实验代码来进行尝试。这也是培养理解错误信息能力的好方法。

仔细检查 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。

定义一个函数 Vect.snoc，它将一个条目添加到 Vect 的末尾。它的类型应该是 Vect α n → α → Vect α (n + 1)，#eval Vect.snoc (.cons "snowy" .nil) "peaks" 应该输出 {{#example_out Examples/ DependentTypes.lean snocSnowy}}。snoc 这个名字是函数式编程常见的习语：将 cons 倒过来写。

定义一个函数 Vect.reverse，它反转一个 Vect 的顺序。

定义一个函数 Vect.drop。它的类型 (n : Nat) → Vect α (k + n) → Vect α k。通过检查 #eval danishPeaks.drop 2 输出 Vect.cons "Ejer Bavnehøj" (Vect.nil) 来验证它是否正确。

定义一个函数 Vect.take。它的类型为 (n : Nat) → Vect α (k + n) → Vect α n。它返回 Vect 中的前 n 个条目。检查它在一个例子上的结果。

Lean 函数式编程

索引族

练习