Agda
Agda 是一個依賴類型的純函數式編程語言。目前的版本,Agda 2,最初由瑞典查爾摩斯工學院的 Ulf Norell 作為博士論文課題設計並實現[3]。先前的版本 Agda 1 由 Catarina Coquand 在 1999 年開發,而現今的版本則是對其的徹底重寫,因此可視作一個全新的語言,但保留了 Agda 的命名和傳統。
![]() | |
編程範型 | 函數式編程 |
---|---|
設計者 | Ulf Norell(2.0版) Catarina Coquand(1.0版) |
實作者 | Ulf Norell(2.0版) Catarina Coquand(1.0版) |
面市時間 | 2007年 1999年 (1.0版) | (2.0版)
當前版本 |
|
型態系統 | 靜態類型、強類型、依賴類型 |
操作系統 | 跨平台 |
許可證 | MIT、BSD-like[2] |
文件擴展名 | .agda 、.lagda |
網站 | Agda wiki |
啟發語言 | |
Coq、Epigram、Haskell | |
影響語言 | |
Idris |
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 v2.7.0 · agda/agda. [2024年8月19日] (英語).
- ^ 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)