Guidance: typeclasses vs. hypothesis

Stream: mathlib4

[Robert Maxton]

What heuristics should I use to decide whether a condition on a given object would best be implemented as a typeclass, versus by explicitly taking an additional argument?

One obvious point is that instances are supposed to be canonical, so in particular if the typeclass lives most naturally in Prop it seems like it would be a natural choice for being a typeclass, as that means that instance synthesis can efficiently and convenient provide the relevant conditions under various common use cases. Except that there are lots of cases in Mathlib where this heuristic doesn't apply, which makes me think I'm missing something.

[Yaël Dillies]

It also depends whether the instances would be at all specific. Eg [Continuous f] [Continuous g] : Continuous (f ∘ g) would be a terrible since literally every function h is syntactically of the form f ∘ g (docs#Function.comp is reducible)

[Yaël Dillies]

... and whether you expect the arguments to be annoying/impossible to provide by hand. Eg if you want your hypothesis to be used by an instance, it must itself be a typeclass

[Robert Maxton]

Hmmm... So my specific case is that I'm defining the extra structure needed for a semiring ideal to make nice quotients, and one of the things I'd like to do is to make the noise go away when it's unnecessary. In particular, if the semiring is in fact a ring then all ideals are subtractive, and if the ideal is the kernel of a hom then it's also subtractive.

Both of these seem like things that instance synthesis should be able to handle without horrible performance penalties, I think?

[Yaël Dillies]

Yes, but will you expect structural instances to exist? eg instances of the form[IsSubtractive I] [IsSubtractive J] : IsSubtractive (I + J)

[Yaël Dillies]

There is also the concern that someone might want to rewrite their subtractive ideal to a different form where it's not structurally obvious anymore that it is subtractive

[Robert Maxton]

... You could, certainly, there are a bunch of theorems about subtractive ideals being preserved under various transformations/homomorphisms...?

[Robert Maxton]

Yaël Dillies said:

There is also the concern that someone might want to rewrite their subtractive ideal to a different form where it's not structurally obvious anymore that it is subtractive

Yes, but I feel like that's best handled by giving the instance an explicit name so that you can use ... (inst := ⟨h⟩) conveniently

[Robert Maxton]

at least, that seems like the best of both worlds to me

[Robert Maxton]

Another case that's coming up is the definition of a maximal/partitioning ring hom, which is a condition that does carry data, but one can prove that any two ways of filling out the data fields produce isomorphic quotients, so it's "morally" the same case as Prop. Though it still has the potential for diamond issues... Actually, in some ways I think that's a stronger argument for it being a typeclass, as otherwise providing all that bundled data would be really annoying.

[Robert Maxton]

Yaël Dillies said:

It also depends whether the instances would be at all specific. Eg [Continuous f] [Continuous g] : Continuous (f ∘ g) would be a terrible since literally every function h is syntactically of the form f ∘ g (docs#Function.comp is reducible)

This makes me kind of want a gadget inParam, that makes instance synthesis behave like aesop safe destruct ^.^;

[Robert Maxton]

don't think the instance synth mechanism allows for that tho

[Yaël Dillies]

Either case, you should try! It's always possible to refactor from/to a typeclass later

[Robert Maxton]

Fair enough!