多态性 Polymorphism

在本章中，我们将继续发展函数式编程的基本概念。关键的新思想是多态性（将函数抽象为它们所操作的数据类型）和高阶函数（将函数视为数据）。我们从多态性开始。

多态列表 Polymorphic Lists

在上一章中，我们一直在处理只包含数字的列表。显然，有趣的程序还需要能够使用其他类型的元素操作列表——布尔列表、列表列表等等。我们可以为每种类型定义一个新的归纳数据类型，例如。。。

Inductive boollist

Inductive boollist : Type :=
  | bool_nil
  | bool_cons (b : bool) (l : boollist).

... 但这很快就会变得单调乏味，部分原因是我们必须为每个数据类型编写不同的构造函数名称，但主要原因是我们还需要为每个新的数据类型定义定义所有列表操作函数（length、rev等）及其所有属性（rev_length、app_assoc等）的新版本。

为了避免所有这些重复，Coq支持多态归纳类型定义。例如，这里有一个多态列表数据类型。

Inductive list

Inductive list (X:Type) : Type :=
  | nil
  | cons (x : X) (l : list X).

这与前一章中的natlist定义完全相同，只是cons构造函数的nat参数已被任意类型X替换，X的绑定已添加到第一行的函数头中，并且构造函数类型中出现的natlist已被列表X替换。

列表本身是什么样的东西？思考这个问题的一个好方法是，列表的定义是从类型到归纳定义的函数；或者，简而言之，list是一个从类型到类型的函数。对于任何特定类型X，类型列表X是归纳定义的列表集，其元素为类型X。

Check list : Type → Type.

列表定义中的X自动成为构造函数nil和cons的参数——也就是说，nil和cons现在是多态构造函数；当我们使用它们时，现在必须提供第一个参数，即它们正在构建的列表的类型。例如，nil nat构造nat类型的空列表。

Check (nil nat) : list nat.

类似地，cons-nat将nat类型的元素添加到list-nat类型的列表中。下面是一个仅包含自然数3的列表的示例。

Check (cons nat 3 (nil nat)) : list nat.

零的类型可能是什么？我们可以从定义中读取类型列表X，但这会忽略作为列表参数的X的绑定。类型→ 列表X没有解释X的含义。（X:类型）→ 列表X更接近。Coq在这种情况下的符号是∀ X：类型，列表X。

Check nil : ∀ X : Type, list X.

类似地，定义中cons的类型类似于X → list X → list X，但使用此约定解释X的含义会导致∀ X, X → list X → list X。

（关于注释的旁注：在.v文件中，“forall”量词用字母表示。在相应的HTML文件中（以及一些IDE显示.v文件的方式，取决于其显示控件的设置），∀ 通常是按照标准的数学“倒A”排版，尽管你仍会在一些地方看到拼写为“forall”的字样。这只是排版的一个怪癖——意思没有区别。）

必须为列表构造函数的每次使用提供类型参数将是相当麻烦的；我们很快就会看到减轻这种注释负担的方法。

Check (cons nat 2 (cons nat 1 (nil nat)))
      : list nat.

现在，我们可以返回到以前编写的所有列表处理函数的多态版本。下面是重复，例如：

Fixpoint repeat

Fixpoint repeat (X : Type) (x : X) (count : nat) : list X :=
  match count with
  | 0 ⇒ nil X
  | S count' ⇒ cons X x (repeat X x count')
  end.

与nil和cons一样，我们可以使用repeat，首先将其应用于类型，然后应用于此类型的元素（以及数字）：

Example test_repeat1 :
  repeat nat 4 2 = cons nat 4 (cons nat 4 (nil nat)).
Proof. reflexivity. Qed.

要使用repeat构建其他类型的列表，我们只需使用适当的类型参数对其进行实例化：

Example test_repeat2 :
  repeat bool false 1 = cons bool false (nil bool).
Proof. reflexivity. Qed.

45: 2 stars, standard (mumble_grumble)

考虑下面两个归纳定义的类型。

Module MumbleGrumble.
Inductive mumble : Type :=
  | a
  | b (x : mumble) (y : nat)
  | c.
Inductive grumble (X:Type) : Type :=
  | d (m : mumble)
  | e (x : X).

对于某些类型的X，以下哪项是grumble X的类型良好的元素？（将是或否添加到每行。）

      - [d (b a 5)]
      - [d mumble (b a 5)]
      - [d bool (b a 5)]
      - [e bool true]
      - [e mumble (b c 0)]
      - [e bool (b c 0)]
      - [c]  *)
