Binding Application in Idris

https://andrevidela.com/blog/2025/binding-application/

by matt_d • 1 year ago

87 5 1 year ago

reuben364• 1 year ago

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• 1 year 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

kmill2• 1 year ago

In Lean's parsed `Syntax`, binders are plain identifiers. The way this works is that identifiers can be annotated with the module it was parsed in as well as a "macro scope", which is a number that's used to make identifiers created by macros be distinct from any previously created identifiers (the current macro scope is some global state that's incremented whenever a macro is being expanded) — an identifier with this annotation is called a hygienic identifier, and when identifiers are tested for equality the annotations are tested too. With this system in place, there's nothing special you need to do to elaborate binders (and it also lets you splice together syntaxes without any regard for hygiene!). For example, `fun x => b x` elaborates by (1) adding a variable `x` to the local scope, (2) elaborating `b x` in that scope, and then (3) abstracting `x` to make the lambda. The key here is that `x` is a hygienic identifier, so an `x` that's from a different module or macro scope won't be captured by the binder `x`.

Yes you can define the syntax that's in the article in Lean. A version of this is the Mathlib `notation3` command, but it's for defining notation rather than re-using the function name (e.g. using a union symbol for `Set.iUnion`), and also the syntax is a bit odd: notation3 "⋃ "(...)", "r:60:(scoped f => iUnion f) => r

The ideas in the article are neat, and I'll have to think about whether it's something Lean could adopt in some way... Support for nested binders would be cool too. For example, I might be able to see something like `List.all (x in xs) (y in ys) => x + y < 10` for `List.all (fun x => List.all (fun y => x + y < 10) ys) xs`.

JoelMcCracken• 1 year ago

ah nice explanation. I've actually read (or tried to) the "macros as a set of scopes" paper that IIUC lean 4's scoping is based upon; I did watch the talk on lean4's macro system. Does it not have some kind of "set of scopes" tracking?

Binding Application in Idris

Related Stories