![cover image](https://wikiwandv2-19431.kxcdn.com/_next/image?url=https://upload.wikimedia.org/wikipedia/commons/thumb/7/71/Agda%2527s_official_logo.svg/langzh-640px-Agda%2527s_official_logo.svg.png&w=640&q=50)
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 在法语中意为公鸡)。