2.依賴型理論

依賴型別理論是一種強大而富有表現力的語言，允許我們表達複雜的數學斷言，編寫複雜的硬體和軟體規範，並以自然和統一的方式對這兩者進行推理。 精益是基於一種稱為歸納建構微積分的依賴型理論，具有可累積的非累積宇宙和歸納型別的層次結構。 到本章結束時，您將瞭解這意味著什麼。

2.1 簡單型別理論

作為數學的基礎，集合論有一個相當吸引人的簡單本體論。 一切都是一組，包括數字，函式，三角形，隨機過程和黎曼流形。 一個值得注意的事實是，人們可以從少數描述一些基本集合理論結構的公理構建一個豐富的數學世界。

但是出於許多目的，包括正式定理證明，最好有一個基礎設施來幫助我們管理和跟蹤我們正在使用的各種數學物件。 “型別理論”的名稱源於每個表示式都具有關聯型別的事實。 例如，在給定的上下文中，x + 0可以表示自然數，f可以表示對自然數的函式。

以下是我們如何在Lean中宣告物件並檢查其型別的一些示例。

import standard
open bool nat

/- declare some constants -/

constant m : nat        -- m is a natural number
constant n : nat
constants b1 b2 : bool  -- declare two constants at once

/- check their types -/

check m            -- output: nat
check n
check n + 0        -- nat    
check m * (n + 0)  -- nat
check b1           -- bool
check b1 && b2     -- "&&" is boolean and
check b1 || b2     -- boolean or
check tt           -- boolean "true"
 

第一個命令，import standard，告訴Lean我們打算使用標準庫。下一個命令open bool nat告訴Lean我們將使用來自布林理論和自然數理論的常數，事實和符號。在技​​術方面，bool和nat是名稱空間;稍後您將瞭解更多相關資訊。為了縮短示例，我們通常會隱藏相關匯入，如果在前面的示例中已經匯入。

/  - 和 -  /註釋表明下一行是精益忽略的註釋塊。類似地，兩個破折號表示該行的其餘部分包含也被忽略的註釋。註釋塊可以巢狀，從而可以“註釋掉”程式碼塊，就像在許多程式語言中一樣。

constant和constants命令將新的常量符號引入工作環境，check命令要求Lean報告其型別。你應該測試一下，然後嘗試輸入你自己的一些例子。以這種方式宣告新物件是試驗系統的好方法，但最終不可取：精益是一個基礎系統，也就是說，它為我們提供了強大的機制來定義我們需要的所有數學物件，而不是簡單地將它們假裝到系統中。我們將在後面的章節中探討這些機制。

簡單型別理論的強大之處在於可以構建其他型別的新型別。例如，如果A和B是型別，則A→B表示從A到B的函式型別，A×B表示笛卡爾積，即，由A元素和B元素組成的有序對的型別。

open prod   -- makes notation for the product available

constants m n : nat

constant f : nat → nat           -- type the arrow as "\to" or "\r"
constant f' : nat -> nat         -- alternative ASCII notation
constant f'' : ℕ → ℕ             -- \nat is alternative notation for nat
constant p : nat × nat           -- type the product as "\times"
constant q : prod nat nat        -- alternative notation
constant g : nat → nat → nat
constant g' : nat → (nat → nat)  -- has the same type as g!
constant h : nat × nat → nat

constant F : (nat → nat) → nat   -- a "functional"

check f               -- ℕ → ℕ
check f n             -- ℕ
check g m n           -- ℕ
check g m             -- ℕ → ℕ
check pair m n        -- ℕ × ℕ
check pr1 p           -- ℕ
check pr2 p           -- ℕ
check pr1 (pair m n)  -- ℕ
check pair (pr1 p) n  -- ℕ × ℕ
check F f             -- ℕ

符號ℕ是nat的符號;您可以輸入\ nat輸入它。還有一些事情需要注意。首先，將函式f應用於值x表示為f x。其次，在寫型別表示式時，箭頭與右側相關聯;例如，g的型別是nat→（nat→nat）。因此，我們可以將g視為一個函式，它接受自然數並返回另一個採用自然數並返回自然數的函式。在型別理論中，這通常比將g作為以一對自然數作為輸入的函式編寫更方便，並返回自然數作為輸出。例如，它允許我們“部分應用”函式g。上面的例子表明g m的型別為nat→nat，即“等待”第二個引數n的函式，然後返回g m n。採用nat×nat→nat型別的函式h和“重新定義”它看起來像g是一個稱為currying的過程，我們將回到下面。

到目前為止，您可能還猜到，在精益中，對m n表示有序的m和n對，如果p是一對，則pr1 p和pr2 p表示兩個投影。

2.2 作為物件的型別

精益依賴型別理論擴充套件簡單型別理論的一種方式是型別本身 - 像nat和bool這樣的實體 - 是一等公民，也就是說它們本身就是研究物件。 對於那種情況，他們每個人也必須有一個型別。

check nat               -- Type₁
check bool              -- Type₁
check nat → bool        -- Type₁
check nat × bool        -- Type₁
check nat → nat         -- ...
check nat × nat → nat
check nat → nat → nat
check nat → (nat → nat)
check nat → nat → bool
check (nat → nat) → nat

我們看到上面的每個表示式都是Type 1型別的物件。 我們馬上解釋下標1。 我們還可以為型別宣告新的常量和建構函式： 

constants A B : Type
constant F : Type → Type
constant G : Type → Type → Type

check A        -- Type
check F A      -- Type
check F nat    -- Type
check G A      -- Type → Type
check G A B    -- Type
check G A nat  -- Type

實際上，我們已經看到型別→型別→型別的函式的示例，即笛卡爾積。 

constants A B : Type

check prod           -- Type → Type → Type
check prod A         -- Type → Type
check prod A B       -- Type
check prod nat nat   -- Type₁

這是另一個例子：給定任何型別A，型別列表A表示型別A的元素列表的型別。

import data.list
open list

constant A : Type

check list      -- Type → Type
check list A    -- Type
check list nat  -- Type₁

我們將看到將型別建構函式視為普通數學函式例項的能力是依賴型別理論的強大特徵。

對於那些對集合理論基礎更為熟悉的人來說，將型別視為集合可能會有所幫助，在這種情況下，型別的元素只是集合的元素。 但附近有潛伏的圓形。 型別本身是一個像nat的表示式; 如果nat有一個型別，那麼Type不應該有型別嗎？

check Type      -- Type