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) ? 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.

多態候選

最后一種要介紹的多態類型是'多態候選（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 t
  end.

例如，如果我們將 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.