Zulip Chat Archive

Stream: general

Topic: parser/elaborator feature request


view this post on Zulip Kenny Lau (Jul 05 2020 at 20:51):

Could we expand the scope of @ (make implicit arguments explicit) to expressions as well?

view this post on Zulip Kenny Lau (Jul 05 2020 at 20:52):

constant foo :  (m : ) {n : } (p : ), 

#check @foo 0 1 2   -- works
#check @(foo 0) 1 2 -- fails

view this post on Zulip Simon Hudon (Jul 05 2020 at 20:56):

That's probably something you can write your own function to do

view this post on Zulip Kenny Lau (Jul 05 2020 at 20:58):

as in C++ code?

view this post on Zulip Simon Hudon (Jul 05 2020 at 20:59):

No, I'm thinking of a Lean function where you write a tactic to build it's type

view this post on Zulip Simon Hudon (Jul 05 2020 at 21:01):

It's less obvious to make than I thought actually

view this post on Zulip Simon Hudon (Jul 05 2020 at 21:02):

Maybe a macro (like format!) would be a good approach to make it work

view this post on Zulip Simon Hudon (Jul 05 2020 at 21:14):

Try this:

import tactic
open tactic

reserve prefix `elab! `:100

setup_tactic_parser
open lean

meta def explicit_binder : expr  expr
| (expr.pi n _ d b) :=
  expr.pi n binder_info.default d $ explicit_binder b
| e := e

@[user_notation]
meta def elab_macro (_ : parse $ tk "elab!") (e : parse texpr) : lean.parser pexpr :=
do e  to_expr e.mk_explicit,
   t  infer_type e,
   let t := explicit_binder t,
   return $ ``(@id %%t %%e)

#check (elab! function.comp) 

view this post on Zulip Simon Hudon (Jul 05 2020 at 21:21):

Still not great

view this post on Zulip Simon Hudon (Jul 05 2020 at 21:24):

In any case, you might like what Leo is putting in the Lean 4 elaborator. He's adding named arguments. You should be able to write foo 0 (n := 1) (p := 2)

view this post on Zulip Mario Carneiro (Jul 05 2020 at 21:51):

I also think that @ should work on expressions. There isn't really a reason not to, and it's one of the reasons why the pretty printer doesn't round trip

view this post on Zulip Simon Hudon (Jul 05 2020 at 21:52):

Why is that?

view this post on Zulip Mario Carneiro (Jul 05 2020 at 21:52):

You can't write @(\lam {x : nat}, x) 1

view this post on Zulip Mario Carneiro (Jul 05 2020 at 21:53):

it means that there are some terms that can't be printed in a way where they will be parsed correctly

view this post on Zulip Mario Carneiro (Jul 05 2020 at 21:55):

def foo := by have := (λ {x : }, x); exact @this 1

set_option pp.all true
#print foo

example :=
@(λ {x : nat}, x) (@has_one.one.{0} nat nat.has_one)

view this post on Zulip Mario Carneiro (Jul 05 2020 at 21:57):

That said, I don't think that kenny's example should work. If you write (foo 0) then that should mean foo 0 _ so @(foo 0) 1 2 means @foo 0 _ 1 2. The correct version would be @(@foo 0) 1 2

view this post on Zulip Mario Carneiro (Jul 05 2020 at 22:00):

It also would make sense for #check λ {x : ℕ}, x to have type

view this post on Zulip Simon Hudon (Jul 05 2020 at 22:00):

Right, that's the issue that I've been having with it. But if foo takes another implicit argument before 0 that's where @ makes a functional applicative too verbose

view this post on Zulip Mario Carneiro (Jul 05 2020 at 22:01):

I'm sorry, I don't understand the objection

view this post on Zulip Simon Hudon (Jul 05 2020 at 22:03):

Kenny's example get more interesting if you have this type:

constant foo :  {q : } (m : ) {n : } (p : ), 

view this post on Zulip Simon Hudon (Jul 05 2020 at 22:05):

Then, your solution @(@foo 0) 1 2 would have to be @(@foo 7 0) 1 2. I think avoiding that would be one reasonable argument for applying @ on a partial application

view this post on Zulip Mario Carneiro (Jul 05 2020 at 22:05):

Did I miss anything?

constant foo :  {a : } (m : ) {n : } (p : ), 
#check (@foo a) -- @foo a
#check (foo m) -- @foo _ m _
#check @(foo m) -- @foo _ m
#check @(@foo a m) -- @foo a m
#check @(foo _) -- @foo _ _
#check (@foo a m) p -- @foo a m _ p

