Der Schutz (Aug 23 2024 at 17:20): Der Schutz (Aug 23 2024 at 17:20):On the latest podcast, I heard Richard say that macros can hurt editor functionality. The example given was for Rust string interpolation not having type information or renaming things in interpolations. Is this just a result of the Rust implementation? Lean 4 supports arbitrary expressions inside interpolated strings, each part of the expression has its type displayed in the editor, and also supports renames. Lean has an extremely extensive macro system though and I'm not familiar with how Rust macros work under the hood.
Richard Feldman (Aug 23 2024 at 17:30):Der Schutz said:
Lean 4 supports arbitrary expressions inside interpolated strings, each part of the expression has its type displayed in the editor, and also supports renames. Lean has an extremely extensive macro system though and I'm not familiar with how Rust macros work under the hood.
it looks like string interpolation is a first-class language feature in Lean 4: https://lean-lang.org/lean4/doc/stringinterp.html
Richard Feldman (Aug 23 2024 at 17:31):I don't know Lean 4, but based on the outline in that section, it looks like it's a separate "syntax extension" from macros, which have their own entry:
Screenshot-2024-08-23-at-1.31.23PM.png
Der Schutz (Aug 23 2024 at 18:56):Richard Feldman said:
Der Schutz said:
Lean 4 supports arbitrary expressions inside interpolated strings, each part of the expression has its type displayed in the editor, and also supports renames. Lean has an extremely extensive macro system though and I'm not familiar with how Rust macros work under the hood.
it looks like string interpolation is a first-class language feature in Lean 4: https://lean-lang.org/lean4/doc/stringinterp.html
The macro is implemented in Lean itself (the implementation is here: https://github.com/leanprover/lean4/blob/edecf3d4baa30ef9a74d6af78a754d88c30b4386/src/Init/Meta.lean#L1264 ) and https://github.com/leanprover/lean4/blob/edecf3d4baa30ef9a74d6af78a754d88c30b4386/src/Init/Data/ToString/Macro.lean#L12 . So there isn't anything special other than that it's already implemented for you. Also Lean has a configuration file DSL where its still a .lean file but the syntax is custom and you get renaming/hover type info/autocompletion. I'm not too sure how that DSL works implementation wise though. But all of this stuff can be implemented in user-land.
Here is an example of the config file DSL, without opening Lake DSL, this would error out because the syntax isn't "valid" Lean syntax. But you still get autocomplete, type info, and other stuff even though the syntax is "made-up". This is up to the macro author to implement however: https://github.com/leanprover/lean4/blob/390a9a63a24ca28306a60faa0381d4292d23af95/src/lake/examples/targets/lakefile.lean#L1
Der Schutz (Aug 23 2024 at 19:12):If the language provides the right API's to authors, then you can have a good editor experience. That being said though, macros are super powerful. I don't think they should be shoved into the language just because, even if having a good editor experience is not one of the main reasons.
Richard Feldman (Aug 23 2024 at 20:05):cool, TIL! do you know if the editor tooling works just as well with macros defined in userspace?
Richard Feldman (Aug 23 2024 at 20:06):(in other words, is the tooling specific to interpolation because it knows how it's implemented, or just as effective with any arbitrary macro)
Der Schutz (Aug 23 2024 at 23:42):Richard Feldman said:
cool, TIL! do you know if the editor tooling works just as well with macros defined in userspace?
I'm definitely not the person to ask because I mainly use the macros rather than make them myself. But for interpolation, a user could implement the exact same thing with the same level of tooling. However the macro author has to write the tooling for the macro itself to some extent. Some of it is automatically handled based off the implementation, and I believe it displays the doc comment for the specific Syntax node on hover for a given Parser. You can also add pretty printing so that it doesn't just print the elaborated form only. toString is carrying here, but this works fine:
import Lean
open Lean Elab Term Meta
/--
A simple string interpolation macro.
Usage: `str_interp!{expression}`
The expression is evaluated and converted to a string.
-/
syntax (name := strInterp) "str_interp!{" term "}" : term
@[macro strInterp]
def expandStrInterp : Macro
| `(str_interp!{$e}) => do
`(toString $e)
| _ => Macro.throwUnsupported
def example1 := str_interp!{3 + 2 + factorial 2}
Hovering over str_interpdisplays the type String and the doc comment above the strInterp syntax. Can hover over any sub-expressions (including if they're nested) and see its type. I can rename factorial and it will rename it within the string interpolation. I just made a vec! macro (turns vec![] into an List type) also to see if it preserves sub-expression types automatically on hover and it does. This is my first time implementing a macro in their system though as trying to read some of the macro/parser implementations is like voodoo for me.
Der Schutz (Aug 24 2024 at 00:09):I was trying to see if I have a custom expression type if it would let me rename automatically and it won't, which makes sense. Maybe there is some LSP API you could hook into to tell it how to work with that, but no clue.
Greg (Oct 14 2024 at 21:53):Hi there Richard,
Just wanted to say I'm really enjoying this podcast! It's a great idea to garner interest for roc and I'm looking forward to giving this language a go.
Thank you and all the best!
Richard Feldman (Oct 14 2024 at 22:46):thanks so much, and glad you're enjoying it! :smiley:
Last updated: Jul 06 2025 at 12:14 UTC