opaque: use-site control of unfolding

[plt-amy]

Idea

Over AIMXXXI, @jespercockx and I implemented unfolding control for a variation on abstract, now called opaque (this is our version of Controlling unfolding in type theory by Gratzer et. al., but in the interest of backwards-compatibility, the default is still "transparent"). Currently, the only way to ‘see through’ an abstract block is to be in another abstract block, in the same module. With opaque blocks, a user can instead write:

module A where opaque
  x : Set
  x = Nat

module B where
  opaque unfolding (A.x) where
    y : A.x
    y = 123

where the type-checking of y depends on knowing the definitional equality A.x = Nat, i.e., unfolding A.x. Any definition which unfolds B.y must also unfold A.x, and Agda will compute this transitive closure by itself, so that you can write:

module C where opaque unfolding (B.y) where
  ty : Set
  ty = B.y ≡ 123

  _ : ty
  _ = refl

If it were possible to write this without unfolding A.x, then we'd have the definitional equality B.y : A.x = 123, where 123 has type Nat, but no equality A.x = Nat. Note that it's impossible to write the definition of _ without first defining C.ty. Quoting the paper:

The effect of a θ unfolds κ1; . . . ; κn declaration is to make κ1; . . . κn unfold within the definition of θ, but still not within its type; it will happen, however, that a type might not be expressible without some unfolding.

That's precisely the situation we have here, and introducing an auxiliary binding for the type is precisely what they do. The implementation at present does not yet contain unfolding k1 in E expressions (or let unfolding, or what-have-you). Additionally, abstract unfolding blocks are "lexically closed", so that the following is valid (within the file we've been building):

module E where
  opaque unfolding (D.z) where
    opaque unfolding (B.y) where
      ty : Set
      ty = B.y + D.z ≡ 579

      _ : ty
      _ = refl

Implementation

Opacity and abstractness are two separate "directions" of a new type, IsReducible. The elaborator stores both an AbstractMode, as before, and a new OpaqueMode, which stores the OpaqueId of the block we're currently in (if any).

When a definition gets looked up, the environment "interacts" with the IsReducible of the definition, and potentially removes either abstract (with the old rules) or opaque (depending on surrounding unfolding declarations). The PostScopeState maintains a mapping from OpaqueId to HashSet QNames, storing the (transitively-closed) sets of names which may be reduced. In addition to the TypeChecking.* changes, opaque unfolding also touches the following components:

• Nicifier: This is the last place where we see opaque blocks as coherent pieces of syntax, so OpaqueIds are generated here. We also add an internal NiceUnfolding declaration associating each OpaqueId to its user-written list of QNames.

• Scope checker: Here we compute the mapping from OpaqueIds to HashSets of QNames, initially by traversing the definitions in the block, and after all of those, scope-checking the list in the NiceUnfolding. That last step is where the transitive closure happens: each name in the list must have its own OpaqueId (otherwise a warning is raised), which allows us to pull in the dependencies of each mentioned name. This also allows us to generate very precise warnings about redundant names in unfolding clauses.

[MatthewDaggitt]

This looks amazing, will definitely help improve the interface of the standard library! Really looking forward to this landing.

in the interest of backwards-compatibility our bindings are still "unfold by default

Will there be a new keyword to make an abstract block "not unfold by default" then?

[jespercockx]

Will there be a new keyword to make an abstract block "not unfold by default" then?

I think what @amy meant is that standard (non-abstract) definitions are still unfolded by default as in current Agda, in contrast to the language that is presented in the paper where everything is abstract-unless-explicitly-unfolded.

One comment I got when explaining this new feature to a colleague is that it has a potential downside for library developers in that they can no longer be sure that changing an abstract definition (without changing its signature) does not break any user code (whew, that was too many negations). A way to work around is, is to make the definition not just abstract but also private (so it becomes impossible to mention its name in an unfolding statement), and have a public wrapper around it that is exported (which might be abstract or not). But this is quite a bit of extra overhead, so we might want to consider if we want to add a dedicated way to make a definition private while keeping its signature public.

[MatthewDaggitt]

I think what @amy meant is that standard (non-abstract) definitions are still unfolded by default as in current Agda, in contrast to the language that is presented in the paper where everything is abstract-unless-explicitly-unfolded.

Thanks, that makes sense!

But this is quite a bit of extra overhead, so we might want to consider if we want to add a dedicated way to make a definition private while keeping its signature public.

