Agda
維基百科,自由的 encyclopedia
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年,17年前(2007)(2.0版) 1999年,25年前(1999)(1.0版) |
當前版本 |
|
型態系統 | 靜態類型、強類型、依賴類型 |
作業系統 | 跨平台 |
許可證 | MIT、BSD-like[2] |
文件擴展名 | .agda 、.lagda |
網站 | Agda wiki |
啟發語言 | |
Coq、Epigram(英語:Epigram)、Haskell | |
影響語言 | |
Idris |
Agda 的類型系統體現了柯里-霍華德同構(Curry-Howard correspondence),因此亦可作為一個構建構造性證明的證明輔助工具(英語:Proof assistant)。它的類型理論基於 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 在法語中意為公雞)。