Coding Poet, Coding Science

Agda语言介绍

发表于 | 更新于 | 分类于 | |

Agda语言是使用了依存类型的函数式编程语言。最初发表于2007年，是在Ulf Norell的博士论文里面。目前实践当中，函数式语言中使用依存类型还不多。但是依存类型在可以预见的未来内会继续发展。目前发展依存类型的函数式语言的动力在于形式证明。目前的版本是Agda2，基本上是重写了。Agda2不像Coq的地方在于，Agda没有对于tactics与函数式proofs的支持。Agda 2语言有对于数据类型、模式匹配、记录、模块、Haskell语法的支持。Agda 2是基于Zhaohui Luo的UTT类型理论，与Martin-L"of类型理论（也就是直觉类型论）有一点的不同。

Agda的值得提及的特性有归纳类型定义（这在Coq中也存在）、依存类型的模式匹配机制（允许在依存类型系统下使用模式匹配）、元变量（允许变量在运行的时候被细化和修改，因此支持程序在运行的时候增量构造，部分代替了tactics在Coq中的作用）、证明自动化（通过反射实现，以及允许程序在5s内枚举可能的证明），以及终止检查（因为Agda是一个完全的语言，能够保证每个程序都必然终止，以此保证语言的一致性，借助于Foetus termination checker实现终止检查）。

Agda和Coq等“后现代的编程语言”一样，对Unicode的变量支持很好。（相比之下，我们认为Haskell、Scala是属于所谓的现代编程语言）。Agda支持三种编译器后端：MAlonzo（输出Haskell）、JavaScript后端，以及Epic后端。关于Agda的论文与理论研究在这里自己就不总结了。

Agda语言的安装是比较简单的。可以直接在ubuntu下面使用apt-get安装。但是建议的安装方式是使用hackage的cabal install agda，因为它是用Haskell写成的。

自己学习Agda目前主要是根据《Dependently Typed Programming in Agda》http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf。里面强调的是其依存类型的风格。Hindley-Milner风格的编程语言如Haskell与ML中，类型与值之间存在明显的分割。两者是互不相关的。但是在依存类型当中，值与类型是相互关联的。函数可以根据值返回不同的类型，但是又不同于动态类型的语言。

在Agda的理解中，典型的依存类型是\(n\)-维向量。若把不同的\(n\)-维向量看成是不同的，那么向理的类型必然依赖于参数\(n\)。C++的模块编程支持这种\(n\)维向量的风格，但是在Hindley-Milner的类型系统中，区别似乎是有些困难。通过这个例子可以看出，依存类型系统会更精细，而且也有可能为C++的模块机制提供一个理论基础。

依存类型在定理证明中的可能的作用是：值的属性当成是一个元素为使得证明的属值为真的那些类型。这样，依存类型的编程语言可以当成是逻辑语言使用。

Agda语言的每个源文件都由一个顶层的模块名称声明开始。此外，agda使用的扩展名是lagda，表示的是agda源文件里面支持了文学编程（其实我们也可以把文学编程看成是后现代编程语言的一种特性，Haskell就具有这个特性）。Agda的文件名与模块名保持一致（像Java那样）。

Agda与Haskell与ML一样，支持对代数数据类型进行模式匹配（但是一般介绍Agda语言的书中，刚开始的时候还是介绍简单类型的函数式数据类型的匹配，而把依存类型的匹配规则放在最后）。数据类型使用data关键字来声明。比如声明一个布尔类型为：

data Bool : Set where
    true  : Bool
    false : Bool

声明中，Bool的类型是Set，Set是小类型的类型（因为Agda支持把Set这个类型当成是Set1的一个元素，也就是支持层次化类型）。此外，Agda的函数定义语法（不动点定义）与Haskell也是很像的，比如Bool的not函数：

not : Bool -> Bool
not true = false
not false = true

不过，not的类型声明其实不是必须的。

另外一种定义是采用归纳定义一个类型定义，比如自然数的定义：

data Nat : Set where
    zero : Nat 
    succ : Nat -> Nat
_+_ : Nat -> Nat -> Nat
zero + m = m
succ n + m = succ (n + m)
_*_ : Nat -> Nat -> Nat
zero * m = zero
succ n * m = m + n * m

这种定义是允许的，但是为了保证合理性，应该加上一个n < succ n的断言。

甚至函数的定义也是基于模式匹配的，比如定义if_then_else为：

if_then_else_ : {A: Set} -> Bool -> A -> A -> A
if true then x else y = x
if false then x else y = y

这样我们就定义了一个if_then_else函数，而且可以把变量加在中间。如果需要声明中缀函数，以及指定中缀函数的优先级，可以使用infixr关键字。另外，像Haskell与ML一样，Agda允许含参数据类型，如：

infixr 40 _::_
data List (A : Set) : Set where
    [] : List A
    _::_ : A -> List A -> List A