As does this 👍

[nad]

There are two use cases for abstract:

• Hiding implementation details.
• Controlling unfolding.

I don't think we should allow any kind of unfolding for abstract, but we could add a new keyword for the second use case.

What about something involving block? The word block on its own is rather ambiguous. Some of Agda's keywords are nouns (module, record, postulate), some are adjectives (private, abstract, public), and some are verbs (open, using). Should this be an adjective (blocked)?

blocked
  A : Set
  A = Nat

...

blocked unfolding (A; ...) where
  ...

Another option is to drop unfolding and to make the list required:

blocked () where
  A : Set
  A = Nat

...

blocked (A; ...) where
  ...

However, that code is less self-explanatory.

[plt-amy]

Ah, I rebased this by hand, but it didn't even occur to squash the fixups away while I was doing it.

Re. the thread, I don't have a strong preference either way on whether this should be added to abstract blocks, or whether we should add a new keyword, so I'll leave choosing the colour of the bike shed to others (e.g. @jespercockx) 😛

Edit: actually, I'll say that

library developers in that they can no longer be sure that changing an abstract definition (without changing its signature) does not break any user code

has a positive converse: If a library exports an abstract definition together with abstract proofs of its properties, but a necessary property is missing, a user can, while waiting for an upstream fix, unfold the definition and prove it themselves, without having to go in and patch the library by hand. Note that if you use e.g. Nix to manage your Agda libraries, then it's impossible (rather than just inconvenient) to modify libraries by hand

[jespercockx]

library developers in that they can no longer be sure that changing an abstract definition (without changing its signature) does not break any user code

This is why I mentioned the trick with having a private definition that cannot be unfolded. I think it makes sense to allow abstract definitions to be unfolded by default (for the reason mentioned by @plt-amy above), but provide a separate mechanism for when you really don't want people to depend on the body.

[jonsterling]

I think it is a good idea to have an easy way to make a definition really private while keeping its signature public, as @jespercockx suggests. We did not really treat this explicitly in our paper, but I think it is necessary for a serious implementation. I would personally favor having an easy / not-as-encoded way to do this, though it would be fine if it had the same semantics as Jesper mentions.

Regarding the naming of abstract, I agree that it could be potentially confusing to change the meaning of abstract since there is already code that uses it under the expectation of its current semantics. But I'm personally not sure of a better name, and I would hope that integrating controlled unfolding into Agda would result in a more nuanced and powerful version of the abstract feature, rather than yet another layer on top of it.

[nad]

This is why I mentioned the trick with having a private definition that cannot be unfolded. I think it makes sense to allow abstract definitions to be unfolded by default (for the reason mentioned by @plt-amy above), but provide a separate mechanism for when you really don't want people to depend on the body.

The abstract feature was introduced as a mechanism for hiding implementation details, even though it has recently mostly been (ab)used to control unfolding. I have used abstract for hiding implementation details in one paper, and with the new semantics the code in my paper would not make sense.

Note also that the name abstract is presumably related to the concept of an abstract data type: if you implement a data structure using abstract, then you can later switch to a different data structure without breaking users' code.

For these reasons I am opposed to changing the meaning of abstract in the suggested way.

[jonsterling]

What about opaque?

[jespercockx]

What about opaque?

That's not a bad suggestion in case we decide not to go with abstract.

[jespercockx]

Another option would be to keep the semantics of current abstract blocks as is, but use the new syntax abstract unfolding () where for things that can be unfolded later.

[jonsterling]

@jespercockx I think that option might be a little confusing, since it conflates two things that are conceptually different (being able to be unfolded, and needing to unfold things).

[jespercockx]

Well, but in our current implementation these things are conflated: if you want to be able to unfold things, then you yourself also need to be unfolded explicitly. So having the same syntax for both makes some degree of sense.

[jonsterling]

@jespercockx I think it is not good for those things to be conflated... This should be revisited. Zooming out from implementation details, can you explain why it makes sense for these things to be related?

[plt-amy]

Note, mostly to self: I'll rebase this on Monday, or when we settle the bike-shedding ­— whatever comes first 😉

[jespercockx]

@jespercockx I think it is not good for those things to be conflated... This should be revisited. Zooming out from implementation details, can you explain why it makes sense for these things to be related?

If you had a definition of g that requires the definition of f to be unfolded but g itself is always unfolded, then g might not be well-formed in places where f is not unfolded. The reason for this is that we did not yet implement the abbreviation keyword from your paper, and hence we cannot express that "g is unfolded wherever f is unfolded".

