random parser facts

Stream: general

[Mario Carneiro]

New discovery while reading the lean source: These are both legal:

structure foo := mk
structure bar := mk ::

and they add a new type isomorphic to unit. (I would have guessed that the second one works, but the first one is a parser trick.) However these don't work:

structure bad
structure bad.
structure bad :=

[Kenny Lau]

who would read the lean source...

[Mario Carneiro]

how else do you learn about undocumented features (and "features")?

[Mario Carneiro]

aha, here is the random parser fact I was looking for: You may know that you can write {} before the binder of a structure or inductive to make the arguments implicit. This is used for example to make list.nil have no explicit args:

structure regular1 (α : Type) (l : list α) := mk :: (foo : nat)
inductive regular2 (α : Type) (l : list α) | mk : regular2

#check @regular1.mk -- regular1.mk : Π {α : Type} (l : list α), ℕ → regular1 α l
#check @regular1.foo -- Π {α : Type} {l : list α}, regular1 α l → ℕ
#check @regular2.mk -- regular2.mk : Π {α : Type} (l : list α), regular2 α l

structure implicit1 (α : Type) (l : list α) := mk {} :: (foo {} : nat)
inductive implicit2 (α : Type) (l : list α) | mk {} : implicit2

#check @implicit1.mk -- implicit1.mk : Π {α : Type} {l : list α}, ℕ → implicit1 α l
#check @implicit1.foo -- implicit1.foo : Π {α : Type} {l : list α}, implicit1 α l → ℕ
#check @implicit2.mk -- implicit2.mk : Π {α : Type} {l : list α}, implicit2 α l

It turns out there is a third mode, triggered by () before the colon instead. But the parser code here is buggy, so you have to put a space between the parens so it doesn't look like the unit star token:

structure explicit1 (α : Type) (l : list α) := mk ( ) :: (foo ( ) : nat)
inductive explicit2 (α : Type) (l : list α) | mk ( ) : explicit2

#check @explicit1.mk -- explicit1.mk : Π (α : Type) (l : list α), ℕ → explicit1 α l
#check @explicit1.foo -- explicit1.foo : Π (α : Type) (l : list α), explicit1 α l → ℕ
#check @explicit2.mk -- explicit2.mk : Π (α : Type) (l : list α), explicit2 α l

[Kenny Lau]

so every def is invoking an instance of the axiom schema...

[Mario Carneiro]

nonsequitur much?

[Kenny Lau]

yeah sorry it's a random remark

[Mario Carneiro]

I suppose random facts are on topic here

[Kenny Lau]

so what do you think anyway

[Kenny Lau]

every structure / inductive / class / def is invoking an axiom of the axiom schema, all in the name of definitional equalities

[Kenny Lau]

I suppose there's no way around this

[Mario Carneiro]

I literally have no idea what you are talking about. It's not related to the context on this thread as far as I can tell

[Kenny Lau]

I mean, when you create an inductive type, you're effectively adding axioms to the system right

[Mario Carneiro]

yes, inductive is a mechanism for using an axiom schema built into lean. structure and class are fancy ways to say inductive, and def is not an axiom in any sense

[Kenny Lau]

you're adding a new constant and adding an axiom that the constant "unfolds" to a certain value

[Kenny Lau]

when you say def n := 5 you're adding the constant n : nat and the axiom n._equations._eqn_1 : n = 5

[Mario Carneiro]

you're adding a new constant and adding an axiom that the constant "unfolds" to a certain value

no, definitions in DTT don't work like this

[Mario Carneiro]

they are abbreviations for certain terms, so there is no axiom of equality

[Kenny Lau]

I see

[Mario Carneiro]

but for practical reasons definitions are supported by the kernel, which implements definition unfolding as a reduction rule

[Sebastian Ullrich]

Ooh, good topic. Did you know that you can let-bind notations like in

#eval let infix + := nat.mul in 1 + 2

? Is anybody using that? Because implementing that in pure Lean is basically impossible and so this will probably not work in Lean 4 and I wonder if anybody will even notice.

[Mario Carneiro]

what? news to me

[Sebastian Ullrich]

Yeah, me too until I read the source some time ago

[Mario Carneiro]

that's pretty cool though

[Mario Carneiro]

I like the idea of expression-local notations

[Sebastian Ullrich]

Well, don't get too attached to it :sweat_smile:

[Mario Carneiro]

structure has something similar with those (infix bla) binders

[Sebastian Ullrich]

Yes, that's okay (more or less, it's a pain in the macro expander), because the extended parser (terms) is not the one being executed (commands)

[Mario Carneiro]

What about an infix tactic? How hard is that?

[Mario Carneiro]

that seems more doable and just as expressive

[Mario Carneiro]

I hope the parser isn't going to end up being a second tactic language

[Sebastian Ullrich]

That's not much better (or worse) because tactic parsing is still part of the big term parser recursion

[Mario Carneiro]

oh, I see... you won't be able to parse the following expressions until you run the tactic

[Mario Carneiro]

but you can't run the tactic until you've parsed the tactic block

[Mario Carneiro]

okay, I'm convinced... kill it with fire

[Sebastian Ullrich]

Yes, it would not be a true tactic but part of the tactic block notation. Then it's no harder or easier than notation-let

[Sebastian Ullrich]

So let's just pretend this feature has never existed...

[Mario Carneiro]

but what about expressions that we want to parse with a parser that we don't have at parse time? I was thinking more like a real infix tactic

[Mario Carneiro]

Some kind of super quoting expression should be available

[Mario Carneiro]

This is also important for many custom parsers... for example if I want to have a block of code in another language inline and parse it with a custom parser

[Johan Commelin]

Would this allow us to take a step towards unifying group and add_group and still have natural notation?

[Sebastian Ullrich]

@Mario Carneiro I'm not sure I'm following. When using a DSL, you usually statically know its grammar and where it can occur in the Lean grammar (e.g. "as the second argument to this tactic"). Then everything works out.

[Mario Carneiro]

heh, I'm familiar with lots of languages where the grammar is not statically known (hint: lean is one of them)

[Sebastian Ullrich]

It's certainly not changed at tactic execution time

[Mario Carneiro]

I was thinking of parsing more like "read random junk until you see STOP_NOW"

[Mario Carneiro]

and then you might have to read another file (analogous to lean imports or oleans) to tell you what tokens are valid and how to parse them

[Mario Carneiro]

and this happens from lean's perspective at tactic execution time

[Kevin Buzzard]

All I want to know is whether we'll be able to do {t * s for t in T, s in S if t \ne 7} for S and T subsets of a monoid

[Sebastian Ullrich]

Oh that's trivial