上面的List是一个含参类，除此之外，由于Unicode特性，变量可以包含任何的符号。

Agda的依存类型的函数

Agda的依存类型的函数的声明并不特别之处，也是使用(x:A)->B来声明这个变量。不过，由于指定了变元x，所以类型B是可以包含x作为变量的。此外，由于Agda的类型层次结构，所以一个类型的元素也可以是一个类型。

identity : (A : Set ) -> A -> A
identity A x = x
zero' : Nat
zero' = identity Nat zero

上面的函数接受类型\(A\)以及类型\(A\)的一个元素为参数，然后返回相应的元素。再来一个非平凡的例子，这个例子创建了一个apply函数：

apply : (A : Set)(B : A -> Set) ->
    ((x : A) -> B x) -> (a : A) -> B a
apply A B f a = f a

对于依存函数类型，有一些简便的记法可以使用，比如

(x : A)(y : B) -> C for (x : A) -> (y : B) -> C
(x y : A) -> B for (x : A)(y : A) -> B

具体的运算，可能要参考依存类型\(\lambda\)-演算来解决。函数式语言在处理可选参数的上面可能没有一些命令式语言直观。但是Agda提供了缺省参数的情况，这样一个函数可以应用在不同参数数目的场合。

Agda使用如下的方式声明\(n\)-维向量：

data Vec (A : Set) : Nat -> Set where
    []   : Vec A zero
    _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

上式表示Vec A是一个Nat->Set的映射，所以Vec A n得到一个具体的类型。

个人感觉，Agda的设计体现了对模式匹配与类型系统的大的发展。我们可以参考一下。这样我们遇到再奇怪的编程语言的时候也就不再感到奇怪了。Agda还可以导入Haskell的模块。agda的输入输出也是基于单体的。

Agda的文学化编程

Agda的文学化编程与Latex是类似的。不过agda程序可以使用–latex来输出一个tex文档，这样的话，可以实现许多的排版的功能。文学编程功能与Haskell是一样的。

lagda可以看成是一个.lhs文件，它可以由lhs2tex来处理。

agda的vim高亮可以参考https://github.com/derekelkins/agda-vim.git。

http://stevebob.net/agda-environment/上介绍了Agda的入门程序。包括在ubuntu下面安装一直到使用。

编译agda的时候，要想连接到相应的库，使用

agda -c -i /usr/share/agda-stdlib -i . hello.agda

agda的编译器是通过调用Haskell来实现的。

http://blog.oxij.org/2011/12/22/howto-get-started-with-agda/上介绍了怎样开始Agda。不过是2011年的。关键的不是自己写出来一个Hello World，而是怎样让别人在网上写的复杂的教程，或者是一个实际的工程在自己的计算机上跑起来。写这篇博文的是教本科生Haskell的老师。但是作者也想利用Agda。看起来，研究生的阶段不是学习Agda，而是真正地理解其背后的依存类型、归纳数据类型等的原理与实现。（其实自己理想中，所有的形而上学的知识都应该是在大学完成的。但是很多时候，研究生的阶段我们尚未完成）。作者那个时候也认为，本科生理解Agda是几乎不可能的。

作者对于高级编程语言的看法：

Advanced programming language requires advanced tools.

比如说，有企业级的开发环境（IDE、自动编译、调试、符号表查找、版本控制）。此外，也可以是最简单的一个文本编辑器。

不过，Agda的程序比较特殊，通常这些代码并不运行，甚至不进行编译，我们只是想对它们进行类型检查。对于Agda来说，调试也是没有用的。也根本没有调试器。

此外，为了使用Agda，还得有一种方便的方式输入Unicode字符。不过，大部分编辑器中，实现这个功能可能是非常复杂的。

写Agda代码也会不同于以往，因为一般有的时候，一天也写不到25行Agda代码。因为需要Unicode，而且目前Agda提供的也只有Emacs，所以不会Emacs就已经把大部分的程序员阻止在外了。

确保安装了如下的程序：

cabal install agda
## 打开软件包，并安装agda-libs cabal install
cabal install Agda-executable

然后配置~/.emacs文件：　

(load-file (let ((coding-system-for-read 'utf-8))
    (shell-command-to-string "agda-mode locate")))

打开emacs，使用C-x C-f打开一个编辑的文档。配置Emacs环境的方法有很多。但是必须在Emacs下面工作不可。否则，是没法写出合法的Agda代码的。

Agda程序写出来有什么样的作用：其实跟Haskell差不多，Agda程序也从Main开始。

Agda的用法[06-30-2015 16:46:01]

Agda的一种用法是作为一个交互式的定理编辑器，或者说辅助定理证明器。不过，其实没有意义，是因为这些应用中，看不到使用它们证明了什么样的数学的定理。所以，感觉好像真的是没有什么用途。