Software Foundations Vol.I : 多态与高阶函数(Poly)
多态
多态列表
在上一章中只使用了包含数的列表。很明显，程序还需要能够处理其它元素类型的列表
Inductive boollist : Type :=| bool_nil| bool_cons (b : bool) (l : boollist).
这很恼人,一方面必须为每种数据类型都定义不同的构造子，然而主因还是我们必须为每种数据类型再重新定义一遍所有的列表处理函数 （ length、rev 等）以及它们所有的性质（rev_length、app_assoc 等）。
为避免这些重复，Coq 支持定义'多态'归纳类型。 例如，以下就是'多态列表'数据类型。
Inductive list (X:Type) : Type :=| nil| cons (x : X) (l : list X).
这和上一章中 natlist 的定义基本一样，只是将 cons 构造子的 nat 参数换成了任意的类型 X，函数头的第一行添加了 X 的绑定， 而构造子类型中的 natlist 则换成了 list X
list 本身又是什么类型？
一种不错的思路就是把 list 当做从 Type 类型到 Inductive 归纳定义的'函数'；或者换种更简明的思路，即 list 是个从 Type 类型到 Type 类型的函数。
对于任何特定的类型 X， 类型 list X 是一个 Inductive 归纳定义的，元素类型为 X 的列表的集合。
Check list : Type → Type.
list 的定义中的参数 X 自动 成为构造子 nil 和 cons 的参数 —— 也就是说，nil 和 cons 在这里是多态的构造子；调用它们的时候必须要提供一个参数，就是它们要构造的列表的具体类型。
Check (nil nat) : list nat.
cons nat 与此类似，它将类型为 nat 的元素添加到类型为 list nat 的列表中。以下示例构造了一个只包含自然数 3 的列表：
nil 的类型会是什么呢？也许我们可以（根据定义）说它是 list X， 不过这样它就不是接受 X 返回 list 的函数了。
再提出一种：Type → list X 并没有解释 X 是什么，(X : Type) → list X 则比较接近。 Coq 对这种情况的记法为 ∀ X : Type, list X：
Check nil : forall X : Type, list X.
类似地，定义中 cons 的类型看起来像 X → list X → list X 然而以上述约定来解释 X 的含义则可以得到类型 ∀ X, X → list X → list X。
Check cons : ∀ X : Type, X → list X → list X.
如果在每次使用列表构造子时，都要为它提供类型参数，那样会很麻烦。 不过我们很快就会看到如何省去这种麻烦。
Check (cons nat 2 (cons nat 1 (nil nat))): list nat.
现在我们可以回过头来定义之前写下的列表处理函数的多态版本了。 例如 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.
类型标注
我们再写一遍 repeat 的定义，不过这次不指定任何参数的类型。 Coq 还会接受它么？
实际上,下面的代码还说明了一点:不论X作为Type这件事你认为是否重要,你都应该将其声明出来.
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': ∀ X : Type, X → nat → list X.
Check repeat: ∀ X : Type, X → nat → list X.
它与 repeat 的类型完全一致。
Coq 可以使用'类型推断' 基于它们的使用方式来推出 X、x 和 count 一定是什么类型。
例如， 由于 X 是作为 cons 的参数使用的，因此它必定是个 Type 类型， 因为 cons 期望一个 Type 作为其第一个参数，而用 0 和 S 来匹配 count 意味着它必须是个 nat，诸如此类。
这种强大的功能意味着我们不必总是在任何地方都显式地写出类型标注， 不过显式的类型标注对于文档和完整性检查来说仍然非常有用， 因此我们仍会继续使用它。
类型参数的推导
要使用多态函数，需要为其参数再额外传入一个或更多类型。
例如，前面 repeat 函数体中的递归调用必须传递类型 X。不过由于 repeat 的第二个参数为 X 类型的元素，第一个参数明显只能是 X， 既然如此，我们何必显式地写出它呢？
在任何可以写类型参数的地方，都可以将类型参数写为 “洞” _，可以看做是说 “请 Coq 自行找出这里应该填什么。”
更确切地说，当 Coq 遇到 _ 时，它会尝试'统一'所有的局部变量信息， 包括函数应当应用到的类型，其它参数的类型，以及应用函数的上下文中期望的类型， 以此来确定 _ 处应当填入的具体类型。
这听起来很像类型标注推断。实际上，这两种个过程依赖于同样的底层机制。 除了简单地忽略函数中某些参数的类型：
repeat' X x count : list X :=
我们还可以将类型换成洞：
repeat' (X : _) (x : _) (count : _) : list X :=
以此来告诉 Coq 要尝试推断出缺少的信息。
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 _))).
隐式参数
甚至可以通过告诉 Coq '总是'推断给定函数的类型参数来在大多数情况下 直接避免写 _。
Arguments 用于指令指定函数或构造子的名字并列出其参数名， 花括号中的任何参数都会被视作隐式参数。（如果定义中的某个参数没有名字， 那么它可以用通配模式 _ 来标记。这种情况常见于构造子中。）
Arguments: 显式指定函数或构造子名字所对应的参数.
Arguments nil {X}.
Arguments cons {X} _ _.
Arguments repeat {X} x count.
现在我们完全不用提供类型参数了：
Definition list123'' := cons 1 (cons 2 (cons 3 nil)).
此外，我们还可以在定义函数时就声明隐式参数， 只需要将某个参数两边的圆括号换成花括号。例如：
Fixpoint repeat''' {X : Type} (x : X) (count : nat) : list X :=match count with| 0 ⇒ nil| S count' ⇒ cons x (repeat''' x count')end.
（注意现在甚至不必在 repeat''' 的递归调用中提供类型参数了， 实际上提供了反而是无效的，因为 Coq 并不想要它。）
我们会尽可能使用最后一种风格，不过还会继续在 Inductive 构造子中使用显式的 Argument 声明。
原因在于如果将归纳类型的形参标为隐式的话，不仅构造子的类型会变成隐式的，类型本身也会变成隐式的。
例如， 考虑以下 list 类型的另一种定义：
Inductive list' {X:Type} : Type :=| nil'| cons' (x : X) (l : list').
由于 X 在包括 list' 本身的'整个'归纳定义中都是隐式声明的， 因此当我们讨论数值、布尔值或其它任何类型的列表时，都只能写 list'， 而写不了 list' nat、list' bool 等等，这样就有点过分了。
作为本节的收尾，为新的多态列表重新实现几个其它的标准列表函数...
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 {X:Type} (l:list X) : list X :=match l with| nil => nil| cons h t => app (rev t) (cons h nil)end.Fixpoint length {X : Type} (l : list X) : nat :=match l with| nil => 0| cons _ l' => S (length l')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.
Example test_length1: length (cons 1 (cons 2 (cons 3 nil))) = 3.
Proof. reflexivity. Qed.
显式提供类型参数
用 Implicit 将参数声明为隐式的会有个小问题：Coq 偶尔会没有足够的局部信息来确定类型参数。此时，需要告诉 Coq 这次我们会显示地给出参数。
例如，假设写了如下定义：
Fail Definition mynil := nil.
（Definition 前面的 Fail 限定符可用于'任何'指令， 它的作用是确保该指令在执行时确实会失败。如果该指令失败了，Coq 就会打印出相应的错误信息，不过之后会继续处理文件中剩下的部分。）
Fail: 添加在指令的前面,用于判断执行是否失败,但是在失败后继续处理.
在这里，Coq 给出了一条错误信息，因为它不知道应该为 nil 提供何种类型。 可以通过为它提供个显式的类型声明来帮助它，这样 Coq 在“应用”nil 时就有更多可用的信息了：
Definition mynil : list nat := nil.
此外，还可以在函数名前加上前缀 @ 来强制将隐式参数变成显式的：
Check @nil : ∀ 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].
多元序对
按照相同的模式，在上一章中给出的数值序对的定义可被推广为 '多态序对（Polymorphic Pairs）'，它通常叫做'积（Products）'：
Inductive prod (X Y : Type) : Type :=
| pair (x : X) (y : Y).
Arguments pair {X} {Y} _ _.
和列表一样，也可以将类型参数定义成隐式的， 并以此定义类似的具体记法：
Notation "( x , y )" := (pair x y).
也可以使用 Notation 来定义标准的'积类型（Product Types）'记法：
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。
第一元（first）和第二元（second）的射影函数（Projection Functions） 现在看起来和其它函数式编程语言中的很像了：
Definition fst {X Y : Type} (p : X × Y) : X :=match p with| (x, y) ⇒ xend.
Definition snd {X Y : Type} (p : X × Y) : Y :=match p with| (x, y) ⇒ yend.
以下函数接受两个列表，并将它们结合成一个序对的列表。 在其它函数式语言中，它通常被称作 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.
多态候选
最后一种要介绍的多态类型是'多态候选（Polymorphic Options）', 它推广了上一章中的 natoption
Inductive option (X:Type) : Type :=| Some (x : X)| None.
Arguments Some {X} _.
Arguments None {X}.
现在可以重写 nth_error 函数来让它适用于任何类型的列表了。
Fixpoint nth_error {X : Type} (l : list X) (n : nat): option X :=match l with| [] => None| a :: l' => if n =? O then Some a else nth_error l' (pred n)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.
函数作为数据
和大部分现代编程语言一样，特别是“函数式”的语言，包括 OCaml、Haskell、 Racket、Scala、Clojure 等，Coq 也将函数视作“一等公民（First-Class Citizens）”， 即允许将它们作为参数传入其它函数、作为结果返回、以及存储在数据结构中等等。
高阶函数
用于操作其它函数的函数通常叫做'高阶函数'。以下是简单的示例：
Definition doit3times {X:Type} (f:X→X) (n:X) : X :=f (f (f n)).
这里的参数 f 本身也是个（从 X 到 X 的）函数， doit3times 的函数体将 f 对某个值 n 应用三次。
Check @doit3times : ∀ X : Type, (X → X) → X → X.Example test_doit3times: doit3times minustwo 9 = 3.
Proof. reflexivity. Qed.
Example test_doit3times': doit3times negb true = false.
Proof. reflexivity. Qed.
过滤器
下面是个更有用的高阶函数，它接受一个元素类型为 X 的列表和一个 X 的谓词（即一个从 X 到 bool 的函数），然后“过滤”此列表并返回一个新列表， 其中仅包含对该谓词返回 true 的元素。
Fixpoint filter {X:Type} (test: X→bool) (l:list X): (list X) :=match l with| [] ⇒ []| h :: t ⇒ if test h then h :: (filter test t)else filter test tend.
例如，如果我们将 filter 应用到谓词 evenb 和一个数值列表 l 上，那么它就会返回一个只包含 l 中偶数的列表。
Example test_filter1: filter evenb [1;2;3;4] = [2;4].
Proof. reflexivity. Qed.Definition length_is_1 {X : Type} (l : list X) : bool :=(length l) =? 1.
Example test_filter2:filter length_is_1[ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]= [ [3]; [4]; [8] ].
Proof. reflexivity. Qed.
可以使用 filter 给出 Lists 中 countoddmembers 函数的简洁的版本。
Definition countoddmembers' (l:list nat) : nat :=length (filter oddb l).Example test_countoddmembers'1: countoddmembers' [1;0;3;1;4;5] = 4.
Proof. reflexivity. Qed.
Example test_countoddmembers'2: countoddmembers' [0;2;4] = 0.
Proof. reflexivity. Qed.
Example test_countoddmembers'3: countoddmembers' nil = 0.
Proof. reflexivity. Qed.
匿名函数
我们经常需要传入“一次性”的函数作为参数，之后不会再用，而为每个函数取名是十分无聊的。幸运的是，有一种更好的方法。我们可以按需随时构造函数而不必在顶层中声明它 或给它取名。
Example test_anon_fun':doit3times (fun n ⇒ n × n) 2 = 256.
Proof. reflexivity. Qed.
表达式 (fun n ⇒ n × n) 可读作“一个给定 n 并返回 n × n 的函数。”以下为使用匿名函数重写的 filter 示例：
Example test_filter2':filter (fun l ⇒ (length l) =? 1)[ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]= [ [3]; [4]; [8] ].
Proof. reflexivity. Qed.
fun: 结合=>运算符来声明lambda函数.
映射
另一个方便的高阶函数叫做 map。
Fixpoint map {X Y: Type} (f:X→Y) (l:list X) : (list Y) :=match l with| [] ⇒ []| h :: t ⇒ (f h) :: (map f t)end.
它接受一个函数 f 和一个列表 l = [n1, n2, n3, ...] 并返回列表 [f n1, f n2, f n3,...] ，其中 f 可分别应用于 l 中的每一个元素。例如：
Example test_map1: map (fun x ⇒ plus 3 x) [2;0;2] = [5;3;5].
Proof. reflexivity. Qed.
输入列表和输出列表的元素类型不必相同，因为 map 会接受'两个'类型参数 X 和 Y，因此它可以应用到一个数值的列表和一个从数值到布尔值的函数， 并产生一个布尔值列表：
Example test_map2:map oddb [2;1;2;5] = [false;true;false;true].
Proof. reflexivity. Qed.
它甚至可以应用到一个数值的列表和一个从数值到布尔值列表的函数， 并产生一个布尔值的'列表的列表'：
Example test_map3:map (fun n ⇒ [evenb n;oddb n]) [2;1;2;5]= [[true;false];[false;true];[true;false];[false;true]].
Proof. reflexivity. Qed.
折叠
一个更加强大的高阶函数叫做 fold。该函数启发自“reduce 归约” 操作，它是 Google 的 map/reduce 分布式编程框架的核心。
Fixpoint fold {X Y: Type} (f: X→Y→Y) (l: list X) (b: Y): Y :=match l with| nil ⇒ b| h :: t ⇒ f h (fold f t b)end.
直观上来说，fold 操作的行为就是将给定的二元操作符 f 插入到给定列表的每一对元素之间。
例如， fold plus [1;2;3;4] 直观上的意思是 1+2+3+4。为了让它更精确，还需要一个“起始元素” 作为 f 初始的第二个输入。
因此，例如fold plus [1;2;3;4] 0 就会产生 1 + (2 + (3 + (4 + 0))).
以下是更多例子：
Check (fold andb) : list bool → bool → bool.
Example fold_example1 :fold mult [1;2;3;4] 1 = 24.
Proof. reflexivity. Qed.Example fold_example2 :fold andb [true;true;false;true] true = false.
Proof. reflexivity. Qed.Example fold_example3 :fold app [[1];[];[2;3];[4]] [] = [1;2;3;4].
Proof. reflexivity. Qed.
用函数构造函数
目前讨论过的大部分高阶函数都是以函数作为参数的。现在来看将函数作为其它函数的结果'返回'的例子。
下面是一个接受值 x（由某个类型 X 刻画）并返回一个从 nat 到 X 的函数，当它被调用时总是产生 x 并忽略其 nat 参数。
Definition constfun {X: Type} (x: X) : nat→X :=fun (k:nat) ⇒ x.
Definition ftrue := constfun true.
Example constfun_example1 : ftrue 0 = true.
Proof. reflexivity. Qed.Example constfun_example2 : (constfun 5) 99 = 5.
Proof. reflexivity. Qed.
回想 plus 的类型。
Check plus : nat → nat → nat.
该表达式中的每个 → 实际上都是一个类型上的'二元'操作符。
该操作符是'右结合'的，因此 plus 的类型其实是 nat → (nat → nat) 的简写.它接受一个 nat 并返回另一个函数，该函数接受另一个 nat 并返回一个 nat。
在上面的例子中，总是将 plus 一次同时应用到两个参数上。
不过如果喜欢，也可以一次只提供一个参数，这叫做'偏应用（Partial Application）'。
Definition plus3 := plus 3.
Check plus3 : nat → nat.
Example test_plus3 : plus3 4 = 7.
Proof. reflexivity. Qed.
Example test_plus3' : doit3times plus3 0 = 9.
Proof. reflexivity. Qed.
Example test_plus3'' : doit3times (plus 3) 0 = 9.
Proof. reflexivity. Qed.