## Stream: general

### Topic: random parser facts

#### Mario Carneiro (Mar 12 2019 at 00:07):

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 (Mar 12 2019 at 00:16):

who would read the lean source...

#### Mario Carneiro (Mar 12 2019 at 00:18):

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

#### Mario Carneiro (Mar 12 2019 at 00:56):

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 (Mar 12 2019 at 00:58):

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

#### Mario Carneiro (Mar 12 2019 at 00:58):

nonsequitur much?

#### Kenny Lau (Mar 12 2019 at 00:59):

yeah sorry it's a random remark

#### Mario Carneiro (Mar 12 2019 at 01:00):

I suppose random facts are on topic here

#### Kenny Lau (Mar 12 2019 at 01:00):

so what do you think anyway

#### Kenny Lau (Mar 12 2019 at 01:00):

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

#### Kenny Lau (Mar 12 2019 at 01:00):

I suppose there's no way around this

#### Mario Carneiro (Mar 12 2019 at 01:04):

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 (Mar 12 2019 at 01:05):

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

#### Mario Carneiro (Mar 12 2019 at 01:12):

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 (Mar 12 2019 at 01:13):

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

#### Kenny Lau (Mar 12 2019 at 01:13):

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

#### Mario Carneiro (Mar 12 2019 at 01:14):

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 (Mar 12 2019 at 01:15):

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

I see

#### Mario Carneiro (Mar 12 2019 at 01:15):

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

#### Sebastian Ullrich (Mar 13 2019 at 09:25):

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.

what? news to me

#### Sebastian Ullrich (Mar 13 2019 at 09:27):

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

#### Mario Carneiro (Mar 13 2019 at 09:27):

that's pretty cool though

#### Mario Carneiro (Mar 13 2019 at 09:28):

I like the idea of expression-local notations

#### Sebastian Ullrich (Mar 13 2019 at 09:28):

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

#### Mario Carneiro (Mar 13 2019 at 09:28):

structure has something similar with those (infix bla) binders

#### Sebastian Ullrich (Mar 13 2019 at 09:29):

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 (Mar 13 2019 at 09:29):

What about an infix tactic? How hard is that?

#### Mario Carneiro (Mar 13 2019 at 09:30):

that seems more doable and just as expressive

#### Mario Carneiro (Mar 13 2019 at 09:31):

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

#### Sebastian Ullrich (Mar 13 2019 at 09:31):

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

#### Mario Carneiro (Mar 13 2019 at 09:32):

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

#### Mario Carneiro (Mar 13 2019 at 09:33):

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

#### Mario Carneiro (Mar 13 2019 at 09:33):

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

#### Sebastian Ullrich (Mar 13 2019 at 09:33):

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 (Mar 13 2019 at 09:34):

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

#### Mario Carneiro (Mar 13 2019 at 09:35):

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 (Mar 13 2019 at 09:36):

Some kind of super quoting expression should be available

#### Mario Carneiro (Mar 13 2019 at 09:37):

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 (Mar 13 2019 at 09:41):

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

#### Sebastian Ullrich (Mar 13 2019 at 09:49):

@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 (Mar 13 2019 at 09:50):

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

#### Sebastian Ullrich (Mar 13 2019 at 09:51):

It's certainly not changed at tactic execution time

#### Mario Carneiro (Mar 13 2019 at 09:51):

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

#### Mario Carneiro (Mar 13 2019 at 09:53):

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 (Mar 13 2019 at 09:53):

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

#### Kevin Buzzard (Mar 13 2019 at 11:27):

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 (Mar 13 2019 at 11:31):

Oh that's trivial

Last updated: May 15 2021 at 02:11 UTC