Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: parsing type class instance

Xavier Martinet (Feb 02 2022 at 17:04):

Hi,

I am trying to parse the following string (this is @dvd_pow.{0}):

"∀ {M : Type} [_inst_1 : comm_monoid M] {x y : M}, x ∣ y → ∀ {n : ℕ}, n ≠ 0 → x ∣ y ^ n"

(btw, thanks to threads initiated by @Joe Palermo, I was able to handle the case for an arbitrary universe u vs only Type)

I am doing it this way:

def mystr := "∀ {M : Type} [_inst_1 : comm_monoid M] {x y : M}, x ∣ y → ∀ {n : ℕ}, n ≠ 0 → x ∣ y ^ n"

#eval lean.parser.run_with_input (lean.parser.pexpr 0 tt) mystr >>= tactic.i_to_expr >>= tactic.trace
/-
failed to synthesize type class instance for
M : Type,
_inst_1 : comm_monoid M,
x y : M,
ᾰ : x ∣ y,
n : ℕ,
ᾰ : n ≠ 0
⊢ has_pow M ℕ
-/

I have tried different things with lean.parser.add_local, to no avail.

Even this is suprisingly not working:

variables {M : Type} [comm_monoid M]

def mystr := "∀ {x y : M}, x ∣ y → ∀ {n : ℕ}, n ≠ 0 → x ∣ y ^ n"

#eval lean.parser.run_with_input (lean.parser.pexpr 0 tt) mystr >>= tactic.i_to_expr >>= tactic.trace
-- unknown identifier 'M'

Why does the elaborator needs to find a class instance? I mean, it could just see that [_inst_1 : comm_monoid M] is a Π-binder such as `expr.pi `_inst_1 binder_info.strict_implicit <comm_monoid M> <body> ? What am I not getting right?

Xavier Martinet (Feb 02 2022 at 17:09):

(btw there is no such problem with @Joe Palermo example:

def mystr := "Π {α : Type u} [_inst_1 : linear_ordered_add_comm_group α] [_inst_1 : linear_ordered_add_comm_monoid α], linear_ordered_add_comm_monoid_with_top (with_top α)"

#eval lean.parser.run_with_input (do lean.parser.add_local_level "u", lean.parser.pexpr 0 tt) mystr >>= tactic.i_to_expr >>= tactic.trace
/-
Π {α : Type u} [_inst_1 : linear_ordered_add_comm_group α] [_inst_1 : linear_ordered_add_comm_monoid α],
  linear_ordered_add_comm_monoid_with_top (with_top α)
-/

Alex J. Best (Feb 02 2022 at 17:35):

Please include your imports so that your code examples work out of the box (#mwe).
The issue here is that lean doesn't reset the instance cache while reading an expression,
just running

import algebra.group.basic
import algebra.divisibility

#check ∀ {M : Type} [_inst_1 : comm_monoid M] {x y : M},  x ∣ y → ∀ {n : ℕ}, n ≠ 0 → x ∣ y ^ n

gives the same error, one way to get around this is to enter tactic mode and reset the cache, with the by exactI trick, I don't know if this is useful for what you are trying to do though

import algebra.group.basic
import algebra.divisibility


def mystr := "∀ {M : Type} [_inst_1 : comm_monoid M] {x y : M}, by exactI  x ∣ y → ∀ {n : ℕ}, n ≠ 0 → x ∣ y ^ n"

#eval lean.parser.run_with_input (lean.parser.pexpr 0 tt) mystr >>= tactic.i_to_expr >>= tactic.trace

Xavier Martinet (Feb 03 2022 at 09:40):

Yes! this is what I was after, thanks a lot :)

My understanding of the type class instance caching is the following:
1) there is somewhere a lookup table of type class instances, that gets updated at each instance declaration
2) during elaboration, the elaborator, instead of looking at that lookup table, pings a cache for performance reasons
question: I find it surprising because there are not that many instances, right? and a key-value store is implemented in Lean with a red-black tree, so it has O(log n) complexity - and actually, since elaboration is done in C++, nothing could prevent it to be implemented with a hash map, so with O(1) complexity, what is the benefit of a cache then?
3) this cache is updated when there is a def (or theorem, or lemma, but not with have) in which there is a strictly-implicity parameter (left of colon in the function signature)
4) when the elaborator tries to elaborate the expr at the right of the colon, it pings that cache; if there is some strictly-implicity binder there, unless it was added in the cache previously by parameters at the left of the colon, it fails to elaborate ("synthesize", in the error message) the type class instance
question: then why is it working in the Joe Palermo's example?
5) tactic.unfreeze_local_instances >> tactic.freeze_local_instances, after some strictly-implicit binder, will delete the cache and force it to be recomputed (adding the binder), and then will freeze it again

