Agda 是什么？¶

Agda 是一种带有依赖类型的编程语言。它是 Martin-Löf 类型论的一种扩展，也是 Chalmers 编程语言小组语言开发传统中最新开发的语言。此传统中的其它语言包括 Alf、Alfa、Agda 1 和 Cayenne。其它紧密相关的语言包括 Coq、Epigram 和 Idris。

由于带有强定型和依赖类型，Agda 可以作为证明助理，（在构造性设置下）证明数学定理并将这些证明当做算法来运行。

依赖类型¶

Typing for programmers¶

类型论同时涉及到编程和逻辑。我们将类型系统看作表达语法正确性的一种方式。类型正确的程序才有意义。 Lisp 是一种完全无类型的编程语言，其衍生语言 Scheme亦是如此。在这类语言中，若 f 是一个函数，那么我们可以将它应用到任何东西上，包括它自身。这让编写程序变得很容易（几乎所有程序都是良构的），但编写出错误的程序也很容易。程序可能会引发异常或死循环，而分析之问题所在也十分困难。

Haskell 或 ML 及其衍生语言如 Standard ML 和 Caml 都是有类型的语言，它们的函数带有的类型，其类型表达了程序期望的参数类型和结果的类型。

在这两族语言出现之前的语言，有的有定型规则，有的则没有。大部分指令式语言都没有丰富的类型系统。例如，C 带有类型，但非常宽松（几乎一切都是整数或其变体）。此外，其定型系统必须用指针才能定义树或图。

所有这些语言都属于不完全语言（Partial Languages），例如，类型为 T 的表达式 e 的计算结果为以下几种情况：

程序以类型为 T 的值停机
程序 e 不停机
程序引发异常（这由不完全的定义产生，例如一个函数只为正整数定义，但应用在了负整数上。）

Agda 和其它基于类型论的语言是完全语言（Total Languages），即类型为 T 的程序 e of type T 总是会在类型为 T 的值上停机，不会出现运行时错误，也无法不出不停机的程序（除非由程序员显式要求）。

依赖类型¶

让类型族以其它类型的对象为索引，就引入了依赖类型（Dependent Type）。例如，我们可以将长度为 n 的向量类型定义为 Vec n。这是一个类型族，它以 Nat 中的对象为索引（以自然数参数化的类型）。

有了依赖类型后，我们必须推广函数和序对（Pair）的类型。

依赖函数空间（dependent function space） (a : A) -> (B a) 是接受一个类型为 A 的参数 a`，产生类型为 B a 的结果的函数类型。在这里，A 是一个类型， B 是一个以 A 中的元素为索引的类型族。

例如，我们可以将 n x m 的矩阵类型定义为一个以两个自然数为索引的类型。我们将该类型称为 Mat n m。函数 identity 接受一个自然数 n 作为参数，产生一个 n x n 的单位矩阵，该函数的类型为 identity : (n : Nat) -> (Mat n n)。

注意：我们当然可以将 identity 函数的类型指定为 Nat -> Nat -> Mat，其中 Mat 为矩阵类型，不过它没有依赖类型版本的那么精确。

使用依赖类型的优势在于它能在类型系统中表达程序的性质。前面我们还看到它能表示边长为 n 的方阵，它也能定义矩阵运算的类型，保证其长度正确。例如，矩阵乘法的类型为：

∀ {i j k} → (Mat i j) -> (Mat j k) -> (Mat i k)

而类型系统可以确保执行矩阵乘法的程序确实接受了大小正确的参数。它也能够确保矩阵乘法只能应用于第一个参数的列数等于第二个参数的行数的矩阵。

依赖类型与逻辑¶

感谢`柯里-霍华德对应 <http://en.wikipedia.org/wiki/Curry_Howard>`_，我们可以用依赖类型表达逻辑规范。只使用类型，我们就能定义

自然数的相等性
算术运算的性质
与模算术中计算原根的函数一致的类型 (n : Nat) -> (PrimRoot n)

当然，与类型为 Nat -> Nat 的，产生一个自然数原根的程序相比，拥有上面类型的程序会更加难写。然而，这种困难换来的是保证程序能够工作：它不会产生不是原根的结果。

从更加数学的层面来说，我们可以表达公式并用算法证明它们。例如，一个类型为 (n : Nat) -> (PrimRoot n) 的函数也是每个自然数都有一个原根的证明。