Agda

**Agda** 是一個依賴類型的純函數式程式語言。目前的版本，Agda 2，最初由瑞典查爾摩斯工學院的 Ulf Norell 作為博士論文課題設計並實現。先前的版本 Agda 1 由 Catarina Coquand 在 1999 年開發，而現今的版本則是對其的徹底重寫，因此可視作一個全新的語言，但保留了 Agda 的命名和傳統。

Agda 的類型系統體現了柯里 - 霍華德同構（Curry-Howard correspondence），因此亦可作為一個構建構造性證明的證明輔助工具。它的類型理論基於 Zhaohui Luo 提出的 UTT（unified theory of dependent types），與 Per Martin-Löf 的直覺類型論相似。

Agda 與另一個基於依賴類型的證明輔助工具 Coq 設計上存在著顯著的不同之處：它本身並不提供單獨的證明策略語言（tactics），所有的證明均以函數式編程的方式書寫；Agda 擁有許多常規的函數式程序語言要素，諸如：數據類型（data types）、模式匹配（pattern matching）、記錄類型（records）、let 表達式和模塊（modules）等，而其語法設計則高度仿照 Haskell 語言。

用戶可通過 Emacs 或 Atom 編輯器的界面與 Agda 系統進行交互。Agda 系統亦可藉由命令行單獨調用。

通過類型檢查的 Agda 程序可以被編譯到 Haskell，並由 GHC 編譯器最終編譯為可執行的本地機器碼；亦有編譯到 JavaScript 的後端實現。

Agda 的名字來自於一首由音樂家 Cornelis Vreeswijk 創作的瑞典語歌曲「Hönan Agda」，歌詞講述了一隻名叫 Agda 的母雞的故事。這實際上影射了 Coq（Coq 在法語中意為公雞）。

## 簡介

### 一個簡單的「Hello world」程序

將下述程序保存於文件 `hello-world.agda` 中：

在 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 中歸納地定義皮亞諾數：

這表明存在兩種形式可以用來構造一個自然數：首先，zero 是一個自然數；若已知 n 是一個自然數，則 succ n 也必定是一個自然數。

又如，Agda 中對小於或等於關係的定義：

第一處構造（`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 則使用依賴類型模式匹配來達到此目的。例如，自然數的加法可被定義為：

比起運用歸納 / 遞歸原則，直接定義遞歸函數更加簡單直觀。依賴類型模式匹配是 Agda 內置的語言特性之一；其核心類型論並沒有包含歸納 / 遞歸原則。

### 記錄類型（records）

除了歸納類型之外，Agda 還支持記錄類型。記錄的作用是將若干類型的值包裝在一起，並使用不同名稱標識不同的域；它可看作是對依賴乘積類型（dependent product types）的推廣。
例如，在 Agda 中定義一個值對（pair）：

以上代碼定義了一個新的數據類型 `Pair : Set → Set → Set`，以及兩個投影函數：

記錄類型的值可以使用記錄表達式來創建，如：

若在定義記錄類型時使用 `constructor` 關鍵字規定了構造器，則亦可直接使用相應的構造器來創建記錄，如：

### 元變量（metavariables）

Agda 和其他類似的交互式證明系統（如 Coq）相比，一個顯著的特性是在證明構造中對元變量的大量利用。

例如，在 Agda 中可以寫出如下函數：

「?」即是一個元變量。在 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 的後端。

 

## 參見

* 柯里 - 霍華德同構
* 依賴類型
* 直覺類型論
* 同倫類型論
* 立方類型論
* Coq
* Idris
* Haskell

## 參考文獻

## 外部連結

* 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)