Is my understanding correct?
Would you by any chance know what I am not getting right in 2) and 4)?

Xavier Martinet (Feb 03 2022 at 10:13):

And also, what is wrong here?

import algebra.group.basic
import algebra.divisibility

def mystr := "do tactic.unfreeze_local_instances,
tactic.exact  $ ∀ {M : Type} [_inst_1 : comm_monoid M] {x y : M},  x ∣ y → ∀ {n : ℕ}, n ≠ 0 → x ∣ y ^ n,
tactic.freeze_local_instances"

#eval lean.parser.run_with_input (lean.parser.pexpr 0 tt) mystr >>= tactic.i_to_expr >>= tactic.trace
/-
failed to synthesize type class instance for
_x : unit,
M : Type,
_inst_1 : comm_monoid M,
x y : M,
ᾰ : x ∣ y,
n : ℕ,
ᾰ : n ≠ 0
⊢ has_pow M ℕ
-/

Anne Baanen (Feb 03 2022 at 10:13):

Xavier Martinet said:

My understanding of the type class instance caching is the following:
1) there is somewhere a lookup table of type class instances, that gets updated at each instance declaration
2) during elaboration, the elaborator, instead of looking at that lookup table, pings a cache for performance reasons
question: I find it surprising because there are not that many instances, right? and a key-value store is implemented in Lean with a red-black tree, so it has O(log n) complexity - and actually, since elaboration is done in C++, nothing could prevent it to be implemented with a hash map, so with O(1) complexity, what is the benefit of a cache then?

There are about seven thousand instance declarations in mathlib (and I'd estimate a few thousand more generated by an extends clause or through metaprogramming such as @[to_additive])

The instance cache in Lean 3 is implemented using a C++ std::unordered_map, which I understand is typically implemented as a hashmap. One drawback of a hashmap is that we cannot update it easily: if the instance is only available in some subterm we have to copy the whole cache.

Anne Baanen (Feb 03 2022 at 10:15):

Avoiding making a copy for each subterm is why the cache gets frozen, according to this comment

Anne Baanen (Feb 03 2022 at 10:18):

3) this cache is updated when there is a def (or theorem, or lemma, but not with have) in which there is a strictly-implicity parameter (left of colon in the function signature)

As I understand it, anything added left of the colon can appear in the cache. So also

def add {α : Type*} (h : has_add α) : α → α → α := (+)

would add h to the cache.

Anne Baanen (Feb 03 2022 at 10:28):

4) when the elaborator tries to elaborate the expr at the right of the colon, it pings that cache; if there is some strictly-implicity binder there, unless it was added in the cache previously by parameters at the left of the colon, it fails to elaborate ("synthesize", in the error message) the type class instance

Minor correction: the cache is always used, it just gets frozen to the right of the colon. And to be clear, synthesis also uses globally declared instances, not just the locals that are currently in scope.

Anne Baanen (Feb 03 2022 at 10:34):

The important thing here is that the cache doesn't just contain a list of available instances, it also contains a list of which goals have succesfully found an instance and which haven't. That significantly speeds up handling of diamond inheritance:

A₀
↑
A₁ extends A₀
↑
A₂ extends A₁
↑
...
↑
B ← C
↑   ↑
D ← E

Now if we search for an instance of E without an instance of A₀ available, we'll first try C.to_E → B.to_C → ... → A₁.to_A₀ failure, then mark the whole chain from C to A₀ as failed, including B. Then we try D.to_E → B.to_D, encounter a cached failure for B and stop without traversing the whole chain up to A₀ again.

Last updated: Dec 20 2023 at 11:08 UTC