(* FILL IN HERE *)
End MumbleGrumble.

类型注释推理 Type Annotation Inference

让我们再次编写repeat的定义，但这次我们不会指定任何参数的类型。Coq还会接受吗？

Fixpoint repeat'

Fixpoint repeat' X x count : list X :=
  match count with
  | 0 ⇒ nil X
  | S count' ⇒ cons X x (repeat' X x count')
  end.

确实会的。让我们看看Coq分配给repeat'的类型：

Check repeat'
: forall X : Type, X -> nat -> list X.
Check repeat
: forall X : Type, X -> nat -> list X.

它的类型与repeat完全相同。Coq能够使用类型推断，根据X、X和count的使用方式推断出它们的类型。例如，由于X被用作cons的参数，它必须是一个类型，因为cons期望一个类型作为它的第一个参数；将计数与0和S匹配意味着它必须是nat；等等

这种功能强大的工具意味着我们不必在任何地方都编写显式类型注释，尽管显式类型注释作为文档和健全性检查仍然非常有用，因此我们将在大部分时间继续使用它们。

类型参数综合 Type Argument Synthesis

要使用多态函数，除了传递其他参数外，还需要传递一个或多个类型。例如，上面repeat函数体中的递归调用必须沿着类型X传递。但是，由于要重复的第二个参数是X的一个元素，因此第一个参数只能是X，这似乎是非常明显的——为什么我们必须显式地编写它？

幸运的是，Coq允许我们避免这种冗余。我们可以写一个"hole" _来代替任何类型的参数，它可以被理解为“请试着自己弄清楚什么属于这里”。更准确地说，当Coq遇到一个 _时，它将尝试统一所有本地可用的信息——所应用函数的类型，其他参数的类型，以及应用程序出现的上下文所期望的类型，以确定应该用什么具体类型来替换。

这听起来可能类似于类型注释推理——事实上，这两个过程依赖于相同的底层机制。而不是简单地忽略函数中某些参数的类型，比如

repeat' X x count : list X :=

我们也可以用孔来替换这些类型

repeat' (X : _) (x : _) (count : _) : list X :=

告诉Coq尝试推断缺失的信息。 使用孔，重复功能可以这样编写：

Fixpoint repeat'' X

Fixpoint repeat'' X x count : list X :=
  match count with
  | 0        => nil _
  | S count' => cons _ x (repeat'' _ x count')
  end.

在这个例子中，我们不需要通过写_ 而不是X来节省很多。但是在很多情况下，击键和可读性的差异是不寻常的。例如，假设我们想写下一个包含数字1、2和3的列表。而不是这个。。。

Definition list123 :=
  cons nat 1 (cons nat 2 (cons nat 3 (nil nat))).

…我们可以用孔来写：

Definition list123' :=
cons _ 1 (cons _ 2 (cons _ 3 (nil _))).

隐式参数 Implicit Arguments

事实上，在大多数情况下，我们可以更进一步，甚至可以通过告诉Coq总是推断给定函数的类型参数来避免编写_。

Arguments指令指定函数（或构造函数）的名称，然后列出要视为隐式的（前导）参数名称，每个名称都用大括号括起来。

Arguments nil {X}.
Arguments cons {X}.
Arguments repeat {X}.

现在，我们根本不必提供类型参数：

Definition list123'' := cons 1 (cons 2 (cons 3 nil)).

或者，我们可以在定义函数本身时将参数声明为隐式的，方法是将其用大括号而不是括号括起来。例如：

Fixpoint repeat''' X

Fixpoint repeat''' {X : Type} (x : X) (count : nat) : list X :=
  match count with
  | 0        => nil
  | S count' => cons x (repeat''' x count')
  end.

（请注意，我们甚至不必为重复“”的递归调用提供类型参数。事实上，提供类型参数是无效的，因为Coq不需要它。）

只要可能，我们将使用后一种样式，但我们将继续为归纳构造函数使用显式参数声明。这样做的原因是，将归纳类型的参数标记为隐式会导致它对类型本身隐式，而不仅仅是对其构造函数隐式。例如，考虑下面的列表类型的替代定义：

Inductive list'

Inductive list' {X:Type} : Type :=
  | nil'
  | cons' (x : X) (l : list').

因为X被声明为整个归纳定义的隐式，包括list本身，我们现在必须只写list，无论我们谈论的是数字列表、布尔值列表还是其他任何东西，而不是list‘nat或list’bool或其他任何东西；这一步太远了。

最后，让我们在新的多态列表上重新实现一些其他标准列表函数。。。

