Agda 2.8.0 候选版本发布：迈向自包含二进制与增强功能

Agda 是一个基于 Haskell 开发的依赖类型函数式编程语言和证明辅助工具，它结合了编程语言的形式化验证能力与数学证明的表达力。最新发布的 2.8.0 候选版本（RC1）带来了多项重要改进，标志着 Agda 在用户体验和功能扩展方面迈出了重要一步。

自包含二进制与安装优化

2.8.0 版本最显著的改变是 Agda 现在成为一个完全自包含的单一二进制文件。这一架构变革意味着：

1. 移除了独立的 agda-mode 可执行文件，其功能已整合到新的 --emacs-mode 选项下
2. 所有数据文件（包括原始模块、HTML/LaTeX 后端补充、JS/GHC 后端运行时等）现在都内置于二进制文件中
3. 首次运行时会在用户目录（Unix 系统默认为 ~/.local/share/agda）自动生成所需文件

这种设计简化了安装流程，使 Agda 更易于分发和部署。对于打包维护者而言，虽然需要调整打包流程，但整体复杂度实际上是降低了。

构建系统与库管理增强

新版本引入了 --build-library 标志，这是一个革命性的功能，允许开发者一键构建整个 Agda 库。该功能会：

1. 从当前目录开始查找 .agda-lib 文件
2. 提取其中的 include 目录配置
3. 递归扫描这些目录下的所有 Agda 文件
4. 统一检查所有这些文件

这大大简化了大型项目的构建流程，特别是对于包含多个相互依赖模块的代码库。

语言特性与语法扩展

极性注解实验支持

通过新的 --polarity 标志，开发者可以尝试实验性的极性注解功能。极性注解允许更精细地控制类型参数的变体行为，例如：

data Mu (F : @++ Set → Set) : Set where
  fix : F (Mu F) → Mu F

其中 @++ 注解表示正极性，帮助类型检查器验证递归类型的合法性。

记录构造器引用

现在即使没有显式命名记录类型的构造器，也可以通过 (Record name).constructor 语法引用它，解决了长期存在的构造器访问痛点。

模式匹配增强

let 表达式中的函数绑定现在支持更丰富的模式匹配形式，与 λ 表达式和函数类型中的模式保持一致：

let
  f : A → B → C
  f p1 p2 = ...
in ...

编译器与后端改进

JavaScript 后端现在支持 ES6 模块语法（通过 --js-es6 标志），使 Agda 代码能更好地与现代 JavaScript 生态系统集成。同时移除了不再必要的未使用参数优化，提高了编译可靠性。

错误处理与警告系统

错误消息格式现在遵循 GNU 标准，采用更规范的输出格式：

sourcefile:line1.column1-line2.column2: error: [ErrorName]
error message
when error context

新增了多种警告类型，包括：

• 无效显示格式警告（InvalidDisplayForm）
• 未使用变量警告（UnusedVariablesInDisplayForm）
• 无用战术属性警告（UselessTactic）
• 多余极性注解警告（TooManyPolarities）

元编程与反射

新增了 checkFromStringTC 原语，允许在反射期间解析和类型检查字符串形式的代码，为元编程提供了更强大的工具：

checkFromStringTC : String → Type → TC Term

性能优化

实例搜索性能得到显著提升，通过限制判别树的深度和早期丢弃含有可见参数的候选者，减少了不必要的计算开销。同时，具体名称的范围查找也进行了专门优化。

开发工具链

项目现在支持 GHC 8.8.4 到 9.12.2 的编译器版本，移除了对 GHC 8.6 的支持。新增了 dump-core Cabal 构建标志，方便开发者分析优化后的 GHC Core 代码，有助于性能调优。

这个候选版本标志着 Agda 向更稳定、更易用的方向迈进，特别是自包含二进制的设计将极大简化安装和部署流程，为更广泛的采用铺平道路。极性注解等新特性则为高级类型系统编程开辟了新的可能性。