Need help to understand strict implicit vs implicit

Stream: new members

[Kevin Cheung]

There are a few theorems in Finset that contain strict implicits. I am not quite getting what the documentation about strict implicit says: "Strict-implicit binder. In contrast to { ... } regular implicit binders, a strict-implicit binder is inserted automatically only when at least one subsequent explicit parameter is specified."

Suppose I have something simple like the following:

def bar ⦃m : ℕ⦄ { n : ℕ } (q : ℕ) (_ : Fin m) (_ : Fin n)  := m * n * q

How would strict implicit around m here behave differently as opposed to being just an implicit?

[Kyle Miller]

Let's compare strict implicit and regular implicits:

def bar ⦃m : ℕ⦄ { n : ℕ } (q : ℕ) (_ : Fin m) (_ : Fin n)  := m * n * q
def bar' {m : ℕ} { n : ℕ } (q : ℕ) (_ : Fin m) (_ : Fin n)  := m * n * q

/-
Using parentheses forces `#check` to show you the type of the expression,
rather than giving a declaration-style signature for a constant.
-/
#check (bar)
-- bar : ⦃m : ℕ⦄ → {n : ℕ} → ℕ → Fin m → Fin n → ℕ
#check (bar')
-- bar' : ℕ → Fin ?m.9034 → Fin ?m.9035 → ℕ
#check @bar'
-- @bar' : {m n : ℕ} → ℕ → Fin m → Fin n → ℕ
#check bar 1
-- bar 1 : Fin ?m.9037 → Fin ?m.9038 → ℕ
#check bar' 1
-- bar' 1 : Fin ?m.9055 → Fin ?m.9056 → ℕ

[Kyle Miller]

Notice that bar keeps the m argument, but bar' immediately turns it into a metavariable (?m.9034 here).

[Kevin Cheung]

Interesting. So why do #check bar 1 and #check bar' 1 seem to be the same?

[Kyle Miller]

They're both filling in q with 1, so in both cases m is treated as an implicit.

[Kevin Cheung]

So in this case, there is really no practical reason to use strict implicit?

[Kyle Miller]

Strict implicits behave like regular implicits so long as an explicit argument is provided after it.

[Kyle Miller]

If you want to be able to pass bar around while preserving that m could be anything, then strict implicits are useful.

[Kevin Cheung]

Let me if I understand this. Once Lean assigns a metavariable (e.g. ?m.9034), it's fixed for the rest of the code? But having it as m means it can change depending on who accepts bar as an argument?

[Kyle Miller]

Yeah, exactly.

[Kyle Miller]

Many times, rather than strict implicits, you can make it be an explicit argument and then pass _ for that argument when you want to simulate regular implicits.

[Kevin Cheung]

Thank you. I wish your explanation could be found in a book somewhere.

[Kyle Miller]

I don't have the best sense of when strict implicits are useful, but they can be useful for properties like ∀ ⦃x⦄, x ∈ s → x ∈ t, since then x stays free until you pass in the "actual" data, the proof of x ∈ s

[Kyle Miller]

With ∀ x ∈ s, x ∈ t notation (available in mathlib), maybe it should make the x be a strict implicit, but for now it's explicit. (That is, the current meaning is ∀ x, x ∈ s → x ∈ t.)

[Kevin Cheung]

I see. Now, it makes sense.

[Eric Rodriguez]

Kyle Miller said:

With ∀ x ∈ s, x ∈ t notation (available in mathlib), maybe it should make the x be a strict implicit, but for now it's explicit. (That is, the current meaning is ∀ x, x ∈ s → x ∈ t.)

I think for these binders it'd be nice to have these be configurable to be whatever level of implicitness is right

[Kevin Cheung]

How would such configurability look like?

[Eric Rodriguez]

maybe something crazy like ∀ ({x} ∈ s), x ∈ t