Fixpoint app

Fixpoint app {X : Type} (l1 l2 : list X) : list X :=
  match l1 with
  | nil ⇒ l2
  | cons h t ⇒ cons h (app t l2)
  end.

Fixpoint rev

Fixpoint rev {X:Type} (l:list X) : list X :=
match l with
| nil ⇒ nil
| cons h t ⇒ app (rev t) (cons h nil)
end.

Example test_rev1 :
rev (cons 1 (cons 2 nil)) = (cons 2 (cons 1 nil)).
Proof. reflexivity. Qed.

Example test_rev2:
rev (cons true nil) = cons true nil.
Proof. reflexivity. Qed.

Fixpoint length

Fixpoint length {X : Type} (l : list X) : nat :=
  match l with
  | nil ⇒ 0
  | cons _ l' ⇒ S (length l')
  end.
  
  Example test_length1: length (cons 1 (cons 2 (cons 3 nil))) = 3.
Proof. reflexivity. Qed.

显式提供类型参数 Supplying Type Arguments Explicitly

隐式声明参数的一个小问题是，有时Coq没有足够的本地信息来确定类型参数；在这种情况下，我们需要告诉Coq，我们想在这一次明确给出论点。例如，假设我们这样写：

Fail Definition mynil := nil.

（出现在定义之前的失败限定符可用于任何命令，用于确保该命令在执行时确实失败。如果该命令确实失败，Coq将打印相应的错误消息，但将继续处理文件的其余部分。）

这里，Coq给了我们一个错误，因为它不知道向nil提供什么类型的参数。我们可以通过提供一个显式的类型声明来帮助它（这样Coq在到达nil的“应用程序”时可以获得更多信息）：

Definition mynil : list nat := nil.

或者，我们可以通过在函数名前面加@来强制隐式参数显式。

Check @nil : forall X : Type, list X.

Definition mynil' := @nil nat.

使用参数合成和隐式参数，我们可以像以前一样为列表定义方便的符号。由于我们已经使构造函数类型参数隐式化，Coq将知道在使用符号时自动推断这些参数。

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
                     (at level 60, right associativity).

现在，列表可以按照我们希望的方式编写：