view this post on Zulip Simon Hudon (Jul 05 2020 at 22:06):

I don't get your question. Are you asking if your enumeration of desired behavior is exhaustive?

view this post on Zulip Mario Carneiro (Jul 05 2020 at 22:07):

I'm proposing a particular meaning for @ on an expression and giving examples. Is there a problem case somewhere that I haven't demonstrated

view this post on Zulip Floris van Doorn (Jul 05 2020 at 22:40):

FYI: In Lean 2 you were able to apply @ to an expression, and it worked in exactly the way you would expect. I don't know what problem was solved by disallowing it in Lean 3.

view this post on Zulip Simon Hudon (Jul 05 2020 at 22:44):

@Mario Carneiro What I understood of your suggestion was this here:

#check @(foo m) -- @foo _ m _

Notice that it has one underscore than the list you showed. That is something I'm on the fence about

view this post on Zulip Mario Carneiro (Jul 05 2020 at 22:47):

Yeah I confused myself about that too (and #check (λ {x : ℕ}, x) : ℕ is another example of the problem). If we view it strictly compositionally, then by the time you see the @ the expression has already had implicits inserted, which is too late

view this post on Zulip Mario Carneiro (Jul 05 2020 at 22:48):

I think one desideratum is that @ on expressions should have the same effect as @foo when the expression is the local constantfoo

view this post on Zulip Mario Carneiro (Jul 05 2020 at 22:51):

but this means that @(foo m) yields @foo _ m even though (foo m) is @foo _ m _

view this post on Zulip Mario Carneiro (Jul 05 2020 at 22:52):

If @(foo m) means @foo _ m _ then this negates the point of @ on expressions

view this post on Zulip Simon Hudon (Jul 05 2020 at 22:54):

I agree. That's how to make it the most useful. Does that make it a bit weird?

view this post on Zulip Mario Carneiro (Jul 05 2020 at 22:55):

I think it means that @ modifies the context of the expression inside the parens to tell it not to insert final implicits

view this post on Zulip Mario Carneiro (Jul 05 2020 at 23:06):

Put another way, elaboration works one "application group" at a time, with behavior modified by the @ at the head constant, as well as potentially an @ around the whole expression. Here's an enumeration of cases:

constant foo :  {a : } {C :   Type} (b : ) {c : }, C 0
variables {a : } {C :   Type} (b : ) {c : }

#check @foo -- @foo
#check @foo a -- @foo a
#check @foo a C -- @foo a C
#check @foo a C b -- @foo a C b
#check @foo a C b c -- @foo a C b c
#check @@foo -- @foo _
#check @@foo C -- @foo _ C
#check @@foo C b -- @foo _ C b _
#check foo -- @foo _ _
#check foo b -- @foo _ _ b _

#check @(@foo) -- @foo
#check @(@foo a) -- @foo a
#check @(@foo a C) -- @foo a C
#check @(@foo a C b) -- @foo a C b
#check @(@foo a C b c) -- @foo a C b c
#check @(@@foo) -- @foo
#check @(@@foo C) -- @foo _ C
#check @(@@foo C b) -- @foo _ C b
#check @(foo) -- @foo
#check @(foo b) -- @foo _ _ b

view this post on Zulip Mario Carneiro (Jul 05 2020 at 23:07):

The effect of @@(...) is the same as @(...), namely to suppress all insertions of trailing implicit args

view this post on Zulip Mario Carneiro (Jul 05 2020 at 23:09):

This ensures that @(foo) always means the same as @foo

view this post on Zulip Mario Carneiro (Jul 05 2020 at 23:11):

This means that \lam {x}, ... can't be written as is because it will have implicits immediately inserted, unless you protect it with @:

#check λ {x : }, x -- @(λ {x : ℕ}, x) _
#check (λ {x : }, x) -- @(λ {x : ℕ}, x) _
#check @(λ {x : }, x) -- @(λ {x : ℕ}, x)
#check @(λ {x : }, x) 0 -- @(λ {x : ℕ}, x) 0

view this post on Zulip Mario Carneiro (Jul 05 2020 at 23:14):

@Floris van Doorn After going through these cases, it's not clear to me what "exactly what you would expect" means anymore. Could you elaborate on lean 2 @?

view this post on Zulip Floris van Doorn (Jul 05 2020 at 23:57):

I typically used it when (partially) applying a constant to arguments, if you want to leave the first implicit arguments implicit, but make all later arguments explicit. For example, this worked:

constant foo :  {a : } (b : ) {c : } (d : ) {e : }, 
variables {a : } (b : ) {c : } (d : ) {e : }

#check (@(foo b) c d e : )

I think the binder type for lambdas was usually/always ignored when elaborating: it would not immediately apply the function to an argument.

view this post on Zulip Mario Carneiro (Jul 06 2020 at 00:13):

I wonder if we can bring back the !foo annotation too while we're at it

view this post on Zulip Simon Hudon (Jul 06 2020 at 00:31):

What did it do?

view this post on Zulip Mario Carneiro (Jul 06 2020 at 00:31):

it makes all arguments implicit

view this post on Zulip Mario Carneiro (Jul 06 2020 at 00:31):

!foo = foo _ _ _ _

view this post on Zulip Simon Hudon (Jul 06 2020 at 00:32):

Is that useful? Maybe you'd rather have something like Coq's Set Implicit Arguments command.

view this post on Zulip Mario Carneiro (Jul 06 2020 at 00:32):

It's local to the particular application

view this post on Zulip Mario Carneiro (Jul 06 2020 at 00:33):

It's basically the opposite of @foo

view this post on Zulip Floris van Doorn (Jul 06 2020 at 00:51):

In the Lean 2 HoTT library the ! was used all over the place. We made many arguments explicit, because you could easily write !foo if you didn't want to write them explicitly.

view this post on Zulip Simon Hudon (Jul 06 2020 at 01:24):

If you have foo : \Pi a, a -> b, is there a way to omit a but not the parameter of type a?

view this post on Zulip Mario Carneiro (Jul 06 2020 at 01:31):

Not using ! and @

view this post on Zulip Mario Carneiro (Jul 06 2020 at 01:32):

lean 2 also had regular implicit arguments, that's what you would use in that example

view this post on Zulip Simon Hudon (Jul 06 2020 at 01:33):

Ok, I think I see why that's useful. If you have !foo = x, x can dictate the implicit arguments of foo, is that right?

view this post on Zulip Mario Carneiro (Jul 06 2020 at 01:34):

yes

view this post on Zulip Simon Hudon (Jul 06 2020 at 01:34):

I see

view this post on Zulip Mario Carneiro (Jul 06 2020 at 01:34):

also in theorem applications it is very common for our usual implicitness method to be too conservative

view this post on Zulip Simon Hudon (Jul 06 2020 at 01:37):

You mean with apply or when proving a proof term?

view this post on Zulip Mario Carneiro (Jul 06 2020 at 01:55):

in proof terms

view this post on Zulip Mario Carneiro (Jul 06 2020 at 01:56):

Our usual convention says anything that can be inferred from the hypotheses (not the goal) is implicit, but in theorem applications, working backwards, the goal is usually known

view this post on Zulip Simon Hudon (Jul 06 2020 at 01:59):

That's true

view this post on Zulip Simon Hudon (Jul 06 2020 at 01:59):

That might even make proof terms more robust

view this post on Zulip Mario Carneiro (Jul 06 2020 at 02:00):

I usually write foo _ _ for arguments I want inferred, even if I know what should go in the _

view this post on Zulip Simon Hudon (Jul 06 2020 at 02:01):

That's flexible enough. It still breaks if the number of arguments or implicit arguments changes

view this post on Zulip Mario Carneiro (Jul 06 2020 at 02:01):

is that actually reliable though? I would be pretty surprised if the number of arguments changes but the term still unifies

view this post on Zulip Mario Carneiro (Jul 06 2020 at 02:02):

unless it was a duplicate / unused argument or something

view this post on Zulip Simon Hudon (Jul 06 2020 at 02:06):

I think the most likely situation that this would help with is if explicit arguments become implicit or vice versa

view this post on Zulip Kenny Lau (Aug 11 2020 at 16:25):

constant foo :  (m : ) n :  (p : ), 
#check @id _ (foo 0) 1 2

view this post on Zulip Kenny Lau (Aug 11 2020 at 16:25):

@Mario Carneiro look I made it work using {{}} and id

view this post on Zulip Mario Carneiro (Aug 11 2020 at 16:27):

that is unexpected

view this post on Zulip Kenny Lau (Aug 11 2020 at 16:31):

that's what you get by learning Lean using machine learning (i.e. having me just explore things)

view this post on Zulip Kenny Lau (Aug 11 2020 at 16:31):

you get unexpected results


Last updated: May 17 2021 at 22:15 UTC