I find that at the granularity you need to work with current LLMs to get a good enough output, while verifying its correctness is more effort than writing code directly. The usefulness of LLMs to me is to point me in a direction that I can then manually verify and implement.
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.
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
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`.
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?
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.)
One pattern that I have frequently used in EMACS elisp is that redefining a top-level value overwrites that value rather than shadowing it. Basically hot reloading. This doesn't work in a dependently typed context as the type of subsequent definitions can depend on values of earlier definitions.
def t := string
def x: t := "asdf"
redef t := int
redefining t here would cause x to fail to type check. So the only options are to either shadow the variable t, or have redefinitions type-check all terms whose types depend on the value being redefined.
Excluding the type-level debugging they mention, I think a lean style language-server is a better approach. Otherwise you are basically using an append-only ed to edit your environment rather than a vi.
I've fantasized about some kind of a dependently-typed Smalltalk-like thing before, and in those fantasies the solution would be that changes would be submitted in the form of transactions - they wouldn't be live until you bundled them all together into one big change that would be fully type-checked, as you describe.
I just wrote redef to emphasize that I'm not shadowing the original definition.
def a := 1
def f x := a * x
-- at this point f 1 evaluates to 1
redef a := 2
-- at this point f 1 evaluates to 2
But with dependent types, types can depend on prior values (in the previous example the type of x depends on the value t in the most direct way possible, as the type of x is t). If you redefine values, the subsequent definitions may not type-check anymore.
I see what you mean. But would you not experience the same sort of issue simply from redefining types in the same way? It seems this kind of destructive operation (whether on types or terms) is the issue. As someone who's used to ML, it seems strange to allow this kind of thing (instead of simply shadowing), but maybe it's a Lisp thing?
There is a large library of mathematics formalized in lean called mathlib. There are graphs for the module dependencies, but I haven't seen any at the level of definitions (including lemmas and theorems).
That'd almost be partial functions with extra steps. Take the Klesili category with the Maybe Monad,and you get partial functions.
Unless you are manually matching on the the Maybe, and thus observing the timeout, then that isn't the case. You'd probably also want a nondetermism effect which cannot handle unless you specifically build your timeouts to be deterministic, which I think Lean 4 does, but you can't go from partial to total with it afaik.
