Zulip Chat Archive

Stream: new members

Topic: TC resolution


Andre Knispel (Aug 12 2020 at 07:50):

I'm trying to define and experiment with graded rings and I have a few issues with type classes. Here's my code:

import data.equiv.algebra
import data.polynomial
import algebra.module
import algebra.direct_sum

universes u v
variables (α : Type u) (M : Type v)
variables [add_monoid M] [decidable_eq M]

class graded_ring extends ring α :=
(pieces : M  Type u) (groups :  m : M, add_comm_group (pieces m))
(iso : α + direct_sum M pieces)
(of : Π m : M, pieces m  α := λ (m : M) (r : pieces m), iso.inv_fun (direct_sum.of pieces m r))
(mul_respects_grading :  (m m' : M) (r : pieces m) (r' : pieces m'),
   s : pieces (m + m'), of m r * of m' r' = of (m + m') s)

variables [comm_ring α] [r : ring α]

noncomputable instance : graded_ring (polynomial α)  :=
@graded_ring.mk (polynomial α)  _ _ (comm_ring.to_ring (polynomial α))
  (λ _ : , α) (λ _ : , @ring.to_add_comm_group α r) _ _ _

First, I don't understand why the ring instance of polynomial isn't found. If I make it implicit, the search tries increasingly complicated versions of dfinsupp.add_monoid before giving up. Is there a nicer way to do this, ideally so that I can use the record syntax? Second, is there a nicer way to write the commutative group instance of α?

Scott Morrison (Aug 12 2020 at 08:38):

There's a rule that you shouldn't use extend when adding more data to a class, if you need to have more parameters than the thing you're extending.

Scott Morrison (Aug 12 2020 at 08:38):

So I'd suggest you want to substantially reformulate this.

Kevin Buzzard (Aug 12 2020 at 08:42):

These rules are extremely hard to find unless you're a regular here.

Kevin Buzzard (Aug 12 2020 at 08:42):

You just get people like you, Reid or Mario saying "oh this is an antipattern" occasionally

Kevin Buzzard (Aug 12 2020 at 08:44):

What would be really nice would be a resource with some simple bad classes and perhaps not an explanation of why they're bad but at least a description of the rules of thumb to follow. I don't know these rules at all. I am still really bad at making definitions in Lean which is why I'm making so much fuss on another thread about exactly what the definition of yet another concept of finiteness / cardinality should be.

Scott Morrison (Aug 12 2020 at 08:45):

I think the problem is just that it introduces a "bad instance", because now whenever Lean wants to check if something is a ring, is has to check if it is a graded ring, and suddenly there's a metavariable for the type M introduced into the typeclass search problem.

Kevin Buzzard (Aug 12 2020 at 08:46):

Yeah I'm sure that if you actually understand the typeclass system (which I certainly don't) then it's all obvious. The problem is that if a mathematician beginner comes along they can write something which looks completely mathematically reasonable but is somehow impossible to use because of some issue regarding [foo X] v extends foo X

Kevin Buzzard (Aug 12 2020 at 08:46):

or some issue regarding universe parameters in the definition

Kevin Buzzard (Aug 12 2020 at 08:47):

or some issue regarding something having a different number of variables to something else

Kevin Buzzard (Aug 12 2020 at 08:48):

or some other issue -- these things are too numerous to mention. Classes are extremely well understood now, and the "gotchas" are all known to the experts, but whenever I want to make a new definition in Lean I run it past the Zulip chat before I do anything with it at all because I don't know all the pitfalls

Andre Knispel (Aug 12 2020 at 11:48):

Ah, now that I know what I'm looking for, I found the loop ring -> graded_ring -> monoid (for M) -> ... -> ring. I've looked at modules, because they should have the same issue, but the only thing I see is set_option default_priority 100. Does this make the priority for the classes there very low?

Scott Morrison (Aug 12 2020 at 11:51):

I don't think module is comparable, because it is not using extends like you are.

Scott Morrison (Aug 12 2020 at 11:51):

I would guess that you just want an additional typeclass, so you write [ring R] [graded_ring R] to summon one.

Scott Morrison (Aug 12 2020 at 11:52):

You might also look at src#category_theory.graded_object for the bundled version.

Andre Knispel (Aug 12 2020 at 12:04):

Thanks, that helped!

Jalex Stark (Aug 12 2020 at 22:36):

Kevin Buzzard said:

What would be really nice would be a resource with some simple bad classes and perhaps not an explanation of why they're bad but at least a description of the rules of thumb to follow. I don't know these rules at all. I am still really bad at making definitions in Lean which is why I'm making so much fuss on another thread about exactly what the definition of yet another concept of finiteness / cardinality should be.

I guess some of these rules have been implemented in code. Maybe the document you want starts out as docs for the linter?


Last updated: Dec 20 2023 at 11:08 UTC