Zulip Chat Archive

Stream: general

Topic: type class issues


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 14 2018 at 20:12):

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

view this post on Zulip Reid Barton (Nov 14 2018 at 20:13):

can we use instance priority to guide the search here?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Reid Barton (Nov 14 2018 at 20:15):

Well, it did find it here, eventually

view this post on Zulip Reid Barton (Nov 14 2018 at 20:16):

Everything looks more or less fine until the max depth error

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Nov 14 2018 at 20:18):

Because that would find punit.category instantly...

view this post on Zulip 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...

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:27):

I really doubt how this will scale

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:27):

as we get more things into mathlib

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:29):

I think category_theory.small_category is misnamed...

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 14 2018 at 20:33):

@Mario Carneiro Can you elaborate?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 14 2018 at 20:34):

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

view this post on Zulip Johan Commelin (Nov 14 2018 at 20:35):

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

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:35):

@Mario Carneiro talk about is_ring_hom.is_ring_hom

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:36):

what is that even?

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:37):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:37):

guess how this would be called

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:38):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:39):

I mean, who on earth put it there

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:39):

you don't need any classical stuff for subrings

view this post on Zulip 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 Ī± := Ī±

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:40):

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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:40):

Authors: Johan Commelin

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:41):

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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:42):

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

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:44):

I think we need to refactor the typeclass search system

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:44):

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

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:45):

so I might have said nothing in the first place

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:45):

:four_leaf_clover:

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:45):

I think the instance search is as stupid as simp

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:45):

it's much worse than simp

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:45):

and we still haven't fixed the problem with simp

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:45):

for the love of god

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:46):

but I don't study CS

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:47):

at least not without forking lean

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 14 2018 at 20:48):

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

view this post on Zulip 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 ...)

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:49):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 14 2018 at 20:50):

git grep "^instance" | wc -l
1515

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:50):

that last one is obviously problematic

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:50):

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

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:51):

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

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:51):

are we satisfied with "it will eventually terminate"?

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:52):

it's an important first step

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:52):

the next question is "how finite" of course

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:52):

and this depends on how much typeclass caching lean does

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:52):

so I'm not sure on the details

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:53):

We want it to be mostly linear

view this post on Zulip Johan Commelin (Nov 14 2018 at 20:53):

How about prioritizing type 1? Like Reid suggested?

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:54):

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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:54):

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

view this post on Zulip Reid Barton (Nov 14 2018 at 20:55):

Oh I forgot about parent coercions.

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:55):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 14 2018 at 20:57):

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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:57):

yes

view this post on Zulip Reid Barton (Nov 14 2018 at 20:57):

So then there are also things like preorder to category

view this post on Zulip Mario Carneiro (Nov 14 2018 at 20:57):

yes

view this post on Zulip Reid Barton (Nov 14 2018 at 20:58):

And I guess both of those fall under type 2

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 14 2018 at 20:58):

@Mario Carneiro how does this work in metamath?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:00):

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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:01):

It's all third party stuff though

view this post on Zulip Johan Commelin (Nov 14 2018 at 21:01):

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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:01):

this is emphatically not part of "metamath core"

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:01):

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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:02):

I have hope for reid's proposal

view this post on Zulip Reid Barton (Nov 14 2018 at 21:03):

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

view this post on Zulip 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...

view this post on Zulip Reid Barton (Nov 14 2018 at 21:04):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 14 2018 at 21:05):

C is the class

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:05):

I called C the head there

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:06):

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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:06):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 14 2018 at 21:08):

(instance C a => D a is illegal)

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:08):

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

view this post on Zulip Reid Barton (Nov 14 2018 at 21:09):

With GHC extensions

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:12):

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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:12):

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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:12):

this is okay

view this post on Zulip Reid Barton (Nov 14 2018 at 21:12):

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

view this post on Zulip Reid Barton (Nov 14 2018 at 21:13):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:13):

that's the same as in lean

view this post on Zulip Reid Barton (Nov 14 2018 at 21:14):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:16):

Maybe lean should do that too

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:16):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 14 2018 at 21:17):

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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 21:18):

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

view this post on Zulip Reid Barton (Nov 14 2018 at 21:18):

Basically, yeah.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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 := _ }

view this post on Zulip Kenny Lau (Nov 15 2018 at 09:54):

welcome to the club :P

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Leonardo de Moura (Nov 16 2018 at 05:37):

These are just workarounds.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Nov 16 2018 at 07:09):

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

view this post on Zulip 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.

view this post on Zulip 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: May 11 2021 at 23:11 UTC