Definition list123''' := [1; 2; 3].

Exercises

46: 2 stars, standard, optional (poly_exercises)

这里有一些简单的练习，就像列表一章中的练习一样，用于练习多态性。完成下面的证明。

Theorem app_nil_r

Theorem app_nil_r : forall (X:Type), forall l:list X,
  l ++ [] = l.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem app_nil_r : forall (X:Type), forall l:list X,
  l ++ [] = l.
Proof.
intros. 
induction l as [| n l' IHl'].
- simpl. reflexivity.
- simpl. rewrite -> IHl'. reflexivity.
Qed.

Theorem app_assoc

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
intros. induction l as [| n' l' IHl'].
- simpl. reflexivity.
- simpl. rewrite -> IHl'. reflexivity.
Qed.

Lemma app_length

Lemma app_length : forall (X:Type) (l1 l2 : list X),
  length (l1 ++ l2) = length l1 + length l2.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Lemma app_length : forall (X:Type) (l1 l2 : list X),
  length (l1 ++ l2) = length l1 + length l2.
Proof.
intros. 
induction l1 as [| a l1' IHl1'].
- simpl. reflexivity.
- simpl. rewrite -> IHl1'. reflexivity.
Qed.

47: 2 stars, standard, optional (more_poly_exercises)

这里有一些稍微有趣一点的。。。

Theorem rev_app_distr

Theorem rev_app_distr: forall X (l1 l2 : list X),
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem rev_app_distr: forall X (l1 l2 : list X),
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
intros. 
induction l1 as [| b l1' IHl1'].
- simpl. induction l2 as [| b' l2' IHl2']. 
-- simpl. reflexivity.
-- simpl. rewrite -> app_nil_r. reflexivity.
- simpl. rewrite -> IHl1'. rewrite -> app_assoc. reflexivity.
Qed.

Theorem rev_involutive

Theorem rev_involutive : forall X : Type, forall l : list X,
  rev (rev l) = l.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem rev_involutive : forall X : Type, forall l : list X,
  rev (rev l) = l.
Proof.
intros. induction l as [| C l' IHl'].
- simpl. reflexivity.
- simpl.  rewrite -> rev_app_distr. simpl.  rewrite -> IHl'. reflexivity.
Qed.

多态对 Polymorphic Pairs

按照相同的模式，我们在上一章中给出的数字对的定义可以推广到多态对，通常称为乘积：

Inductive prod (X Y : Type) : Type :=
| pair (x : X) (y : Y).

Arguments pair {X} {Y}.

与列表一样，我们使类型参数隐式，并定义熟悉的具体符号。

Notation "( x , y )" := (pair x y).

我们还可以使用符号机制定义产品类型的标准符号：

Notation "X * Y" := (prod X Y) : type_scope.

（注释:type_scope告诉Coq，这个缩写词只能在解析类型时使用，而不能在解析表达式时使用。这避免了与乘法符号的冲突。）

一开始很容易混淆（x，y）和x×y。请记住，（x，y）是由其他两个值构建的值，而x×y是由其他两个类型构建的类型。如果x有类型x，y有类型y，那么（x，y）有类型x×y。

第一个和第二个投影函数现在看起来与任何函数式编程语言中的投影函数非常相似。

Definition fst {X Y : Type} (p : X × Y) : X :=
  match p with
  | (x, y) => x
  end.
Definition snd {X Y : Type} (p : X × Y) : Y :=
  match p with
  | (x, y) => y
  end.

下面的函数获取两个列表，并将它们组合成一个成对的列表。在其他函数式语言中，它通常被称为zip；为了与Coq的标准库保持一致，我们称之为combine。

Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y)
         : list (X*Y) :=
match lx, ly with
| [], _ => []
| _, [] => []
| x :: tx, y :: ty => (x, y) :: (combine tx ty)
end.

48: 1 star, standard, optional (combine_checks)

尝试在纸上回答以下问题，并在Coq中检查您的答案：

combine的类型是什么（即，在Check @combine 打印时检查什么？）

什么是

Compute (combine [1;2] [false;false;true;true]).

打印?

     = [(1, false); (2, false)]
     : list (nat * bool)

49: 2 stars, standard, especially useful (split)

函数split是combine的右反转：它获取一组对并返回一组列表。在许多函数式语言中，它被称为解压。

在下面填写split的定义。确保它通过了给定的单元测试。

Fixpoint split {X Y : Type} (l : list (X*Y)) : (list X) * (list Y)
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_split:
  split [(1,false);(2,false)] = ([1;2],[false;false]).
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Fixpoint split {X Y : Type} (l : list (X*Y)) : (list X) * (list Y):=
  match l with
  | [] => ([],[])
  | (x, y) :: l' => (x :: (fst (split l')), y :: (snd (split l')))
  end.

Example test_split:
  split [(1,false);(2,false)] = ([1;2],[false;false]).
Proof.
simpl.
reflexivity.
Qed.

多态选项 olymorphic Options

目前我们最后一种多态类型是多态选项，它是前一章中natoption的推广。（我们将定义放在一个模块中，因为标准库已经定义了选项，下面我们要使用这个选项。）

Module OptionPlayground.

Inductive option (X:Type) : Type :=
  | Some (x : X)
  | None.

Arguments Some {X}.
Arguments None {X}.

End OptionPlayground.

我们现在可以重写nth_error函数，以便它可以处理任何类型的列表

Fixpoint nth_error {X : Type} (l : list X) (n : nat)
                   : option X :=
  match l with
  | nil => None
  | a :: l' => match n with
               | O => Some a
               | S n' => nth_error l' n'
               end
  end.

Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.
Proof. reflexivity. Qed.
Example test_nth_error2 : nth_error [[1];[2]] 1 = Some [2].
Proof. reflexivity. Qed.
Example test_nth_error3 : nth_error [true] 2 = None.
Proof. reflexivity. Qed.

50: 1 star, standard, optional (hd_error_poly)

完成上一章中hd_error函数多态版本的定义。确保它通过了下面的单元测试。

Definition hd_error {X : Type} (l : list X) : option X
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

同样，为了强制隐式参数显式，我们可以在函数名之前使用@。

Check @hd_error : forall X : Type, list X -> option X.

Example test_hd_error1 : hd_error [1;2] = Some 1.
(* FILL IN HERE *) Admitted.
Example test_hd_error2 : hd_error  [[1];[2]]  = Some [1].
(* FILL IN HERE *) Admitted.

Coq代码

Definition hd_error {X : Type} (l : list X) : option X:=
match l with
| nil => None
| a :: l' => Some a
end.

Example test_hd_error1 : hd_error [1;2] = Some 1.
Proof. reflexivity. Qed.
Example test_hd_error2 : hd_error  [[1];[2]]  = Some [1].
Proof. reflexivity. Qed.