However, this made me consider that even if abbreviation does not necessarily need to be part of this PR, we should still consider it in the syntax to make sure it can be added easily later. The most obvious way to support it would be to allow unfolding to appear on its own without abstract:

abstract
  f : ...
  f = ...

unfolding (f) where
  g : ...
  g = ...

unfolding (f) where
  h : ... g ...
  h = ...

This would unfold the definition of g in the type signature in h, since g would be always unfolded together with f.

[jespercockx]

Regarding the question of whether it is fine to steal the abstract keyword for this feature or not, my preference is still to reuse abstract, but if this is unacceptable then my second choice would be to introduce a new keyword opaque (as suggested by @jonsterling ).

[jespercockx]

Regarding the non-bikeshedding part of this PR, one issue I would still like to see addressed is the fact that currently, unfolding one abstract definition in a module automatically unfolds all other definitions in the same module, which was not really granular enough in the experiments I did so far. However, it is unavoidable with the current semantics of abstract because abstract definitions in the same module can "see through" each other. Arguably, this would be easier to fix if we introduce a new keyword opaque and simply not allow the same for opaque definitions.

[JacquesCarette]

Re unfolding one abstract definition: I know this would be a breaking change, but wouldn't it make more sense for different abstract blocks in the same module to be separate? My mental model was that of "abstract blocks", not of module being the only grouping mechanism.

I guess the work-around would be to define anonymous modules to contain each of the "abstract blocks" -- would that do it?

[jespercockx]

Re unfolding one abstract definition: I know this would be a breaking change, but wouldn't it make more sense for different abstract blocks in the same module to be separate? My mental model was that of "abstract blocks", not of module being the only grouping mechanism.

I agree, but I think it's better to not conflate this with the discussion about this new feature (which should preserve backwards compatibility whenever possible).

I guess the work-around would be to define anonymous modules to contain each of the "abstract blocks" -- would that do it?

Yes, that's what I'm doing at the moment in my experiments.

[JacquesCarette]

Since the work-around works, I agree that it's better not to conflate. [Need to start planning for Agda 3.0 ...]

[jespercockx]

@plt-amy Do you want to look into making these two changes (introducing the opaque keyword and making opaque definitions not see through opaque definitions in the same module)? Otherwise I could take a look myself as well.

[jespercockx]

What I imagined was to keep it largely orthogonal to abstract/non-abstract, so with four possible states: transparent (the default), abstract, opaque, and abstract+opaque. Abstract+opaque cannot just be the same as abstract, as an abstract definition cannot look through an abstract+opaque definition in the same module. Hence the semigroup instance would be:

• transparent is neutral
• abstract combined with opaque is abstract+opaque
• abstract+opaque is the zero
• combining abstraction barriers is commutative and idempotent

Your example would not be accepted, since opaque unfolding can only look through an opaque barrier, not an abstract one. Abstract definitions can also not look through opaque definitions (whether they are in the same module or not).

