## Stream: general

### Topic: parser/elaborator feature request

#### Kenny Lau (Jul 05 2020 at 20:51):

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

#### 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


#### Simon Hudon (Jul 05 2020 at 20:56):

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

as in C++ code?

#### 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

#### Simon Hudon (Jul 05 2020 at 21:01):

It's less obvious to make than I thought actually

#### Simon Hudon (Jul 05 2020 at 21:02):

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

#### 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) ℤ


Still not great

#### 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)

#### 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

Why is that?

#### Mario Carneiro (Jul 05 2020 at 21:52):

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

#### 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

#### 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)


#### 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

#### Mario Carneiro (Jul 05 2020 at 22:00):

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

#### 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

#### Mario Carneiro (Jul 05 2020 at 22:01):

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

#### 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 : ℕ), ℕ


#### 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

#### 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


#### 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

#### 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.

#### Simon Hudon (Jul 05 2020 at 22:44):

#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

#### 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

#### 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

#### Mario Carneiro (Jul 05 2020 at 22:51):

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

#### Mario Carneiro (Jul 05 2020 at 22:52):

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

#### 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?

#### 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

#### 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


#### Mario Carneiro (Jul 05 2020 at 23:07):

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

#### Mario Carneiro (Jul 05 2020 at 23:09):

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

#### 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


#### 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 @?

#### 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.

#### Mario Carneiro (Jul 06 2020 at 00:13):

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

What did it do?

#### Mario Carneiro (Jul 06 2020 at 00:31):

it makes all arguments implicit

#### Mario Carneiro (Jul 06 2020 at 00:31):

!foo = foo _ _ _ _

#### Simon Hudon (Jul 06 2020 at 00:32):

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

#### Mario Carneiro (Jul 06 2020 at 00:32):

It's local to the particular application

#### Mario Carneiro (Jul 06 2020 at 00:33):

It's basically the opposite of @foo

#### 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.

#### 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?

#### Mario Carneiro (Jul 06 2020 at 01:31):

Not using ! and @

#### Mario Carneiro (Jul 06 2020 at 01:32):

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

#### 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?

yes

I see

#### 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

#### Simon Hudon (Jul 06 2020 at 01:37):

You mean with apply or when proving a proof term?

in proof terms

#### 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

That's true

#### Simon Hudon (Jul 06 2020 at 01:59):

That might even make proof terms more robust

#### 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 _

#### Simon Hudon (Jul 06 2020 at 02:01):

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

#### 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

#### Mario Carneiro (Jul 06 2020 at 02:02):

unless it was a duplicate / unused argument or something

#### 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

#### Kenny Lau (Aug 11 2020 at 16:25):

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


#### Kenny Lau (Aug 11 2020 at 16:25):

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

#### Mario Carneiro (Aug 11 2020 at 16:27):

that is unexpected

#### 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)

#### Kenny Lau (Aug 11 2020 at 16:31):

you get unexpected results

Last updated: May 17 2021 at 22:15 UTC