Agda

编程范型| 函数式编程
設計者| Ulf Norell（2.0版）
Catarina Coquand（1.0版）
實作者| Ulf Norell（2.0版）
Catarina Coquand（1.0版）
发行时间| 2007年，​18年前​（2007）（2.0版）
1999年，​26年前​（1999）（1.0版）
当前版本|

* 2.8.0（2025年7月5日；穩定版本）[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 在法语中意为公鸡）。

## 简介

[编辑]

### 一个简单的“Hello world”程序

[编辑]

将下述程序保存于文件`hello-world.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 中归纳地定义皮亚诺数：

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

这表明存在两种形式可以用来构造一个自然数：首先，zero 是一个自然数；若已知 n 是一个自然数，则 succ n 也必定是一个自然数。

又如，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 则使用依赖类型模式匹配来达到此目的。例如，自然数的加法可被定义为：

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

比起运用归纳/递归原则，直接定义递归函数更加简单直观。依赖类型模式匹配是 Agda 内置的语言特性之一；其核心类型论并没有包含归纳/递归原则。

### 记录类型（records）

[编辑]

除了归纳类型之外，Agda 还支持记录类型。记录的作用是将若干类型的值包装在一起，并使用不同名称标识不同的域；它可看作是对依赖乘积类型（dependent product types）的推广。 例如，在 Agda 中定义一个值对（pair）：

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

以上代码定义了一个新的数据类型`Pair : Set → Set → Set`，以及两个投影函数：

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

记录类型的值可以使用记录表达式来创建，如：

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

若在定义记录类型时使用`constructor`关键字规定了构造器，则亦可直接使用相应的构造器来创建记录，如：

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

p34 : Pair Nat Nat
p34 = 3 , 4

### 元变量（metavariables）

[编辑]

Agda 和其他类似的交互式证明系统（如 Coq）相比，一个显著的特性是在证明构造中对元变量的大量利用。

例如，在 Agda 中可以写出如下函数：

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

“?”即是一个元变量。在 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

## 参考文献

[编辑]

1. ^ Release 2.8.0. 2025年7月5日  [2025年7月13日].
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）.

## 外部链接

[编辑]

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

* 查
* 论
* 编

编程语言

范型|

| 过程式|

* FORTRAN
* COBOL
* JOVIAL
* ALGOL 60
* JOSS（英语：JOSS）
* BASIC
* PL/I
* MUMPS（英语：MUMPS）
* ALGOL 68
* Forth
* Pascal
* Turbo Pascal
* C
* Modula-2
* Ada 83
* occam
* Oberon
* Go
* Ballerina（英语：Ballerina (programming language)）

|

面向对象|

* Simula 67
* Smalltalk
* Objective-C
* Eiffel
* Object Pascal
* Delphi
* Self
* CLOS
* Visual Basic
* Gambas
* Ada 95
* Java
* C#
* Vala
* Crystal（英语：Crystal (programming language)）

多范型|

* C++
* Modula-3
* Dylan
* Python
* Lua
* JavaScript
* Ruby
* D
* Factor
* Scala
* F#
* Haxe
* Nim
* Chapel（英语：Chapel (programming language)）
* Rust
* Kotlin
* Dart
* Swift
* Zig
* Ring（英语：Ring (programming language)）
* V（英语：V (programming language)）
* Mojo
* Carbon

函数式|

* LISP
* Scheme
* Common Lisp
* Clojure
* Logo
* APL/`J`
* ML
* Standard ML
* OCaml
* Erlang
* Elixir
* Haskell
* SAC
* Agda
* Idris
* jq
* Gleam（英语：Gleam (programming language)）

逻辑式|

* Prolog
* Datalog
* Mercury
* AnsProlog
* ProbLog（英语：ProbLog）

脚本语言|

| 动态语言|

* SNOBOL
* Icon
* REXX
* Perl
* Raku
* Tcl/Tk
* Python
* Lua
* Ruby
* PHP
* Hack
* CFML（英语：ColdFusion Markup Language）
* REBOL
* Red（英语：Red (programming language)）
* Io
* Julia
* jq

|

Shell语言|

* Unix shell
* sh/ash/dash
* csh/tcsh
* ksh
* bash
* zsh
* rc（英语：rc (Unix shell)）
* AWK
* PowerShell

ECMA-262|

* ECMAScript
* JavaScript
* TypeScript
* CoffeeScript/LiveScript（英语：LiveScript (programming language)）
* Elm
* PureScript
* Reason
* Bosque（英语：Bosque (programming language)）

特定平台|

| .NET|

* C#
* C++/CLI
* F#
* PowerShell
* VB.NET
* Small Basic

|

JVM|

* Java
* AspectJ（英语：AspectJ）
* Scala
* Clojure
* Groovy
* Kotlin

特定领域|

| 科学计算|

* Speakeasy（英语：Speakeasy (computational environment)）
* IDL
* GDL
* Maxima
* Maple
* MATLAB
* Octave
* Scilab
* Wolfram
* R
* Yorick（英语：Yorick (programming language)）
* SageMath
* Julia

|

GPU计算|

* Cg/HLSL
* GLSL/GLSL ES
* Brook（英语：BrookGPU）
* CUDA/PTX（英语：Parallel Thread Execution）
* OpenCL/SPIR-V（英语：Standard Portable Intermediate Representation）
* Futhark
* WGSL（英语：WebGPU Shading Language）

数据查询|

* CODASYL（英语：CODASYL）
* SQL
* PL/SQL
* T-SQL
* SQL/PSM（英语：SQL/PSM）
* xBase（英语：xBase）
* XPath
* XQuery（英语：XQuery）
* GraphQL

可视化|

* Prograph（英语：Prograph）
* Simulink
* LabVIEW
* Orange（英语：Orange (software)）
* KNIME（英语：KNIME）
* Scratch
* Snap!
* App Inventor
* Power Fx

传媒设计|

* SuperCollider
* Pure Data
* AviSynth
* Processing
* ChucK

其它|

* 汇编语言
* APT（英语：APT (programming language)）
* GPSS（英语：GPSS）
* CLIPS（英语：CLIPS）
* AMPL
* dc
* sed
* yacc
* make
* PostScript
* XSLT
* LLVM IR
* WebAssembly
* 深奥的编程语言

* 目录
* 列表
* 历史
* 比较（英语：Comparison of programming languages）
* 时间线

*[查]: 查看该模板
*[论]: 讨论该模板
*[编]: 编辑该模板