Zulip Chat Archive

Stream: general

Topic: type class issues


Johan Commelin (Nov 14 2018 at 19:54):

This is amazing: https://gist.githubusercontent.com/jcommelin/8736c28a8e74f3d478b1c2b7737fa513/raw/d655018af064ef75572afb17d2ffb7d051c500c0/crazy_type_class_error.lean
I feel like the algorithm could be a lot smarter here. For example, search for x_52 on that page, and go to the first match. You will be on the last line of this chunk of code:

[class_instances] (1) ?x_32 : category
  (@comma {X // B X}
     (@category_theory.full_subcategory (@opens X _inst_1)
        (@site.to_category (@opens X _inst_1) (@category_theory.site X _inst_1))
        (Ī» (X : @opens X _inst_1), B X))
     punit
     category_theory.punit_category
     (@opens X _inst_1)
     (@site.to_category (@opens X _inst_1) (@category_theory.site X _inst_1))
     (@full_subcategory_inclusion (@opens X _inst_1)
        (@site.to_category (@opens X _inst_1) (@category_theory.site X _inst_1))
        B)
     (@functor.of_obj (@opens X _inst_1) (@site.to_category (@opens X _inst_1) (@category_theory.site X _inst_1)) U)) := @category_theory.comma_category ?x_51 ?x_52 ?x_53 ?x_54 ?x_55 ?x_56 ?x_57 ?x_58

So basically it has already figured out all these type class instances, and it should immediately be able to fill in ?x_52 and friends. But it doesn't... and then it hits the search limit.

Johan Commelin (Nov 14 2018 at 20:10):

[class_instances] (4) ?x_238 : category punit := @category_theory.small_category ?x_422 ?x_423

goes all the way down to

[class_instances] (12) ?x_460 : linear_ordered_field punit := @discrete_linear_ordered_field.to_linear_ordered_field ?x_461 ?x_462

I guess it might be a good idea to insert a shortcut somewhere?

Reid Barton (Nov 14 2018 at 20:12):

looks like the actual solution is category punit := category_theory.punit_category

Reid Barton (Nov 14 2018 at 20:13):

can we use instance priority to guide the search here?

Reid Barton (Nov 14 2018 at 20:14):

the funny thing is that punitactually has a unique structure of all those classes it looks for

Johan Commelin (Nov 14 2018 at 20:15):

@Reid Barton I'm really confused, because a lot of the time it is finding that instance. But that sometimes it goes astray...

Reid Barton (Nov 14 2018 at 20:15):

Well, it did find it here, eventually

Reid Barton (Nov 14 2018 at 20:16):

Everything looks more or less fine until the max depth error

Johan Commelin (Nov 14 2018 at 20:18):

Hmmm, would it be good strategy if Lean is searching for an instance of foo bar to first check if maybe bar.foo exists?

Johan Commelin (Nov 14 2018 at 20:18):

Because that would find punit.category instantly...

Johan Commelin (Nov 14 2018 at 20:24):

Ahrg, this is so annoying. So now I can start writing lots of @ signs, and insert the typeclass instances manually, and the code becomes unreadable...

Kenny Lau (Nov 14 2018 at 20:27):

I really doubt how this will scale

Kenny Lau (Nov 14 2018 at 20:27):

as we get more things into mathlib

Mario Carneiro (Nov 14 2018 at 20:29):

I think category_theory.small_category is misnamed...

Reid Barton (Nov 14 2018 at 20:32):

Either :four_leaf_clover: will have to improve the instance search algorithm, or we will have to start being more careful about how we write instances, with other tradeoffs

Johan Commelin (Nov 14 2018 at 20:33):

@Mario Carneiro Can you elaborate?

Johan Commelin (Nov 14 2018 at 20:33):

I now have

obj := Ī» U, @limit _ (@category_theory.opposite _
(@category_theory.comma_category _ _ _ category_theory.punit_category _ _ _ _)) _ _
((comma.fst (full_subcategory_inclusion B) (functor.of_obj U)).op ā‹™ F) _,

and I get red squiggles under the ā‹™ at the end.

Johan Commelin (Nov 14 2018 at 20:34):

Errors:

failed to synthesize type class instance for
X : Type v,
_inst_1 : topological_space X,
B : set (opens X),
C : Type u,
š’ž : category C,
F : category_theory.presheaf ā†„B C,
U : opens Xįµ’įµ–
āŠ¢ category comma (full_subcategory_inclusion B) (functor.of_obj U)įµ’įµ–
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ā‡
inferred
  category_theory.opposite
sheaf.lean:414:66: error

failed to synthesize type class instance for
X : Type v,
_inst_1 : topological_space X,
B : set (opens X),
C : Type u,
š’ž : category C,
F : category_theory.presheaf ā†„B C,
U : opens Xįµ’įµ–
āŠ¢ category comma (full_subcategory_inclusion B) (functor.of_obj U)įµ’įµ–
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ā‡
inferred
  category_theory.opposite
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  š’ž
inferred
  ?m_1
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  š’ž
inferred
  ?m_1
Additional information:
/home/jmc/data/math/community-mathlib/category_theory/sheaf.lean:415:20: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    limits.limit.pre ?m_7 ?m_9
  has type
    limits.limit ?m_5 āŸ¶ limits.limit (?m_9 ā‹™ ?m_5) : Type ?
  but is expected to have type
    ā‡ Uā‚ āŸ¶ ā‡ Uā‚‚ : Type v
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  š’ž
inferred
  ?m_1
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  š’ž
inferred
  ?m_1
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  š’ž
inferred
  ?m_1

Reid Barton (Nov 14 2018 at 20:34):

instance [preorder Ī±] : small_category Ī± := ... got the name category_theory.small_category

Johan Commelin (Nov 14 2018 at 20:35):

Aaah, that's not so nice. That should be in the preorder namespace.

Kenny Lau (Nov 14 2018 at 20:35):

@Mario Carneiro talk about is_ring_hom.is_ring_hom

Mario Carneiro (Nov 14 2018 at 20:36):

what is that even?

Kenny Lau (Nov 14 2018 at 20:37):

https://github.com/leanprover/mathlib/blob/master/ring_theory/subring.lean#L28

Kenny Lau (Nov 14 2018 at 20:37):

namespace is_ring_hom

instance {S : set R} [is_subring S] : is_ring_hom (@subtype.val R S) :=
by refine {..} ; intros ; refl

end is_ring_hom

Kenny Lau (Nov 14 2018 at 20:37):

guess how this would be called

Kenny Lau (Nov 14 2018 at 20:38):

also what on earth is it with the local attribute [instance] classical.prop_decidable

Reid Barton (Nov 14 2018 at 20:38):

There's also some bug where Lean's normal naming strategy for an instance is not used under certain circumstances (I'm not sure exactly which)

Mario Carneiro (Nov 14 2018 at 20:39):

classical.prop_decidable existed long before classical.dec, I think it's in the style guide and TPIL

Kenny Lau (Nov 14 2018 at 20:39):

I mean, who on earth put it there

Kenny Lau (Nov 14 2018 at 20:39):

you don't need any classical stuff for subrings

Reid Barton (Nov 14 2018 at 20:39):

We could have a strategy where we don't write instances like instance [preorder Ī±] : small_category Ī±, but rather instance [preorder Ī±] : small_category (preorder Ī±), where def preorder Ī± := Ī±

Mario Carneiro (Nov 14 2018 at 20:40):

maybe it was needed once, or a mathematician wrote the file

Mario Carneiro (Nov 14 2018 at 20:40):

Authors: Johan Commelin

Kenny Lau (Nov 14 2018 at 20:41):

but curiously he was never part of the file's history

Reid Barton (Nov 14 2018 at 20:41):

That would cut out all the silly search starting preorder punit (actually it is not really silly, since punit could very well be a preorder, but anyways we want a different instance)

Mario Carneiro (Nov 14 2018 at 20:42):

I think we need to think about a more principled approach to instance priorities

Mario Carneiro (Nov 14 2018 at 20:44):

for preorder categories, I guess it depends on whether you view it as "a preorder is a special kind of category" or "any preorder can be equipped with a canonical category structure"

Kenny Lau (Nov 14 2018 at 20:44):

I think we need to refactor the typeclass search system

Kenny Lau (Nov 14 2018 at 20:44):

but I don't know how any of those things work

Kenny Lau (Nov 14 2018 at 20:45):

so I might have said nothing in the first place

Reid Barton (Nov 14 2018 at 20:45):

Well I'm not necessarily thinking about anything as anything, I just want to avoid these 20 pages of failed instance searches whenever I try to look for a category instance which is after the preorder one.

Mario Carneiro (Nov 14 2018 at 20:45):

:four_leaf_clover:

Kenny Lau (Nov 14 2018 at 20:45):

I think the instance search is as stupid as simp

Mario Carneiro (Nov 14 2018 at 20:45):

it's much worse than simp

Kenny Lau (Nov 14 2018 at 20:45):

and we still haven't fixed the problem with simp

Kenny Lau (Nov 14 2018 at 20:45):

for the love of god

Kenny Lau (Nov 14 2018 at 20:46):

who thought depth first search is a good idea (instance) and who thought breadth first search is a good idea (simp)

Kenny Lau (Nov 14 2018 at 20:46):

but I don't study CS

Mario Carneiro (Nov 14 2018 at 20:47):

But it's not a tactic, it's built into lean, so there is very little customization or alternatives we can try in lean 3

Mario Carneiro (Nov 14 2018 at 20:47):

at least not without forking lean

Reid Barton (Nov 14 2018 at 20:48):

OK here is a thought. What if we by convention give each instance which doesn't match against the head a lower priority

Reid Barton (Nov 14 2018 at 20:48):

i.e. each instance of the form \Pi a, ... : C a

Reid Barton (Nov 14 2018 at 20:49):

Because of course we want to match against things like ... : C (T a) first, if we're trying to find an instance C (T ...)

Kenny Lau (Nov 14 2018 at 20:49):

@Mario Carneiro but from your CS experience, what is the best search method?

Mario Carneiro (Nov 14 2018 at 20:49):

There are two essentially different kinds of instances: "parent coercions" that change the head, and things that change the type to something smaller and leave the head alone

Mario Carneiro (Nov 14 2018 at 20:50):

we know the search terminates in the second case because it's well founded on the structure construction, and in the first case because our tree of classes is finite

Johan Commelin (Nov 14 2018 at 20:50):

git grep "^instance" | wc -l
1515

Mario Carneiro (Nov 14 2018 at 20:50):

that last one is obviously problematic

Mario Carneiro (Nov 14 2018 at 20:50):

because it gets worse as you add more things anywhere in mathlib

Kenny Lau (Nov 14 2018 at 20:51):

I think TREE(3) is also finite so I don't really get your point

Kenny Lau (Nov 14 2018 at 20:51):

are we satisfied with "it will eventually terminate"?

Mario Carneiro (Nov 14 2018 at 20:52):

it's an important first step

Mario Carneiro (Nov 14 2018 at 20:52):

the next question is "how finite" of course

Mario Carneiro (Nov 14 2018 at 20:52):

and this depends on how much typeclass caching lean does

Mario Carneiro (Nov 14 2018 at 20:52):

so I'm not sure on the details

Mario Carneiro (Nov 14 2018 at 20:53):

We want it to be mostly linear

Johan Commelin (Nov 14 2018 at 20:53):

How about prioritizing type 1? Like Reid suggested?

Mario Carneiro (Nov 14 2018 at 20:54):

Parent coercions have a fixed priority, I don't think we can change it

Mario Carneiro (Nov 14 2018 at 20:54):

This is one place where I think lean is using the wrong search strategy btw

Reid Barton (Nov 14 2018 at 20:55):

Oh I forgot about parent coercions.

Kenny Lau (Nov 14 2018 at 20:55):

we don't we ask the big guys about the typeclass system in lean 4?

Mario Carneiro (Nov 14 2018 at 20:56):

If we call type coercions type 1 and parent / "head changing" coercions type 2, then I think we should use backward chaining for type 1 and forward chaining for type 2

Mario Carneiro (Nov 14 2018 at 20:57):

For example, if you prove that ordered_field real then lean will pre-calculate proofs of preorder real and a bunch of other stuff

Reid Barton (Nov 14 2018 at 20:57):

Are we talking about actual parent coercions like from group to monoid?

Mario Carneiro (Nov 14 2018 at 20:57):

yes

Reid Barton (Nov 14 2018 at 20:57):

So then there are also things like preorder to category

Mario Carneiro (Nov 14 2018 at 20:57):

yes

Reid Barton (Nov 14 2018 at 20:58):

And I guess both of those fall under type 2

Mario Carneiro (Nov 14 2018 at 20:58):

and if you have ordered_field A in the context then it calculates preorder A when solving typeclass problems

Kenny Lau (Nov 14 2018 at 20:58):

@Mario Carneiro how does this work in metamath?

Mario Carneiro (Nov 14 2018 at 21:00):

You get to do this stuff yourself, but there is a smallish spine so it's at most two or three theorem applications to get from anything to anything else

Mario Carneiro (Nov 14 2018 at 21:00):

the backward chaining stuff might be done automatically in later versions?

Mario Carneiro (Nov 14 2018 at 21:01):

It's all third party stuff though

Johan Commelin (Nov 14 2018 at 21:01):

So is there any hope we can improve the system in Lean 3?

Mario Carneiro (Nov 14 2018 at 21:01):

this is emphatically not part of "metamath core"

Mario Carneiro (Nov 14 2018 at 21:01):

priorities seem like the best option, but we need a good rule

Mario Carneiro (Nov 14 2018 at 21:02):

I have hope for reid's proposal

Reid Barton (Nov 14 2018 at 21:03):

The obvious, but more annoying variant is to raise the priority of every "type 1" instance

Johan Commelin (Nov 14 2018 at 21:04):

I think Mario said that those were fixed... but maybe I misunderstood which type he referred to...

Reid Barton (Nov 14 2018 at 21:04):

I'm also a little confused about Mario's description of the two types

Reid Barton (Nov 14 2018 at 21:04):

In Haskell, if we have an instance C (T a b), we call T the instance head

Reid Barton (Nov 14 2018 at 21:05):

C is the class

Reid Barton (Nov 14 2018 at 21:05):

I'm not sure whether Mario is using the same terminology, or switched the classes or what

Mario Carneiro (Nov 14 2018 at 21:05):

I called C the head there

Mario Carneiro (Nov 14 2018 at 21:06):

so parent coercions change the head, i.e. C a => D a

Mario Carneiro (Nov 14 2018 at 21:06):

and type coercions are like C a , C b => C (T a b)

Reid Barton (Nov 14 2018 at 21:08):

I might be wrong in assuming instances like C a, C b => C (T a b) are more common in mathlib--in standard Haskell they're the only kind of instances you are allowed to write

Reid Barton (Nov 14 2018 at 21:08):

(instance C a => D a is illegal)

Mario Carneiro (Nov 14 2018 at 21:08):

That's not true, I think you can do parent coercions in Haskell too

Reid Barton (Nov 14 2018 at 21:09):

With GHC extensions

Reid Barton (Nov 14 2018 at 21:09):

But the effect is probably like 99% of all instances are of the C (T a b) form

Mario Carneiro (Nov 14 2018 at 21:12):

oh, I see, there are parent coercions but no user defined parent coercions

Mario Carneiro (Nov 14 2018 at 21:12):

class Test a where
  test :: a -> a
class Test a => Test2 a where
  test2 :: a -> a

Mario Carneiro (Nov 14 2018 at 21:12):

this is okay

Reid Barton (Nov 14 2018 at 21:12):

There isn't even a coercion in the same sense as in Lean

Reid Barton (Nov 14 2018 at 21:13):

There, to write a Test2 instance, you must first write a Test instance

Reid Barton (Nov 14 2018 at 21:13):

The purpose of Test a => Test2 a is instead to avoid writing contexts like (Test a, Test2 a) => t

Mario Carneiro (Nov 14 2018 at 21:13):

that's the same as in lean

Reid Barton (Nov 14 2018 at 21:14):

Oh, well... I guess Lean hides the need to write the Test instance separately

Mario Carneiro (Nov 14 2018 at 21:14):

class Test (a : Type) := (test : a ā†’ a)
class Test2 (a : Type) extends Test a := (test2 : a ā†’ a)

instance : Test nat := {test := id}
instance : Test2 nat := {test2 := id} --requires the first instance

Reid Barton (Nov 14 2018 at 21:15):

But you can also write instance : Test2 nat := {test := id, test2 := id} without the first instance, which has no equivalent in Haskell

Mario Carneiro (Nov 14 2018 at 21:16):

Maybe lean should do that too

Mario Carneiro (Nov 14 2018 at 21:16):

that is essentially requiring the user to do the forward chaining thing I said

Reid Barton (Nov 14 2018 at 21:16):

I actually don't know off-hand how GHC solves a Test a constraint if you only have Test2 in the context

Reid Barton (Nov 14 2018 at 21:17):

I wouldn't be surprised if it does forward chaining in that situation

Mario Carneiro (Nov 14 2018 at 21:18):

you mean when you have test :: Test2 a => a -> a?

Reid Barton (Nov 14 2018 at 21:18):

Basically, yeah.

Mario Carneiro (Nov 14 2018 at 21:24):

I think it is complete in Haskell's case to always saturate downwards (derive all superclasses of all the things in the context) and then backward chain from uses (without using any parent coercions)

Johan Commelin (Nov 15 2018 at 09:48):

Aahrg, Lean is just becoming completely unresponsive when I try to fill in the instances by hand.

Johan Commelin (Nov 15 2018 at 09:49):

Look at the code that I have now: this is getting pretty crazy...

def extend : presheaf X C :=
{ obj := Ī» U, @limit.{u v} _ (@category_theory.opposite.{v v} _
(@category_theory.comma_category.{v v v v v v}
  _ (category_theory.full_subcategory.{v v} _)
  _ category_theory.punit_category.{v}
  _ (@site.to_category.{v} (@opens.{v} X _inst_1) (@category_theory.site.{v} X _inst_1)) _ _))
  _ _
((comma.fst (full_subcategory_inclusion B) (functor.of_obj U)).op ā‹™ F)
(limits.has_limit_of_has_limits_of_shape.{u v} _),
  map := _ }

Kenny Lau (Nov 15 2018 at 09:54):

welcome to the club :P

Johan Commelin (Nov 15 2018 at 10:03):

Ok, I need to confess. I'm making a big fool out of myself. There was actually a missing assumption... so no wonder Lean couldn't find the instance. The code is now back to

def extend : presheaf X C :=
{ obj := Ī» U, limit ((comma.fst (full_subcategory_inclusion B) (functor.of_obj U)).op ā‹™ F),
  map := _ }

However it is still taking >10s to typecheck this stuff. Before I removed all the explicit instances, it also took >10s.

Leonardo de Moura (Nov 16 2018 at 05:23):

@Johan Commelin

Johan Commelin: So is there any hope we can improve the system in Lean 3?

To improve Lean 3, you need to fork it, and improve it yourself. The development is frozen in the main repo, and all efforts are focused on Lean 4. That being said, nobody should expect Lean 4 will solve all problems and everybody will be happy.

Leonardo de Moura (Nov 16 2018 at 05:25):

@Kenny Lau

Kenny Lau: we don't we ask the big guys about the typeclass system in lean 4?

We didn't get there yet. We have only random ideas on how to improve the typeclass system in lean 4.

Leonardo de Moura (Nov 16 2018 at 05:27):

@Kenny Lau

Kenny Lau: I think we need to refactor the typeclass search system

If you want a better typeclass system in the next few months, you should fork the current system, and refactor the typeclass search system yourself.

Johan Commelin (Nov 16 2018 at 05:33):

@Leonardo de Moura Ok, I was hoping that maybe we could use priorities to guide the type class system. Anyway, thanks for the input! And thanks for all you're doing for Lean (3 and 4).

Leonardo de Moura (Nov 16 2018 at 05:36):

@Johan Commelin Yes, priorities will help. Shortcuts will help too. Example: https://github.com/leanprover/lean/blob/master/library/init/data/int/basic.lean#L418-L429

Leonardo de Moura (Nov 16 2018 at 05:37):

These are just workarounds.

Mario Carneiro (Nov 16 2018 at 07:07):

It's not clear to me how much shortcuts actually help, though, because they make the typeclass graph even larger

Mario Carneiro (Nov 16 2018 at 07:08):

if you have instances from A -> B -> C and add a shortcut A -> C, then a typeclass search for some unrelated F will traverse both paths to C (and possibly the entire subtree rooted at C)

Mario Carneiro (Nov 16 2018 at 07:09):

Are there any plans for lean 4 to do anything with the typeclass system?

Leonardo de Moura (Nov 16 2018 at 07:20):

You can add the shortcuts using local attributes. In this way, you can add shortcuts to a file without affecting other files.

Leonardo de Moura (Nov 16 2018 at 07:21):

Sebastian and I discussed a few improvements (e.g., better indexing and caching), but as I said above these are just ideas on the whiteboard. We didnā€™t get there yet.


Last updated: Aug 03 2023 at 10:10 UTC