agda 编译器如何确定要编译的内容？

Question

在Coq中，明确了什么来自逻辑世界（Prop），什么来自计算世界（Set）。证明世界为计算世界提供保证，并且是唯一需要编译的世界。

在Agda中没有明显的区别所以我想知道：

Agda编译器如何决定什么需要编译，什么需要留下？

谢谢。

Answer 1

更新：我在 readthedocs.io 添加了与新用户手册无关的文档。

在 Agda 中，您可以用点将函数参数标记为不相关，这意味着该参数将只进行类型检查，而不会进行评估。例如，您可以按如下方式定义排序列表（来自 wiki）：

  data SList (bound : ℕ) : Set where
    []    : SList bound
    scons : (head : ℕ) →
          .(head ≤ bound) →        -- note the dot!
          (tail : SList head) →
          SList bound

证明head ≤ bound前面有一个点，所以它会被擦除（在编译时和运行时）。

除了明确的不相关注释外，Agda 编译器还有许多优化可以在没有任何用户干预的情况下删除未使用的参数，例如 this paper.

的强制优化

agda 编译器如何确定要编译的内容？

How does agda compiler figure out what to compile?

compiler-construction

agda