Binding Application in Idris(andrevidela.com)
86 pointsby matt_d9 days ago1 comment
  • reuben3645 days 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.
    • andrevidela5 days 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

    • kmill5 days 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`.

      • JoelMcCracken5 days 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?
        • kmill5 days ago
          The system used in Lean 4 is explained in https://arxiv.org/abs/2001.10490v7 (Ullrich and Moura, "Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages").

          There's still a set-of-scopes system, but it seems to be pretty different from https://users.cs.utah.edu/plt/scope-sets/ (And to clarify what I wrote previously, each identifier has a list of macro scopes.)

          The set-of-scopes in Lean 4 is for correct expansion of macro-creating-macros. The scopes are associated to macro expansions rather than binding forms. Lean's syntax quotations add the current macro scope to every identifier that appears in quotations in the expansion. That way, if there are multiple expansions of the same macro for example, it's not possible for identifiers in the expansion to collide. There's an example in section 3.2 of a macro macro that defines some top-level definitions.

          (Section 8 of the paper, related work, suggests that set-of-scopes in Lean and Racket are closer than I'm understanding; I think what's going on is that Lean has a separate withFreshMacroScope primitive that macros can invoke, and syntax quotations participate in macro scopes, whereas Racket seems to give this responsibility to binding forms, and they're responsible for adding macro scopes to their binders and bodies. I'm a bit unclear on this.)