I'm wondering whether such syntax is subsumed by something like Lean 4 macros. I believe Lean 4 already treats binders specially in its syntax for macro hygiene reasons, but I'm not confident in that assertion.
andrevidela•3h ago
Author here.
Not macros but syntax blocks entirely subsume this. The point of the feature is actually to avoid syntax blocks at all cost while providing their most cherished feature: binding names to expressions.
The issue with syntax blocks is that they entirely break any parser for the language since they introduce arbitrary syntactic sugar to the language. That's a cool idea but a disaster in production. It also makes error messages entirely useless because the compiler cannot know if the syntax is wrong because the user is wrong, or if the syntax is wrong because the user forgot to import a module that declares a syntax block.
This is closer to the trailing lambda feature of many existing languages with a dependently-typed twist. It turns out that this is enough to get a proper syntax for Pi, Sigma, and loops
reuben364•4h ago
andrevidela•3h ago
Not macros but syntax blocks entirely subsume this. The point of the feature is actually to avoid syntax blocks at all cost while providing their most cherished feature: binding names to expressions.
The issue with syntax blocks is that they entirely break any parser for the language since they introduce arbitrary syntactic sugar to the language. That's a cool idea but a disaster in production. It also makes error messages entirely useless because the compiler cannot know if the syntax is wrong because the user is wrong, or if the syntax is wrong because the user forgot to import a module that declares a syntax block.
This is closer to the trailing lambda feature of many existing languages with a dependently-typed twist. It turns out that this is enough to get a proper syntax for Pi, Sigma, and loops