Agda User Manual v2.6.1

• 语言: 英语
• 格式: .epub
• 来源: agda.readthedocs.io

摘要

《Agda User Manual v2.6.1》是Agda编程语言的用户手册，介绍了Agda语言及其类型检查、编译和编辑系统的使用。手册还提供了贡献指南、文档编写说明以及如何使用Agda的工具和资源的信息。文档特别提到了Agda 2.6.1版本的新特性，包括对累加性（cumulativity）的支持，并详细说明了如何编写和测试文档中的代码示例。

AI总结

《Agda 用户手册 v2.6.1》是 Agda 编程语言的官方文档，介绍了 Agda 的类型检查、编译和编辑系统及相关工具的使用方法。以下是文档的核心内容总结：

### 1. **概述**
- **Agda** 是一个支持依赖类型的编程语言，结合了类型理论和编程语言的特性。
- 该手册是仍在进行中的工作，尚未完成，欢迎通过 GitHub 提交贡献和修正。

### 2. **新特性**
- **版本 2.6.1** 引入了**可选累加性宇宙（Cumulativity）**，默认情况下可以通过 `--cumulativity` 标志启用。
- 累加性规则：`Set i <; Set j` 当 `i < j` 时成立，例如 `Nat : Set`、`Nat : Set₁` 以及 `Nat : ∀ {i} → Set i`。
- 累加性启用后，可以简化高层宇宙的实现，例如 `lift : ∀ {a b} → Set a → Set (a ⊆ b)` 可以直接定义为 `lift x = x`。

### 3. **核心语言功能**
- **多 arity 函数**：在 Agda 早期版本中，定义多 arity 函数较为复杂，需要处理宇宙层级的问题。启用累加性后，可以简化为使用最高层级的宇宙，例如：

  N-ary : ∀ {ℓ₁ ℓ₂} n → Set ℓ₁ → Set ℓ₂ → Set (N-ary-level ℓ₁ ℓ₂ n)
  N-ary zero A B = B
  N-ary (suc n) A B = A → N-ary n A B

### 4. **工具与环境**
- **文档渲染**：支持本地渲染文档，需安装 Python 3.3+、Sphinx 和 LaTeX。
- **代码检查**：通过 `make user-manual-test` 可以检查文档中的所有代码示例是否正确。
- **编辑器支持**：在 Emacs 中使用 `agda2-mode` 可以交互式地编写和检查代码。

### 5. **安装与入门**
- **安装**：可以从 Hackage 安装预构建包，或从 GitHub 克隆开发版本。
- **入门**：包含“Hello World”示例、快速上手指南以及多篇教程，适合新手。

### 6. **语言参考**
- **基本语法**：包括数据类型定义、函数定义、隐式参数、局部定义（`let` 和 `where`）等。
- **高级特性**：支持积模式（copatterns）、互递归、模式同义词、注入性类型构造器等。

### 7. **错误与警告**
- 新增选项如 `--allow-incomplete-matches` 和 `--allow-unsolved-metas`，允许忽略不完整的模式匹配或未解决的元变量。
- 可通过选项禁用积极性检查（`--no-positivity-check`）和终止性检查（`--no-termination-check`）。

### 8. **贡献指南**
- Agda 和其相关库托管在 GitHub 上，贡献者需 fork 仓库、提交修改并创建 pull request。
- 文档编写采用 reStructuredText 格式，需遵循代码规范并清理尾随空格。

### 9. **其他资源**
- **Agda Wiki** 提供丰富的教程、介绍、出版物和书籍，适合深入学习。
- **工具支持**：包括 Agda 编辑器、编译器、反编译器等。

### 总结
Agda 是一个功能强大的依赖类型编程语言，v2.6.1 版本引入了累加性宇宙等重要特性，简化了高层宇宙的处理。文档提供了从安装到高级功能的全面指导，并鼓励社区参与贡献。对于新手，可以从“Getting Started”和 Agda Wiki 入手，熟悉语言的基本用法和工具支持。