Opaque definitions

Opaque definitions are a mechanism for controlling unfolding of Agda definitions, to help with both goal readability and performance. Like abstract definitions, opaque definitions will not unfold in general, but unlike abstract definitions, opacity can be selectively controlled at use-sites.

Our implementation of unfolding control is based on the theory introduced by Gratzer et. al. in Controlling unfolding in type theory, but handled entirely at the elaborator level, without a dependency on our (cubical) extension types.

Overview

• Functions (and primitive functions) can be marked opaque. Outside of opaque blocks, these behave like postulates.

• Opaque blocks, even in unrelated modules, can have unfolding clauses, which allow the user to list their choice of names that should be locally treated as transparent.

• Opaque definitions do not reduce in type signatures, even inside opaque blocks where they would otherwise be unfolded.

Unfolding opaque definitions

Consider an implementation of the integers as an abstract setoid: The underlying representation is given by pairs of natural numbers, representing a difference, but day-to-day, we would like to treat ℤ as its own type.

Our core module might define these operations:

module Integer where
  opaque
    ℤ : Set
    ℤ = Nat × Nat
    _≡ℤ_ : (x y : ℤ) → Set
    (p , n) ≡ℤ (p' , n') = (p + n') ≡ (p' + n)
    infix 10 _≡ℤ_
    0ℤ : ℤ
    0ℤ = 0 , 0
    1ℤ : ℤ
    1ℤ = 1 , 0
    _+ℤ_ : (x y : ℤ) → ℤ
    (p , n) +ℤ (p' , n') = (p + p') , (n + n')
    _*ℤ_ : (x y : ℤ) → ℤ
    (a , b) *ℤ (c , d) = ((a * c) + (b * d)) , ((a * d) + (b * c))
    infixl 20 _+ℤ_
    infixl 30 _*ℤ_
    -ℤ_ : ℤ → ℤ
    -ℤ (p , n) = (n , p)

We’d now like to prove that the integers form a ring, under the _≡ℤ_ notion of equality. Some of the equations on natural numbers involved are pretty nasty, though, so this would be very hard to do without a solver for semiring equations. However, such a solver would also depend on reflection machinery, bloating the dependency tree of the Integer module for people who do not care about it provably forming a ring.

Fortunately, since ℤ is opaque rather than abstract, a different module, say Integer-ring, can provide its own proofs, in an opaque block that unfolds the definition of ℤ:

module Integer-ring where
  open Integer
  opaque
    unfolding ℤ
    distlℤ : ∀ x y z → x *ℤ (y +ℤ z) ≡ℤ x *ℤ y +ℤ x *ℤ z
    distlℤ (a , b) (c , d) (e , f) = use-nat-solver where postulate
      use-nat-solver
        : a * (c + e) + b * (d + f) + (a * d + b * c + (a * f + b * e))
        ≡ a * c + b * d + (a * e + b * f) + (a * (d + f) + b * (c + e))

Since the definition of distlℤ is in an opaque block with an unfolding ℤ clause, it sees through the opacity of ℤ, and of all names unfolded by ℤ’s opaque block (see below).

What actually unfolds?

When an opaque block is checked, Agda will compute ahead-of-time the set of names it is allowed to unfold. This set is per-block, not per-definition. An unfolding clause, if it mentions opaque names, will cause the unfolding sets associated with those names to be added to the current block.

The following illustrates the behaviour of these rules:

• Unfolding any name in an opaque block will cause any of the other names in that block to be unfolded as well. Example:

  module _ where private
    opaque
      x : Nat
      y : Nat
      x = 3
      y = 4
    opaque
      unfolding x
      _ : y ≡ 4
      _ = refl

  Here, even though only x was asked for, y is also available for unfolding.

• Since the unfolding sets brought in by clauses are associated with the block, unfolding is transitive:

  module _ where private
    opaque
      x : Nat
      x = 3
    opaque
      unfolding x
      y : Nat
      y = 4 + x
    opaque
      unfolding y
      _ : y ≡ 7
      _ = refl

• Opaque blocks which are lexically nested can also unfold the names of their parent blocks, even if the name is not in scope when the child block is defined:

  module _ where private
    opaque
      x : Nat
      x = 3
      opaque
        y : Nat
        y = 4
        _ : x ≡ 3
        _ = refl
      z : Nat
      z = 5
    opaque
      unfolding y
      _ : z ≡ 5
      _ = refl

  This is because the x and z are direct children of the same opaque block: the opaque block that defines y does not “split” its parent block.

Multiple unfolding clauses are supported, as well as unfolding more than one name per clause. The syntax for the latter is simply a space-separated list of names, which must refer to unambiguous functions:

module _ where private
  opaque
    x : Nat
    x = 3
  opaque
    y : Nat
    y = 4
  opaque
    z : Nat
    z = 5
  opaque
    unfolding x y
    unfolding z
    _ : x + y + z ≡ 12
    _ = refl

Finally, unfolding clauses do not introduce new layout context, so that the following is legal: note that y appears to the left of x, but is still attached to the same unfolding clause. This allows the user their preference for how to lay out their unfolding sets:

opaque
  unfolding x
    y
  unfolding z
  _ : x + y + z ≡ 12
  _ = refl

Having an unfolding clause appear after other definitions, or outside of opaque blocks, is a syntax error.

Note that unlike abstract blocks, which are treated on a per-module basis, opaque blocks will only unfold names according to the rules above:

module _ where private
  opaque
    x : Nat
    x = 3
  -- opaque
    -- _ : x ≡ 3
    -- _ = refl
    -- Fails with: x != 3 of type Nat

Unfolding in types

Note that unfolding clauses do not apply to the type signatures inside an opaque block. Much like for abstract blocks, this prevents leakage of implementation details, but it is also necessary to ensure that the types of names defined by the opaque block remain valid outside the opaque block. Consider:

opaque
  S : Set₁
  S = Set
  foo′ : S
  foo′ = Nat
opaque
  unfolding foo′
  -- bar′ : foo′
  -- bar′ = 123
  -- Error: S should be a sort, but it isn't

If the definition of bar′ were allowed, we would have bar′ : foo′ in the context. Outside of the relevant opaque blocks, foo′ is not a type, for foo′ : S, and S is not a sort. In cases like this, using an auxiliary definition whose type is a sort is required:

-- Lift foo′ to a definition:
ty′ : Set
ty′ = foo′
bar′ : ty′
bar′ = 123

Since ty′ : Set is manifestly a well-formed type, even outside of this opaque block, there is no problem in adding bar′ : ty′ to the context.

Bibliography

Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, and Lars Birkedal; “Controlling unfolding in type theory”.