[HN Gopher] Binding Application in Idris
       ___________________________________________________________________
        
       Binding Application in Idris
        
       Author : matt_d
       Score  : 72 points
       Date   : 2025-07-10 23:08 UTC (3 days ago)
        
 (HTM) web link (andrevidela.com)
 (TXT) w3m dump (andrevidela.com)
        
       | reuben364 wrote:
       | 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 wrote:
         | 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
        
         | kmill wrote:
         | 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 wrote:
           | 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?
        
       ___________________________________________________________________
       (page generated 2025-07-14 23:01 UTC)