Zulip Chat Archive

Stream: general

Topic: random parser facts


view this post on Zulip 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 :=

view this post on Zulip Kenny Lau (Mar 12 2019 at 00:16):

who would read the lean source...

view this post on Zulip Mario Carneiro (Mar 12 2019 at 00:18):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 12 2019 at 00:58):

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

view this post on Zulip Mario Carneiro (Mar 12 2019 at 00:58):

nonsequitur much?

view this post on Zulip Kenny Lau (Mar 12 2019 at 00:59):

yeah sorry it's a random remark

view this post on Zulip Mario Carneiro (Mar 12 2019 at 01:00):

I suppose random facts are on topic here

view this post on Zulip Kenny Lau (Mar 12 2019 at 01:00):

so what do you think anyway

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 12 2019 at 01:00):

I suppose there's no way around this

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 12 2019 at 01:15):

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

view this post on Zulip Kenny Lau (Mar 12 2019 at 01:15):

I see

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:26):

what? news to me

view this post on Zulip Sebastian Ullrich (Mar 13 2019 at 09:27):

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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:27):

that's pretty cool though

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:28):

I like the idea of expression-local notations

view this post on Zulip Sebastian Ullrich (Mar 13 2019 at 09:28):

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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:28):

structure has something similar with those (infix bla) binders

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:29):

What about an infix tactic? How hard is that?

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:30):

that seems more doable and just as expressive

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:31):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:33):

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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:33):

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

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Mar 13 2019 at 09:34):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:36):

Some kind of super quoting expression should be available

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Sebastian Ullrich (Mar 13 2019 at 09:51):

It's certainly not changed at tactic execution time

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:51):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 09:53):

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

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Mar 13 2019 at 11:31):

Oh that's trivial


Last updated: May 15 2021 at 02:11 UTC