Lean metaprogramming vs Swift macros

Stream: new members

[misterdrgn]

HI all. I have another question comparing Lean to Swift, since Swift is the language I'm currently using in my research lab. Swift has a powerful macro system that I use to auto-generate code supporting functional programming idioms. However, Swift's macro system has several drawbacks, and I'm curious how Lean compares on each of these points.

1) Swift macros have to be built in their own package.
This is annoying when you're first getting started, but not much of an issue in the long run. I'm pretty confident Lean wins on this point.

2) Swift macros don't allow you to make new syntax.
Most Swift macros come in the form of a label you write to the side of some existing code, so you can't make new syntax constructs with it, the way you can in Lisp for example. I'm not trying to write a DSL or anything, so that hasn't really been an issue for me.

Now we come to the two points that for me are probably the biggest drawbacks of Swift overall...

3) Swift macros don't have access to type information.
The macros operate on the AST, prior to type inference. Even when types are provided by the programmer so no inference is necessary, there is afaik no direct access to information about a type. For example, the type might be MyType, and there'd be no way to know that that is an alias for an array of strings or something. All you'd have access to is the name "MyType". Admittedly, I haven't used macros in another strongly typed language, so I don't know how a language like Lean compares here.

4) Swift macro expansions are ignored by the auto-generated documentation.
This is maybe the biggest thing, as I use macros to generate code, including public functions. I work with a team, and unless I document things careful and explain what each macro does, the team will have no idea what code a macro is generating. It's frustrating because otherwise, Xcode generates very nice documentation for Swift code. I'm really curious how Lean's doc-gen4 compares here.

Thanks.

[Aaron Liu]

misterdrgn said:

1) Swift macros have to be built in their own package.
This is annoying when you're first getting started, but not much of an issue in the long run. I'm pretty confident Lean wins on this point.

Syntax parsers, macros, and elaborators all work in the same file, as soon as they're defined. However, options and environment extensions don't work in the same file, and must be defined in an imported file.

[Aaron Liu]

misterdrgn said:

2) Swift macros don't allow you to make new syntax.
Most Swift macros come in the form of a label you write to the side of some existing code, so you can't make new syntax constructs with it, the way you can in Lisp for example. I'm not trying to write a DSL or anything, so that hasn't really been an issue for me.

In Lean, you can make new syntax categories and write new syntax.

[Aaron Liu]

misterdrgn said:

3) Swift macros don't have access to type information.
The macros operate on the AST, prior to type inference. Even when types are provided by the programmer so no inference is necessary, there is afaik no direct access to information about a type. For example, the type might be MyType, and there'd be no way to know that that is an alias for an array of strings or something. All you'd have access to is the name "MyType". Admittedly, I haven't used macros in another strongly typed language, so I don't know how a language like Lean compares here.

Lean macros basically only have access to the syntax, macro scopes, and basic error handling. For more complicated things, like needing to know type information, you would write an elaborator, which has access to the environment, and can do type inference, typeclass synthesis, and look up definitions.

[Aaron Liu]

misterdrgn said:

4) Swift macro expansions are ignored by the auto-generated documentation.
This is maybe the biggest thing, as I use macros to generate code, including public functions. I work with a team, and unless I document things careful and explain what each macro does, the team will have no idea what code a macro is generating. It's frustrating because otherwise, Xcode generates very nice documentation for Swift code. I'm really curious how Lean's doc-gen4 compares here.

Let's look at an example: docs#UInt8.zero_def, docs#UInt16.zero_def, etc were all generated by a macro, but docgen4 seems to document them fine. In fact, you can even see the docs#commandDeclare_uint_theorems__ at the top of the docs for that file!

[misterdrgn]

@Aaron Liu Thank you as always for the thorough response. That’s what I was hoping for.