Field Exports

Stream: lean4

[Mac]

A common pattern in Lean is to export the fields of a class like so:

class Pure (f : Type u → Type v) where
  pure {α : Type u} : α → f α

export Pure (pure)

I would like to request the following shorthand for this be made available:

class Pure (f : Type u → Type v) where
  export pure {α : Type u} : α → f α

That is, prepending a field declaration with export results in it being exported into the surrounding namespace.

Is this reasonable? Does anyone else want this?

[Kevin Buzzard]

Can you make this happen yourself somehow with a macro or something? My understanding from talking to Leo was that this sort of request can be implemented by users and hence he doesn't have to bother.

[Mac]

Kevin Buzzard said:

Can you make this happen yourself somehow with a macro or something?

I don't think so? Doing this user-side would require overwriting the class syntax, which would then mean you could not expand the macro to the old class syntax (as it has been overwritten) thus you would have to rewrite the class command elaborator from the ground up to add this little tweak. At least as far as I am aware.

[Daniel Selsam]

@Mac I believe you are right, that currently you would need to re-simulate the upwards-closure as in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lemma.20.3A.3D.20theorem.3F/near/237003783

[Daniel Selsam]

Once you did, you could define an expandExports? helper (similar to expandDeclNamespace? called at https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Declaration.lean#L142-L146) and then fallback on the regular elaboration process. But besides being clunky, there would be a performance cost on errors, since it would effectively try to parse ill-formed structure commands twice.

[Mac]

In addition to there being problems with this being custom syntax, I also feel that this is a feature that deserves to be part of standard Lean. It can already get a lot of mileage in the Lean sources (hence why I used the definition of Pure as an example). It also fits with the style of a general programming language as in many ways it is like a visibility modifier (or the export of JavaScript/TypeScript) that can appear on fields in other languages.

[Mac]

However, the idea here is to gather the Lean community's thoughts on the issue and see whether this really is something worth pursuing (i.e., would this be useful to users and are the developers willing to implement such a feature). In essence, this both a feature request and a request for comment (RFC).

[Daniel Selsam]

My 2 cents: I personally do not think it is worth adding.

[Brandon Brown]

Yeah this feature seems somewhat convenient but given how many other higher-priority things there are to do it might be best to consider it for a 1.x release (x > 0). I'd rather get a stable Lean4 a bit sooner and have some missing convenience features that can be added later

[Sebastian Ullrich]

Mac said:

Doing this user-side would require overwriting the class syntax, which would then mean you could not expand the macro to the old class syntax (as it has been overwritten)

Fwiw, this can be done using

`(Lean.Parser.Command.structure|class ...)

You'll need to import Lean though.

[Sebastian Ullrich]

Or you declare the part of the macro with the quotation before the new syntax

[Mario Carneiro]

Mac said:

However, the idea here is to gather the Lean community's thoughts on the issue and see whether this really is something worth pursuing (i.e., would this be useful to users and are the developers willing to implement such a feature). In essence, this both a feature request and a request for comment (RFC).

Suggestion: let's mark the threads of such features that are following the lean 4 community contribution guidelines explicitly as [Pre-RFC] or [RFC] in the title to give them some more exposure and indicate the intended goal of raising the issue here.