Run-time Irrelevance

From version 2.6.1 Agda supports run-time irrelevance (or erasure) annotations. Values marked as erased are not present at run time, and consequently the type checker enforces that no computations depend on erased values.

Syntax

A function or constructor argument is declared erased using the @0 or @erased annotation. (These annotations may only be used if the option --erasure is active.) For example, the following definition of vectors guarantees that the length argument to _∷_ is not present at runtime:

  1. data Vec (A : Set a) : @0 Nat → Set a where
  2.   []  : Vec A 0
  3.   _∷_ : ∀ {@0 n} → A → Vec A n → Vec A (suc n)

The GHC backend compiles this to a datatype where the cons constructor takes only two arguments.

Note

In this particular case, the compiler identifies that the length argument can be erased also without the annotation, using Brady et al’s forcing analysis [1]. Marking it erased explictly, however, ensures that it is erased without relying on the analysis.

Note

If --erasure is used, then parameters are marked as erased in the type signatures of constructors and record fields, even if the parameters are not marked as erased in the data or record type’s telescope, with one exception: for indexed data types this only happens if the --with-K flag is active.

Erasure annotations can also appear in function arguments (both first-order and higher-order). For instance, here is an implementation of foldl on vectors:

  1. foldl : (B : @0 Nat → Set b)
  2.       → (f : ∀ {@0 n} → B n → A → B (suc n))
  3.       → (z : B 0)
  4.       → ∀ {@0 n} → Vec A n → B n
  5. foldl B f z []       = z
  6. foldl B f z (x ∷ xs) = foldl (λ n → B (suc n)) (λ {n} → f {suc n}) (f z x) xs

Here the length arguments to foldl and to f have been marked erased. As a result it gets compiled to the following Haskell code (modulo renaming):

  1. foldl f z xs
  2.   = case xs of
  3.       []     -> z
  4.       x ∷ xs -> foldl f (f _ z x) xs

In contrast to constructor arguments, erased arguments to higher-order functions are not removed completely, but instead replaced by a placeholder value _. The crucial optimization enabled by the erasure annotation is compiling λ {n} → f {suc n} to simply f, removing a terrible space leak from the program. Compare to the result of compiling without erasure:

  1. foldl f z xs
  2.   = case xs of
  3.       []     -> z
  4.       x ∷ xs -> foldl (\ n -> f (1 + n)) (f 0 z x) xs

It is also possible to mark top-level function definitions as erased. This guarantees that they are only used in erased arguments and can be useful to ensure that code intended only for compile-time evaluation is not executed at run time. (One can also use erased things in the bodies of erased definitions.) For instance,

  1. @0 spec : Nat → Nat   -- slow, but easy to verify
  2. impl    : Nat → Nat   -- fast, but hard to understand
  3. proof   : ∀ n → spec n ≡ impl n

Erased record fields become erased arguments to the record constructor and the projection functions are treated as erased definitions.

Constructors can also be marked as erased. Here is one example:

  1. Is-proposition : Set a → Set a
  2. Is-proposition A = (x y : A) → x ≡ y
  4. data ∥_∥ (A : Set a) : Set a where
  5.   ∣_∣        : A → ∥ A ∥
  6.   @0 trivial : Is-proposition ∥ A ∥
  8. rec : @0 Is-proposition B → (A → B) → ∥ A ∥ → B
  9. rec p f ∣ x ∣           = f x
  10. rec p f (trivial x y i) = p (rec p f x) (rec p f y) i

In the code above the constructor trivial is only available at compile-time, whereas ∣_∣ is also available at run-time. Clauses that match on erased constructors in non-erased positions are omitted by (at least some) compiler backends, so one can use erased names in the bodies of such clauses. (There is an exception for constructors that were not originally declared as erased, but that are currently treated as erased.)

One can also mark data and record types as erased. Such types can only be used in erased positions, their constructors and projections are erased, and definitions in record modules for erased record types are erased. A data or record type is marked as erased by writing @0 or @erased right after the data or record keyword of the data or record type’s declaration:

  1. data @0 D₁ : Set where
  2.   c : D₁
  4. data @0 D₂ : Set
  6. data D₂ where
  7.   c : D₁ → D₂
  9. interleaved mutual
  11.   data @0 D₃ : Set where
  13.   data D₃ where
  14.     c : D₃
  16. record @0 R₁ : Set where
  17.   field
  18.     x : D₁
  20. record @0 R₂ : Set
  22. record R₂ where
  23.   field
  24.     x : R₁

