Agda

概述

Agda 是一门依赖类型的纯函数式编程语言，同时也是交互式定理证明助手，主要由瑞典查尔姆斯理工大学的研究者开发，现行版本通常称 Agda 2。

原理

Agda 建立在 Martin-Löf 直觉主义类型论之上。依据 Curry-Howard 同构，命题即类型、证明即程序：编写一个类型正确的程序，就等价于给出该命题的构造性证明。Agda 要求所有函数是全函数（total），并通过终止性检查保证一致性。

特性

Agda 支持归纳族（inductive families）、依赖模式匹配、混合位缀（mixfix）语法和 Unicode 标识符，配合 Emacs 或 VS Code 插件可进行交互式的「填洞」式证明开发。

应用

Agda 广泛用于类型论教学与编程语言元理论研究，《Programming Language Foundations in Agda》是代表性教材。