Agda安全模式下的限制与规范详解

Agda作为一款依赖类型理论的形式化验证工具，其安全模式（--safe）为确保证明可靠性提供了严格的编译时检查机制。本文将系统梳理安全模式下的各项限制规范，帮助开发者理解该模式的设计哲学和实际约束。

核心安全原则

安全模式的核心目标是确保所有证明均通过构造性手段完成，禁止任何可能破坏类型安全或逻辑一致性的语言特性。该模式下，Agda会强制禁用以下三类特性：

1. 非构造性逻辑元素

   • 禁止使用postulate声明未经验证的假设
   • 禁用primTrustMe等可能破坏等式推理的原始操作

2. 元编程与编译控制

   • 禁止COMPILE指令等代码生成相关特性
   • 禁用INJECTIVE等影响类型检查行为的编译指示

3. 验证绕过机制

   • 禁止终止性检查绕过（TERMINATING/NON_TERMINATING）
   • 禁用一致性检查豁免（NO_POSITIVITY_CHECK/NO_UNIVERSE_CHECK）

典型受限场景

当启用安全模式时，以下常见操作将触发编译错误：

• 尝试使用{-# TERMINATING #-}标记非终止函数
• 使用{-# NON_TERMINATING #-}规避终止性验证
• 通过{-# NO_UNIVERSE_CHECK #-}绕过宇宙层级约束
• 声明未实现的核心函数（primitive）

设计意义

这些限制共同确保了：

1. 所有证明都基于有效的构造性证据
2. 类型系统的一致性不会被破坏
3. 程序行为具有可靠的数学基础

开发者应将这些约束视为形式化验证的质量保证机制，而非功能限制。对于需要特定编译指示的场景，建议通过修改证明策略而非禁用检查来实现目标。