Finally one can mark modules as erased. The module identifier itself does not become erased, but all definitions inside the module. A module is marked as erased by writing @0 or @erased right after the module keyword:

  1. module @0 _ where
  3.   F : @0 Set → Set
  4.   F A = A
  6. module M (A : Set) where
  8.   record R : Set where
  9.     field
  10.       @0 x : A
  12. module @0 N (@0 A : Set) = M A
  14. G : (@0 A : Set) → let module @0 M₂ = M A in Set
  15. G A = M.R C
  16.   module @0 _ where
  17.     C : Set
  18.     C = A

Rules

The typing rules are based on Conor McBride’s “I Got Plenty o’Nuttin’” [2] and Bob Atkey’s “The Syntax and Semantics of Quantitative Type Theory” [3]. In essence the type checker keeps track of whether it is running in run-time mode, checking something that is needed at run time, or compile-time mode, checking something that will be erased. In compile-time mode everything to do with erasure can safely be ignored, but in run-time mode the following restrictions apply:

  • Cannot use erased variables or definitions.

  • Cannot pattern match on erased arguments, unless there is at most one valid case. If --without-K is enabled and there is one valid case, then there are further restrictions:

    • The constructor’s data or record type must not be indexed.

    • If the type is anything but a record type with η-equality, then the option --erased-matches must be enabled.

Consider the function foo taking an erased vector argument:

  1. foo : (n : Nat) (@0 xs : Vec Nat n) → Nat
  2. foo zero    []       = 0
  3. foo (suc n) (x ∷ xs) = foo n xs

This is okay (when the K rule is on), since after matching on the length, the matching on the vector does not provide any computational information, and any variables in the pattern (x and xs in this case) are marked erased in turn. On the other hand, if we don’t match on the length first, the type checker complains:

  1. foo : (n : Nat) (@0 xs : Vec Nat n) → Nat
  2. foo n []       = 0
  3. foo n (x ∷ xs) = foo _ xs
  4. -- Error: Cannot branch on erased argument of datatype Vec Nat n

The type checker enters compile-time mode when

  • checking erased arguments to a constructor, function or module application,

  • checking the body of an erased definition (including an erased module application),

  • checking the body of a clause that matches (in a non-erased position) on a constructor that was originally defined as erased (it does not suffice for the constructor to be currently treated as erased),

  • checking the domain of an erased Π type, or

  • checking a type, i.e. when moving to the right of a :, with some exceptions:

    • Compile-time mode is not entered for the domains of non-erased Π types.

    • If the K rule is off then compile-time mode is not entered for non-erased constructors (of fibrant type) or record fields.

Note that the type checker does not enter compile-time mode based on the type a term is checked against (except that a distinction is sometimes made between fibrant and non-fibrant types). In particular, checking a term against Set does not trigger compile-time mode.

There is also a hard compile-time mode. In this mode all definitions are treated as erased. The hard compile-time mode is entered when an erased definition is checked.

The type-checker switches from compile-time mode to run-time mode for certain expressions/declarations if it is not in the hard compile-time mode:

  • Absurd lambdas.

  • Non-erased pattern-matching lambdas.

  • Non-erased module definitions (”module M … = …”) or applications (”M …”).

  • Applications of ♯ (see Old Coinduction).

Note

The text above should be extended with information about how the reflection machinery interacts with run-time irrelevance.

References

[1] Brady, Edwin, Conor McBride, and James McKinna. “Inductive Families Need Not Store Their Indices.” International Workshop on Types for Proofs and Programs. Springer, Berlin, Heidelberg, 2003.

[2] McBride, Conor. “I Got Plenty o’Nuttin’.” A List of Successes That Can Change the World. Springer, Cham, 2016.

[3] Atkey, Robert. “The Syntax and Semantics of Quantitative Type Theory”. In LICS ‘18: Oxford, United Kingdom. 2018.