parser/elaborator feature request

Stream: general

[Kenny Lau]

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

[Kenny Lau]

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

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

[Simon Hudon]

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

[Kenny Lau]

as in C++ code?

[Simon Hudon]

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

[Simon Hudon]

It's less obvious to make than I thought actually

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

Still not great

[Simon Hudon]

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]

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

[Simon Hudon]

Why is that?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Simon Hudon]

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]

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

[Simon Hudon]

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

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

[Simon Hudon]

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]

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

[Simon Hudon]

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

[Mario Carneiro]

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]

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]

@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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

@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]

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]

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

[Simon Hudon]

What did it do?

[Mario Carneiro]

it makes all arguments implicit

[Mario Carneiro]

!foo = foo _ _ _ _

[Simon Hudon]

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

[Mario Carneiro]

It's local to the particular application

[Mario Carneiro]

It's basically the opposite of @foo

[Floris van Doorn]

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]

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

[Mario Carneiro]

Not using ! and @

[Mario Carneiro]

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

[Simon Hudon]

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?

[Mario Carneiro]

yes

[Simon Hudon]

I see

[Mario Carneiro]

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

[Simon Hudon]

You mean with apply or when proving a proof term?

[Mario Carneiro]

in proof terms

[Mario Carneiro]

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

[Simon Hudon]

That's true

[Simon Hudon]

That might even make proof terms more robust

[Mario Carneiro]

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

[Simon Hudon]

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

[Mario Carneiro]

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

[Mario Carneiro]

unless it was a duplicate / unused argument or something

[Simon Hudon]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

that is unexpected

[Kenny Lau]

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

[Kenny Lau]

you get unexpected results