Agda

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版）
当前版本	2.7.0.1（2024年9月12日；穩定版本）[1]
型態系統	静态类型、强类型、依赖类型
操作系统	跨平台
許可證	MIT、BSD-like[2]
文件扩展名	.agda、.lagda
網站	Agda wiki
啟發語言
Coq、Epigram（英语：Epigram）、Haskell
影響語言
Idris

Agda 是一个依赖类型的纯函数式编程语言。目前的版本，Agda 2，最初由瑞典查尔摩斯工学院的 Ulf Norell 作为博士论文课题设计并实现^[3]。先前的版本 Agda 1 由 Catarina Coquand 在 1999 年开发，而现今的版本则是对其的彻底重写，因此可视作一个全新的语言，但保留了 Agda 的命名和传统。

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 在法语中意为公鸡）。

1. ^ Release 2.7.0.1. 2024年9月12日 [2024年9月20日]. 
2. ^ Agda license file. [2020-01-08]. （原始内容存档于2022-04-26）. 
3. ^ Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007. [1] （页面存档备份，存于互联网档案馆）
4. ^ Luo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.
5. ^ 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）.