RFC: Export scoped commands

Stream: lean4

[Soundwave]

Apologies if this has been hashed already, seems the issues it addresses have come up over the years with unclear resolution:

Proposal: Command causing another namespace to be considered in-scope for the purpose of "scoped" if the namespace in which it resides is in scope.

Example (syntax can be reworked, it's admittedly not super intuitive):

namespace Foo
  def add (x : Nat) (y : Nat) : Nat := by sorry

  scoped infixr:50 " ⊕ " => add
end Foo

namespace Bar
  export scoped Foo
end Bar

namespace Baz
  open Bar

  #check 2 ⊕ 2 -- Okay!
end Baz

Motivation: Currently the prelude and core need to flood namespaces, possibly including the root namespace, with notation for the core language without resorting to littering open everywhere. With current mechanisms, this is only possible by defining the notation in the root namespace, but this feature would permit the prelude to include an export to the root namespace, and modules within the prelude and core to use more conservative floods, such as only throughout Lean and Init. This would resolve long-standing issues with notation in self-contained developments and DSLs.

Impacts: No regressions. Minimizes complexity of increasing prelude flexibility. Presumably improves DX for library interoperability in other contexts, although I’m unsure how relevant that is to the current Lean ecosystem.

[Kyle Miller]

Could you say a bit more about the motivation? What pieces of the core language would not be exported to the root namespace? If that's not the intent, how would export scoped help?

There's a related feature, a variation of export that only makes names available when you've opened the namespace (or are in the namespace) that @Mac Malone and I have talked about. While export scoped does make some sense, since it's as-if the activities that occur with open are exported into another namespace (although that's not how it would be implemented), I wonder if there's another syntax that would work for "sticky" open. All I can think of is scoped open Foo and scoped open scoped Foo right now, but these are bound to be confusing.

There's also a related feature request for being able to locally disable syntaxes. Potentially syntaxes can be grouped and disabled together.

[Soundwave]

The prelude would export all of the core language to the root namespace, but crucially, via a module that is only included as part of the implicit import (Is it just Init? In this case Init would be the sole importer of a module that exports notation into Init. Similarly with Lean). That way you have the option of importing core modules, e.g. metaprogramming modules, without necessarily importing scoped commands. As it stands, a header like

prelude
import Init.Prelude
-- Lean.Elab.Tactic covers most of the bases but it....

has a major limitation in flexibility because Init.Notation is downstream of everything.

I hit on the scoped open syntax as well and chose export scoped to disambiguate from open scoped, but yes, it does feel like more of an open than an export. It also doesn't necessarily need to fit either of these schemes, I'm not fussed about it.

I'm not opposed to syntax hiding but it does bring two issues to mind: lesser, a lack of symmetry with identifiers, which can only be shadowed or refactored out of scope; and greater, syntaxes are ~anonymous and so it'd be quite a namespace shakeup to normalize referring to them in order to disable them.

[Kyle Miller]

I see — I didn't expect this to be about supporting user preludes. As far as I understand it, prelude is only meant for the implementation of Lean itself, and the system assumes that the supplied prelude is loaded. My feeling is that it's unlikely that we'll see any development in this direction, certainly not any time soon.

Some sort of scoped open/export is plausible in the near future, but not specifically for the use case you're envisioning.

This would resolve long-standing issues with notation in self-contained developments and DSLs.

Is this something that has been affecting you for a long time? I saw your question today about doing logic from scratch, with the Sheffer stroke. Is this minimized from some larger ongoing project?

From what I've seen, the solution to creating a DSL is to create a custom syntax category rather than try to reuse term. It's still work, but at least commands aren't broken because you don't have the full prelude loaded.

[Soundwave]

Kyle Miller said:

I see — I didn't expect this to be about supporting user preludes.

It's not, in the sense that I wouldn't have brought it up if I didn't think it was a sensible concern for other libraries. I am interested in writing preludes, but I understand that this isn't exactly sanctioned.

Is this something that has been affecting you for a long time? I saw your question today about doing logic from scratch, with the Sheffer stroke. Is this minimized from some larger ongoing project?

Yes re:minimization, although broadly this isn't a major pain point. I was more speaking to variations on "Can you override core notation? Well yes, but no." that have been asked over the years.

