What do these double curly braces `⦃⦄` mean?

Stream: new members

[Markus Schmaus]

I was able to find most notations using the docs search but I was unable to find anything on ⦃⦄ even though I've seen them in some places in the source code. What do they do?

[Kyle Miller]

These are part of the core language, "strict implicits". Here are some examples: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Need.20help.20to.20understand.20strict.20implicit.20vs.20implicit/near/419354924

[Kyle Miller]

They're less eager than {} implicit arguments.

[Mario Carneiro]

how far are we from having hovers for strict implicit braces?

[Mario Carneiro]

it appears docs#Lean.Parser.Term.strictImplicitBinder already has docs

[Kyle Miller]

I'm not sure why declSig seems to be the end of the line for hovering, at least until it gets into the binder types.

[Mario Carneiro]

this is that issue with builtin docstrings, I'm sure (it's not a @[builtin_term_parser] itself, but something used in one)

[Markus Schmaus]

Hovers would be great. It would also be great if docs#Lean.Parser.Term.strictImplicitBinder could be found by searching for '⦃'. And lastly that doc string should probably mention the ⦃ ... ⦄ notation.

[Kyle Miller]

Added documentation in lean4#3917 and got the hovers to work

[Mario Carneiro]

lean4#3918 also gets the hovers to work for strict implicits, among other things

[Markus Schmaus]

Now that I understand what they do, why are strict implicits not used more often?

I can think of two cases on when to use implicits. First, most often, when they can be inferred from subsequent arguments. Second, more rarely, when they can be inferred from the return type. It sounds to me that in the first case strict implicits would be more useful, and regular implicits only for the second case.

[Michael Stoll]

I agree. I assume the reason why strict implicts are used fairly sparingly is part historical accident and part laziness (it is easier to type "{" than "\{{").

[Mario Carneiro]

no, I think it is more than that. They were almost dropped from lean 4, we petitioned to add them back

[Mario Carneiro]

they are very deliberately being discouraged

[Michael Stoll]

Why?

[Mario Carneiro]

implicit lambdas mean that lean can often "just figure it out" when you use an expression with implicits unapplied

[Michael Stoll]

theorem foo {α : Type} (a : α) : a = a := rfl

example : True := by
  have := foo -- don't know how to synthesize implicit argument @foo ?m.24
  trivial

theorem bar ⦃α : Type⦄ (a : α) : a = a := rfl

example : True := by
  have := bar -- OK
  trivial

My experience is that when I use a lemma with (usual) implicits unapplied, then Lean complains, because it tries to fill the implicit arguments, but can't do so, because it is missing the information from the later explicit arguments.

[Michael Stoll]

E.g.,

theorem baz : ∀ {n}, n ≥ 37 → n ≠ 0 := sorry

example : True := by
  have := baz -- complains
  trivial

I don't really see the downside of using strict implicits in cases like this.

[Riccardo Brasca]

Indeed do we have a lot of examples where normal implicits are better than strict implicits?

[Markus Schmaus]

I thought about this some more and realized that the distinction I made above isn't as clear cut as I first thought.

By my original argument for a function foo {α β : Type} (x : α) : β, I would have claimed that α can be inferred from a subsequent argument and β from the return type, but the same function signature could also have been written as foo {α β : Type} : α → β, in which case it would appear that both implicit arguments can be referred from the return type.

To make this more concrete consider the function docs#id , by my original argument it may look like a strict implicit for α might sound reasonable, but then this would result in an error in the following example.

def id' ⦃α : Type u⦄ (x : α) : α := x

#eval [1, 2].map id -- works
#eval [1, 2].map id' -- error

For id, lean can infer α from the return type, but for id' it is forbidden to do so.

[Kyle Miller]

I think strict implicits make sense where a sequence of implicit arguments followed by an explicit argument should all be considered to be "one" binder. For example, ∀ n ≥ 37, n ≠ 0 should be ∀ {{n}}, n ≥ 37 → n ≠ 0, since if it expands using {n} it's confusing, leaking an implementation detail of how the n ≥ 37 binder works.

[Kyle Miller]

Though, you do frequently want to pass in n explicitly, leaving the following proof for tactics. I wonder what syntax there could be to pass in a single implicit argument without going into @ explicit mode and without using named arguments?

[Kyle Miller]

Like, if h : ∀ {{n}}, n ≥ 37 → n ≠ 0, maybe you could write h @(5)? Though, right now @(...) is syntax for disabling the implicit lambda feature.

[Vincent Beffara]

Something like h (_ := 5) that would match the first argument?

[Kyle Miller]

That might work