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
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.
Functions (and primitive functions) can be marked
opaque. Outside of
opaqueblocks, these behave like postulates.
Opaque blocks, even in unrelated modules, can have
unfoldingclauses, 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.
ℤ is opaque rather than abstract, a different
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?¶
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
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
xwas asked for,
yis 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
zare direct children of the same
opaqueblock that defines
ydoes 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
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
opaque unfolding x y unfolding z _ : x + y + z ≡ 12 _ = refl
unfolding clause appear after other definitions, or
opaque blocks, is a syntax error.
Note that unlike
abstract blocks, which are treated on a per-module
opaque blocks will only unfold names according to the rules
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
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
foo′ in the context. Outside of the relevant opaque blocks,
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
ty′ : Set is manifestly a well-formed type, even outside of
this opaque block, there is no problem in adding
bar′ : ty′ to the
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, and Lars Birkedal; “Controlling unfolding in type theory”.