檢視 Agda 的原始碼

'''Agda'''是一个依賴類型的純函數式程式語言。目前的版本，Agda 二，頭仔由瑞典查爾摩斯工學院的 Ulf Norell 做博士論文課題設計並實現。進前的版本 Agda 一由 Catarina Coquand 佇一九九九年開發，這馬的版本是對其實的徹底重寫，所以會當看做一个全新的語言，猶毋過保留 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 二 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 ( 二千空六 )

[[分類: 待校正]]