[ elab ] Make %macro-function be callable without the ElabReflection extension

[buzden]

Description

Macro-functions are a great way of hiding some complex thing in a library without showing this to a user. A pretty example was shown as a motivating example in PR #2930.

But since currently call to a macro function, generally, is just a %runElab of an appropriate expression, each use of such function means to users that they need to turn on the language extension flag ElabReflection, despite they may not feel why.

I mean, imagine a library that does some hard stuff in a macro function (like enabling some syntax in PR mentioned above, or some DSL-y thing), and user just imports this library and uses its functions and gets "%language ElabReflection not enabled" all the time. I understand this requirement in explicit %runElab expressions and declarations -- here a user explicitly has chosen to run an elaboration script and we hope they know what they are doing, thus, this is their responsibility to say explicitly that they want this extension.

But %macro function seem to fill the different use case, when we want to hide this machinery from the user, i.e. to put all the responsibility on the effects to the library's author. But the current setting makes such library's user still to enable an extension, which, probably, they don't understand. The current setting also unables library authors to change existing function definition to a %macro without additional requirements from the users to enable the extension.

So, my suggestion is to enable usage of %macro-functions without the language extension, with no change in the behaviour of explicit %runElab calls. This is fully a backward-compatible change. This PR does this, among with couple of tiny textual improvements.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG.md (and potentially also
  CONTRIBUTORS.md).

[GunpowderGuy]

So to reiterate, this would allow modules without the elab extension turned on, to depend on libraries that use macro functions internally, if they dont expose that implementation detail to the end user?

[buzden]

So to reiterate, this would allow modules without the elab extension turned on, to depend on libraries that use macro functions internally, if they dont expose that implementation detail to the end user?

It depends on what you are calling the implementation detail. E.g., if there is a library that internally uses some macro function, but this is completely not exposed to the end user, it is okay now. E.g.:

module Lib1

import public Language.Reflection

export %macro
deriveNiceThing : Params -> Elab NiceThing
...

module Lib2

import Lib1

%language ElabReflection

export
aNiceThing : NiceThing
aNiceThing = deriveNiceThing niceThingParams

module SomeApp

import Lib2

usageOfNiceThing : Nat
usageOfNiceThing = someComputationOf aNiceThing

In this case a library Lib2 uses internally a macro function deriveNiceThing, but the end-used of the library Lib2 is not aware of it. And this type of code would compile by the current compiler.

But if we look at the Lib2 as the end-user of the library Lib1, then we'll see that Lib1 exposes a %macro-function, and Lib2 which uses this function as if it is a regular function of type Params -> NiceThing, needs to declare %language Elab.Reflection, which I propose to not to require to be declared.

[GunpowderGuy]

"Lib2 which uses this function as if it is a regular function of type Params -> NiceThing, needs to declare %language Elab.Reflection"
So macros only allow things that could theoretically be done by functions with normal ( type level ) metaprogramming?
However macros may be easier to use or the compiler may need to be expanded before said usage can be represented?

[buzden]

So macros only allow things that could theoretically be done by functions with normal ( type level ) metaprogramming?

No, %macro functions in Idris are just functions which when you call, are prepended with %runElab with respect to arguments. For example, if function fun is declared as %macro, the call fun a b c is elaborated to %runElab fun' a b c, or to (%runElab fun' a b) c, or to (%runElab fun' a) b c, or to (%runElab fun') a b c, whichever typechecks first. I used fun' in the example above to denote an access to fun as if there was no %macro in it, i.e., elaboration script of the function fun itself.

So, answering shortly, %macro functions have exactly the same abilities, as usual elaboration script, but the fact that there is an elaboration script underlying, is hidden. That makes then easier to use by the end user, especially when those macro functions are used as part of nice syntax or eDSL.

[GunpowderGuy]

While I support the idea of making macros more accessible by detaching them from the ElabReflection extension, I think it's crucial that they still require a specific extension to activate. Metaprogramming features have a history of being revised or updated, either for better design or to prevent unintended leakage of internal language details.

Take Rust as an example. It started with compiler plugins and pattern-matching macros. Later, more advanced procedural macros were introduced. These were initially intended to only replace compiler plugins but ended up largely replacing the first macro system as well due to its limitations and flaws. Eventually rust attempted to replace its pattern-matching macros with a new system, but this turned out to be a much bigger undertaking than anticipated, leaving the situation unresolved.

That situation would have been even more complicated if those features had been available by default, Idris 2 should keep current macros feature gated as well, potentially under a dedicated extension. This approach minimizes the risk of complications as the language evolves

[buzden]

This approach minimizes the risk of complications as the language evolves

I don't understand how this approach minimizes the risk. I, as a library author, either solve a problem with a macro, or I don't solve the problem. A user either has to use some extension (currently, ElabReflection), or doesn't (with this PR). Usage of an extension is tightly bound with a decision of a library author to use macro, which is usually dictated by a matter of a problem solved by this macro. How this situation eases from complications as the language evolves?

[gallais]

Probably worth talking about it during one of the weekly meetings to get @edwinb's opinion.

[GunpowderGuy]

Looks like next week's meeting was cancelled. We should coordinate on discord whether we can all discuss this the week after that