Agda
 | |
| 編程範型 | 函數式編程 |
|---|---|
| 設計者 | Ulf Norell（2.0版） Catarina Coquand（1.0版） |
| 實作者 | Ulf Norell（2.0版） Catarina Coquand（1.0版） |
| 面市時間 | 2007年（2.0版） 1999年（1.0版） |
| 當前版本 |
|
| 型態系統 | 靜態類型、強類型、依賴類型 |
| 作業系統 | 跨平台 |
| 許可證 | MIT、BSD-like[2] |
| 文件擴展名 | .agda、.lagda |
| 網站 | Agda wiki |
| 啟發語言 | |
| Coq、Epigram、Haskell | |
| 影響語言 | |
| Idris | |
Agda 是一個依賴類型的純函數式程式語言。目前的版本，Agda 2，最初由瑞典查爾摩斯工學院的 Ulf Norell 作為博士論文課題設計並實現[3]。先前的版本 Agda 1 由 Catarina Coquand 在 1999 年開發，而現今的版本則是對其的徹底重寫，因此可視作一個全新的語言，但保留了 Agda 的命名和傳統。
Agda 的類型系統體現了柯里-霍華德同構（Curry-Howard correspondence），因此亦可作為一個構建構造性證明的證明輔助工具。它的類型理論基於 Zhaohui Luo 提出的 UTT（unified theory of dependent types）[4]，與 Per Martin-Löf 的直覺類型論相似。
Agda 與另一個基於依賴類型的證明輔助工具 Coq 設計上存在著顯著的不同之處：它本身並不提供單獨的證明策略語言（tactics），所有的證明均以函數式編程的方式書寫；Agda 擁有許多常規的函數式程序語言要素，諸如：數據類型（data types）、模式匹配（pattern matching）、記錄類型（records）、let表達式和模塊（modules）等，而其語法設計則高度仿照 Haskell 語言。
用戶可通過 Emacs 或 Atom 編輯器的界面與 Agda 系統進行交互[5]。Agda 系統亦可藉由命令行單獨調用。
通過類型檢查的 Agda 程序可以被編譯到 Haskell，並由 GHC 編譯器最終編譯為可執行的本地機器碼；亦有編譯到 JavaScript 的後端實現。
Agda 的名字來自於一首由音樂家 Cornelis Vreeswijk 創作的瑞典語歌曲「Hönan Agda」，歌詞講述了一隻名叫 Agda 的母雞的故事。這實際上影射了 Coq（Coq 在法語中意為公雞）。
簡介
[編輯]一個簡單的「Hello world」程序
[編輯]將下述程序保存於文件hello-world.agda中：
module hello-world where
open import IO
main = run (putStrLn "Hello, World!")
在 Emacs 中可使用 C-c C-x C-c 來編譯此程序；或在命令行中執行agda --compile hello-world.agda進行編譯。
幾點解釋：
- Agda 程序以模塊（module）的形式組織而成。每一個文件中的第一個模塊稱之為最高級別（top-level）模塊，其名稱必須和文件名相符。模塊的內容可以包括數據類型的定義、函數的定義等。
- 外部模塊可以通過
import子句導入。例如在上述程序中，open import IO導入 Agda 標準庫中的IO（標準輸入輸出）模塊，並將其在當前作用域中打開。 - 一個導出了函數名及類型簽名
main : IO a的模塊即可以被編譯成可執行文件。例如，上述程序中的main函數作用是將字符串「Hello, World!」寫到標準輸出，之後退出程序。
歸納類型（inductive types）
[編輯]在 Agda 中定義數據類型的方式與其它（非依賴類型）程式語言中的代數數據類型相似。 例如，在 Agda 中歸納地定義皮亞諾數：
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
這表明存在兩種形式可以用來構造一個自然數：首先，zero 是一個自然數；若已知 n 是一個自然數，則 succ n 也必定是一個自然數。
又如，Agda 中對小於或等於關係的定義：
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {n m : ℕ} → n ≤ m → succ n ≤ succ m
第一處構造（z≤n）指出：zero 必定小於或等於任何自然數；第二處構造（s≤s）指出：當 n <= m 時必定有 succ n <= succ m。
例如，考慮z≤n {succ zero}，依照定義，它是對零小於一的證明；再考慮s≤s {zero} {succ zero} (z≤n {succ zero})，則是對一小於二的證明。
依賴類型模式匹配（dependently typed pattern matching）
[編輯]在類型論中，歸納和遞歸原則通常被用來證明涉及到歸納類型的定理。Agda 則使用依賴類型模式匹配來達到此目的。例如，自然數的加法可被定義為：
add zero n = n
add (succ m) n = succ (add m n)
比起運用歸納/遞歸原則，直接定義遞歸函數更加簡單直觀。依賴類型模式匹配是 Agda 內置的語言特性之一；其核心類型論並沒有包含歸納/遞歸原則。
記錄類型（records）
[編輯]除了歸納類型之外，Agda 還支持記錄類型。記錄的作用是將若干類型的值包裝在一起，並使用不同名稱標識不同的域；它可看作是對依賴乘積類型（dependent product types）的推廣。 例如，在 Agda 中定義一個值對（pair）：
record Pair (A B : Set) : Set where
field
fst : A
snd : B
以上代碼定義了一個新的數據類型Pair : Set → Set → Set，以及兩個投影函數：
Pair.fst : {A B : Set} → Pair A B → A
Pair.snd : {A B : Set} → Pair A B → B
記錄類型的值可以使用記錄表達式來創建，如：
p12 = record { fst = 1; snd = 2 }
若在定義記錄類型時使用constructor關鍵字規定了構造器，則亦可直接使用相應的構造器來創建記錄，如：
record Pair (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B
p34 : Pair Nat Nat
p34 = 3 , 4
元變量（metavariables）
[編輯]Agda 和其他類似的交互式證明系統（如 Coq）相比，一個顯著的特性是在證明構造中對元變量的大量利用。
例如，在 Agda 中可以寫出如下函數：
add : ℕ → ℕ → ℕ
add x y = ?
「?」即是一個元變量。在 Emacs mode 中交互時，系統會提示用戶所期望的類型，允許用戶進一步添加具體代碼到其中。該特性為漸進式程序構造提供了支持，從而達到與 Coq 的證明策略（tactics）類似的意圖。
證明自動化和反射（reflection）
[編輯]宇宙（universe）
[編輯]高階歸納類型（higher inductive types）
[編輯]終止檢查（termination checking）
[編輯]作為一個定理證明系統，Agda 語言中的定義必須是完整（total）的。所有的程序必須終止，所有的模式必須得到匹配。若無法保證定義的完整性，其類型論背後所對應的邏輯將失去一致性，導致假命題可以被證明。
目前 Agda 使用 Foetus 終止檢查器。
Unicode
[編輯]Agda 語言大量吸收了 Unicode 字符集中的數學符號，這使得其證明更具可讀性。Agda 的 Emacs mode 中提供了輸入這些符號的快捷鍵；這仿照 TeX 中書寫數學符號的形式。例如，輸入 Σ 可以使用 \Sigma。
標準庫
[編輯]Agda 的標準庫包含了一些常見資料結構的定義和相關的定理證明，例如自然數、列表（lists）與矢量（vectors）。
編譯器
[編輯]Agda 目前具備兩個官方的編譯器後端：編譯到 Haskell 的 MAlonzo 後端；和另一個編譯到 JavaScript 的後端。
參見
[編輯]參考文獻
[編輯]- ^ Release 2.7.0.1. 2024年9月12日 [2024年9月20日].
- ^ Agda license file. [2020-01-08]. （原始內容存檔於2022-04-26）.
- ^ Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007. [1] （頁面存檔備份，存於網際網路檔案館）
- ^ Luo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.
- ^ Coquand, Catarina; Synek, Dan; Takeyama, Makoto. An Emacs interface for type directed support constructing proofs and programs (PDF). European Joint Conferences on Theory and Practice of Software 2005. [2013-12-24]. （原始內容 (PDF)存檔於2011-07-22）.
外部連結
[編輯]- The Agda 2 homepage（頁面存檔備份，存於網際網路檔案館） (a wiki), including documentation and a link to a bug-report tool
- Agda at the Hackage repository（頁面存檔備份，存於網際網路檔案館）
- Learn you an Agda（頁面存檔備份，存於網際網路檔案館）, a tutorial.
- A course on Functional Programming, with seven parts on Agda
- Introduction to Agda（頁面存檔備份，存於網際網路檔案館）, a five-part YouTube playlist by Daniel Peebles
- Dependently Typed Programming in Agda（頁面存檔備份，存於網際網路檔案館）, by Ulf Norell
- A Brief Overview of Agda（頁面存檔備份，存於網際網路檔案館）, by Ana Bove, Peter Dybjer, and Ulf Norell
- An Agda Tutorial, Misao Nagayama, Hideaki Nishihara, Makoto Takeyama (2006)