(This is just a proposal for the design, feel free to shout if this doesn't make sense).

[plt-amy]

I think that's a sensible approach. It'll take a couple more words to document when something can be unfolded, but it's more consistent than (e.g.) abstract and opaque overriding each other. Something like:

Unfolding of a function definition may be blocked either by an abstract barrier, or by an opaque barrier. The following rules apply:

• If a function f is defined in an abstract block in the same, or a child module of, as a function g, then abstract blocks surrounding g are ignored.
• If a function f is defined in an opaque unfolding (g) block, then opaque blocks surrounding g and any of its transitive dependencies are ignored.

together with examples of opaque non-abstract not reducing outside of opaque unfolding, an error message (possibly?) for an opaque unfolding declaration mentioning an abstract opaque definition in a disjoint module, etc.

Unfortunately, I won't be able to get my ADHD meds refilled until the 14th, since my psychiatrist's on vacation, so I find it unlikely that I'll be able to focus long enough to implement this until then. If waiting until then is okay, you can leave the implementation to me; but if we don't want to let this PR get in the way of other stuff (or don't want to generate another nasty rebase), @jespercockx I think it'd be better if you could take over (thanks)

[jespercockx]

I have enough other tasks so if you could do it after the 14th then I can definitely wait until then ;)

[xekoukou]

Maybe with this, #3414 #3836 are also easier to implement. In other words, an interactive normaiization of goals , errors, context.

[plt-amy]

I finally got around to moving the documentation for opaque to its proper place, adding it to the changelog, and updating the PR description. I'm happy with the current state of the PR¹, and I think we should merge it before it gets completely out of hand.

¹ I'm writing this comment before CI on the last batch of commits finishes, so there might still be fixups I'll need to squash before merging.

[andreasabel]

Wow, great, this has come a long way!
I haven't been following the development...

Agda is a layout-sensitive language, so the new syntax should take advantage of this.

[andreasabel]

The parentheses are superfluent, it seems, or is there an example where they are needed to parse?

Also, unfolding should be a layout keyword so that you can drop the semicolons if you like:

opaque unfolding 
    quux ; bar 
    foo 
    baz ; baz′ 
    asdf ; ghij ; some-other 
  where
...

[andreasabel]

I can give this a shot since I have worked with layout before.

[Trebor-Huang]

Are these parentheses supposed to resemble import using statements?

[plt-amy]

That was the idea, yes

[andreasabel]

I think the first stab reused the parser for import directives (and thus similar syntax), but in essence, this is a plain identifier list, so no sophisticated parser needed.
unfolding ... where is already a pair of brackets, this is why we do not need to nest another pair inside this.

NB. I am not fond of the using syntax either, but at least there the parentheses have a function (since there is no closing bracket matching using).

[jespercockx]

I'm not sure if I like definitions in the same opaque block (i.e. not one in opaque and one in a child unfolding) not to be able to see each-other..

Ah yes I see the problem. The current problem I had with the prototype abstract unfolding from AIM is that all abstract definitions in the same module can see through each other, which is much too coarse. But perhaps having definitions from the same opaque block see through each other would not be so bad, and would make the implementation more straightforward as you said.

In that case, quux should unfold all of foo, bar, and baz since they are in the same opaque block.

[jespercockx]

Btw, would be great if we could write unfolding ... in .... However, I don't know if this can be integrated into our layout mechanism, because in has a different role there. Have to have a look.

We discussed a local unfolding construct during the AIM, but the consensus was that we should first implement a minimum viable product with just top-level unfoldings, and then look into extending it later.

[plt-amy]

Translating Andreas' example to today's syntax and semantics, we have:

• foo and quux can unfold each other,
• bar and baz can unfold each other,
• Neither pair of definitions automatically unfolds the other pair.

Nested opaque blocks are treated independently of any enclosing opaque blocks.

Definitions in the same opaque block (in a literal sense) automatically unfold each other, in addition to the transitive closure of the names mentioned in the unfolding clause, if any.

We decided on this because abstract does the same, and it's also very smoothly supported by the current implementation.

My question is, having split "opaque block" from "unfolding block" syntactically, should they be semantically split, too? And if so, how? Should unfolding blocks also unfold everything that belongs to the same enclosing opaque block? What about nested opaque blocks: should they also unfold lexically-enclosing opaque blocks?

[nad]

We decided on this because abstract does the same, and it's also very smoothly supported by the current implementation.

Different top-level abstract blocks in the same module are treated as one block. I hope that will not be the case for opaque blocks.

[jespercockx]

My question is, having split "opaque block" from "unfolding block" syntactically, should they be semantically split, too? And if so, how? Should unfolding blocks also unfold everything that belongs to the same enclosing opaque block? What about nested opaque blocks: should they also unfold lexically-enclosing opaque blocks?

(Coming back to this issue finally.) I think it makes sense to also make the distinction semantically, even if it is just to provide options for later extensions to the feature. I.e. I think we can currently allow a unfolding block only inside an opaque block.

Regarding the question of nesting, let us try to stick as close as we can to the semantics in the paper. Basically, each opaque block would introduce a new unique identifier (called "proposition symbols" in the paper), and a definition should only unfold if all the identifiers in its surrounding opaque blocks are in the current unfolding set (i.e. their proposition symbols are in the context). A unfolding f where block then should introduce all the identifiers of f to the context, i.e. it should unfold all the definitions in the same opaque block as f as well as the ones in its surrounding opaque blocks, but crucially not those in the 'sister' opaque blocks.

Here is an example:

opaque
  f = 1
  opaque
    g = 2
  opaque
    h = 3

opaque unfolding g where
  k = (f + g) + h

  shouldWork : k ≡ 3 + h
  shouldWork = refl

  shouldFail : k ≡ 6
  shouldFail = {! refl !}