Agda编译器如何决定编译内容？对比Coq的逻辑与计算分层

Great question! Unlike Coq which enforces an explicit split between Prop (proof layer, erased during compilation) and Set (computational layer, retained), Agda uses a combination of explicit annotations and type system inference to distinguish content that affects runtime behavior from content that's only needed for type checking. Here's a breakdown:

1. Explicit Irrelevance Annotations #

Agda lets you mark terms, variables, or types as irrelevant (meaning they don't contribute to runtime computation) using the @0 annotation (older versions used .). The compiler will automatically erase any content marked this way.

For example, if you have a function that requires a proof of commutativity to satisfy type constraints, but doesn't use that proof in its runtime logic:

module Example where
open import Data.Nat
open import Relation.Binary.PropositionalEquality

-- The proof parameter is marked @0, so it gets erased at compile time
plus-comm-apply : @0 (n m : ℕ) → (plus n m ≡ plus m n) → ℕ → ℕ
plus-comm-apply _ _ _ x = x + 5

Here, the proof argument and the n/m parameters are marked irrelevant—they're only there to pass type checking, so the compiler discards them entirely when generating code for target languages like Haskell or JavaScript.

2. Automatic Inference of Proof Irrelevance #

Agda's type system automatically recognizes certain types as propositional—types where all inhabitants are considered equivalent (like equality _≡_, or logical negation ¬_). For terms of these types, the compiler treats them as irrelevant by default, even without explicit annotations.

Suppose you write a function that uses an equality proof to rewrite a term during type checking, but doesn't reference the proof at runtime:

rewrite-example : (x y : ℕ) → x ≡ y → ℕ
rewrite-example x y eq = x + 3  -- eq is used only for type-level rewriting

The eq parameter will be erased automatically, because Agda knows it's a proof of an equality proposition—its specific value doesn't affect the runtime result.

3. Runtime Relevance Analysis #

Beyond annotations and propositional types, Agda's compiler performs a relevance analysis to determine which terms are actually used in runtime computation. If a term is only referenced in type-level contexts (and never in code that affects the output), it gets erased.

For example, even if you forget to mark a proof parameter as irrelevant, if the function body never uses it (beyond satisfying type constraints), the compiler will still discard it. This is similar to how dead code is eliminated in traditional compilers, but tailored to dependent types.

4. Flexibility vs. Explicitness #

The key difference from Coq is that Agda's approach is more flexible: you're not locked into a fixed Prop/Set divide. You can mark arbitrary terms as irrelevant (not just proofs), and the compiler infers much of this automatically. This lets you fine-tune what gets compiled without being constrained by a rigid logical/computational split.

内容的提问来源于stack exchange，提问作者MrO