Yeah, there are solutions for DSLs, I just figure a step towards the Racket-esque with a DX improvement is a win-win, if low priority. Incidentally, in my tinkering I've found Init.Prelude + the coercions for TSyntax to be surprisingly functional for an unsupported mode. Really the main issue is not being able to lean on the core without yanking the rest of the prelude with it.

[Kyle Miller]

Having Racket-style #langs is an idea we kick around, but the current focus is improving the Lean language itself and supporting embedded DSLs, for example David Thrane Christiansen has made a nice DSL (Verso) for writing documents such as the new Lean language reference.

Making use of namespace activation is an interesting idea for trying to support #langs, but my guess is we'll see real support for turning off existing notations, or maybe also third-party mini-Lean frontends that have a way to opt-in to language features in a composable way, for teaching or other research.

By the way, there's an obstacle here with relying namespace activation, which makes using it as a step toward #lang not as good as you might want. There are plenty of notations that are "builtin" that use the @[builtin_term_parser] mechanism (see src/Lean/Parser/Term.lean), and these are not syntax that can be scoped.

DX improvement

I'm still not clear on the whole story here how it improves the developer experience for someone using the full Lean language — export scoped doesn't help the "can you override core notation" problem, right? I do see it being useful for creating namespaces with a curated set of instances and notations from other namespaces, to be clear.

Mathlib runs into issues with the core prefix ! notation for boolean negation, since it has a postfix ! for factorial that leads to ambiguities. It would be nice to have a way to turn off "programming" notations. The preference though is for these basic notations to be immediately available, so I imagine, if it becomes possible, it will be opt-out instead of opt-in.

A design that comes to mind is that each syntax could have option name(s) associated to it, which would let set_option (or a syntax-specific command) control classes of syntax. Assuming these configurations could be scoped, that would enable you to have namespaces in which certain syntaxes are disabled, but even without that feature you can create command macros that set the desired configuration. That's more powerful than export scoped, which can only add syntaxes. Though, it's not so nice that different namespaces might have conflicting configurations; scoped is nice in that there are no conflicts, only unions.

A wrinkle though is that the pretty printer needs to be similarly controlled (it's not nice seeing things pretty printed in a way you can't write yourself). These processes are not coupled, and it would take a little coordination, but it should be doable. At least all notations defined with notation could be handled at once.

[Soundwave]

Kyle Miller said:

By the way, there's an obstacle here with relying namespace activation, which makes using it as a step toward #lang not as good as you might want. There are plenty of notations that are "builtin" that use the @[builtin_term_parser] mechanism (see src/Lean/Parser/Term.lean), and these are not syntax that can be scoped.

Known. Full #langs seemed like a ways off (and honestly, even as someone who wants to pick apart the core, I'm not itching for them); this seemed like a more reasonable step

I'm still not clear on the whole story here how it improves the developer experience for someone
using the full Lean language — export scoped doesn't help the "can you override core notation" problem, right? I do see it being useful for creating namespaces with a curated set of instances and notations from other namespaces, to be clear.

This is a fair point. Without additional mechanisms it doesn't immediately, but without something to this effect the prelude has no mechanism by which to permit this. If we wanted to sanction specifically this use case of subverting the prelude, it'd then be as simple as a header command to suppress the one import.

A design that comes to mind is that each syntax could have option name(s) associated to it, which would let set_option (or a syntax-specific command) control classes of syntax. Assuming these configurations could be scoped, that would enable you to have namespaces in which certain syntaxes are disabled, but even without that feature you can create command macros that set the desired configuration. That's more powerful than export scoped, which can only add syntaxes. Though, it's not so nice that different namespaces might have conflicting configurations; scoped is nice in that there are no conflicts, only unions.

This seems fine to me from a UX standpoint.

The reason why I'm inclined towards making this work with an additive mechanism with a default and opt-in baseline reductions is that my experience with reflection-heavy Java has been that normalizing subtractions is a Pandora's box of potential nightmare maintainability scenarios.

Coming at it from an angle of "Okay, in the idealistic model where #langs etc. are built out, does this make sense?" being able to export scopes seems somewhat natural, and moves closer to a model where import and #lang are one and the same, whereas syntax options is... fine, though see above, and they would seem to be less pressing in this scenario.

[Soundwave]

Re: The Mathlib use case, I will admit that syntax groups uniquely do address this, but my intuition there is to make syntaxes identifiable and shadowable, not add syntax options.

Which come to think of it, does in and of itself cover most use cases for interop with the full language.