Agda User Manual v2.6.1

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

摘要

该文档是Agda编程语言的用户手册（版本2.6.1），由Agda团队于2020年3月16日发布。手册涵盖了Agda的概述、入门指南、语言参考和工具选项。语言参考部分详细介绍了抽象定义、内置类型、共归纳、共模式、核心语言、立体类型、累积性、数据类型、平直模态、外部函数接口、函数定义、函数类型、声明变量泛化、隐式参数、实例参数、无关性、Lambda抽象、局部定义、词法结构、字面量重载、混合修复运算符、模块系统、互递归、模式同义词、正性检查、假设等特性。手册还包含运行时的无关性注解、重写规则、选项设置、错误和警告处理以及模式匹配和等式相关内容。工具部分包括命令行选项和编辑指南。

AI总结

《Agda用户手册 v2.6.1》主要内容总结如下：

**一、概述**
Agda是一种依赖类型函数式编程语言，支持交互式开发、类型检查和编译。该手册是官方文档，目前仍在完善中，欢迎贡献。

**二、入门指南**
- **安装**：可通过源码或包管理器安装，支持macOS、Linux等系统。安装时可使用`cpphs`、`debug`等标志。
- **Hello World**：在`hello-world.agda`文件中定义模块，导入`IO`库，通过`main = run (putStrLn "Hello, World!")`实现输出。编译命令为`agda --compile hello-world.agda`。
- **编辑与检查**：常用Emacs或Atom编辑器。支持交互式开发，通过`?`占位符创建“洞”，可查看目标类型、上下文等。快捷键包括`C-c C-l`加载、`C-c C-,`查看目标类型等。

**三、语言参考（核心特性）**
- **抽象定义、内置类型、共归纳、共模式、核心语言、立方类型、累积性、数据类型、平面模态、外部函数接口、函数定义与类型、变量泛化、隐式参数、实例参数、无关性、Lambda抽象、局部定义、词法结构、字面量重载、混合运算符、模块系统、互递归、模式同义词、正性检查、公设**等。
- **重写规则**：支持通过`--confluence-check`检查局部合流性。可通过`BUILTIN REWRITE`注册自定义重写关系。
- **运行时无关性（v2.6.1新特性）**：使用`@0`或`@erased`标记参数，这些参数在运行时被擦除。例如，向量的长度参数可标记为擦除，编译后不再存在。高阶函数的擦除参数会被替换为占位符`_`，优化性能。

**四、工具与选项**
- **命令行选项**：包括`--safe`（禁用公设等）、`--cubical`（启用立方类型）、`--rewriting`（启用重写规则）、`--without-K`（禁用K公理）、`--no-eta-equality`（禁用记录η等式）等。
- **调试与打印**：支持`--no-unicode`、`--show-implicit`、`--verbose`等。
- **模式匹配与等式**：支持`--exact-split`、`--no-flat-split`、`--keep-pattern-variables`（v2.6.1新特性，防止交互式case split替换变量为点模式）等。
- **错误与警告**：支持`--allow-incomplete-matches`、`--allow-unsolved-metas`、`--no-positivity-check`、`--no-termination-check`、`--warning`等。

**五、贡献与文档**
- 项目托管在GitHub，可通过fork和PR贡献。文档使用reStructuredText格式，位于`doc/user-manual`目录，可本地构建（需Python、Sphinx、LaTeX）。
- 鼓励贡献者关注`difficulty: easy`和`help wanted`标签的问题。