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`中：

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

```agda
data ℕ : Set where
  zero : ℕ 
  succ : ℕ → ℕ
```

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

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

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

```agda
add zero n = n
add (succ m) n = succ (add m n)
```

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

### 記錄類型（records）

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

例如，在 Agda 中定義一個值對（pair）：

```agda
record Pair (A B : Set) : Set where
  field
    fst : A
    snd : B
```

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

```agda
Pair.fst : {A B : Set} → Pair A B → A
Pair.snd : {A B : Set} → Pair A B → B
```

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

```agda
p12 = record { fst = 1; snd = 2 }
```

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

```agda
record Pair (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

p34 : Pair Nat Nat
p34 = 3 , 4
```

### 元變量（metavariables）

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

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

```agda
add : ℕ → ℕ → ℕ 
add x y = ?
```

「?」即是一個元變量。在 Emacs mode 中交互時，系統會提示使用者所期望的類型，允許用戶進一步添加具體代碼到其中。該特性為漸進式程序構造提供了支持，從而達到與 Coq 的證明策略（tactics）類似的意圖。

### 終止檢查（termination checking）

作為一個定理證明系統，Agda 語言中的定義必須是完整（total）的。所有的程序必須終止，所有的模式必須得到匹配。若無法保證定義的完整性，其類型論背後所對應的邏輯將失去一致性，導致假命題可以被證明。

目前 Agda 使用 Foetus 終止檢查器。

### Unicode

Agda 語言大量吸收了 Unicode 字符集中的數學符號，這使得其證明更具可讀性。Agda 的 Emacs mode 中提供了輸入這些符號的快捷鍵；這仿照 TeX 中書寫數學符號的形式。例如，輸入 Σ 可以使用 `\Sigma`。

### 標準庫

Agda 的標準庫包含了一些常見數據結構的定義和相關的定理證明，例如自然數、列表（lists）與矢量（vectors）。

### 編譯器

Agda 目前具備兩個官方的編譯器後端：編譯到 Haskell 的 MAlonzo 後端；和另一個編譯到 JavaScript 的後端。

## 外部連結

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

## 基本資料

- 編程范型：函數式編程
- 設計者：Ulf Norell（2.0版）、Catarina Coquand（1.0版）
- 開發者：Ulf Norell（2.0版）、Catarina Coquand（1.0版）
- 發行時間：2007年（2.0版）、1999年（1.0版）
- 軟體版本週期：2.6.2
- 軟體版本週期：2021年6月19日
- 類型系統：靜態類型、強類型、依賴類型
- 施影響於：Idris
- 受影響於：Coq、Epigram、Haskell
- 許可證：MIT、BSD-like
- 網站： Agda wiki
- 文件擴展名：`.agda`、`.lagda`
- 作業系統：跨平台