Multiple overlapping typeclasses

Stream: general

[David Loeffler]

How should one deal with lemmas where the "natural" generality involves several typeclass assumptions which contain conflicting data?

For instance, suppose I have a lemma which requires a type X with a norm, an additive group structure, and a distinguished element "1". The typeclass [NormedAddGroup X] gives a norm and add-group structure satisfying sensible compatibilities, while [AddGroupWithOne X] gives an add-group structure and a 1.

However, if you use both at once,

{X : Type*} [NormedAddGroup X] [AddGroupWithOne X]

you don't get the right thing: you get a type with two possibly different add-group structures, one of which one has the norm and the other has the 1.

How do I force the NormedAddGroup structure and the AddGroupWithOne structure to have the same underlying AddGroup structure?

[Yaël Dillies]

You make a new NormedAddCommGroupWithOne typeclass extending NormedAddCommGroup and AddCommGroupWithOne

[Yaël Dillies]

But doesn't NormedRing fit your purposes?

[David Loeffler]

NormedRing has far more structure; it calls for the existence of multiplication on X (and for the norm to be submultiplicative), both of which are irrelevant in the case at hand. Probably it's true that there are no interesting examples of NormedAddCommGroupWithOnes that are not NormedRings, but this was only intended as an example of a more general problem.

[David Loeffler]

You make a new NormedAddCommGroupWithOne typeclass extending NormedAddCommGroup and AddCommGroupWithOne

I'm wary of creating a special-purpose typeclass just for one or two lemmas...

[Yaël Dillies]

:shrug: That's how typeclasses work. The other option is to have more mixins, eg make NormedAddCommGroup α take in an [AddCommGroup α] parameter, rather than implying it

[David Loeffler]

So how would this work in practice?

class NormedAddMonoidWithOne (R : Type*)
  extends NormedAddGroup R, AddMonoidWithOne R

example (R : Type) [NormedRing R] : NormedAddCommMonoidWithOne R := by infer_instance -- fails

[Yaël Dillies]

class NormedAddMonoidWithOne (R : Type*)
  extends NormedAddGroup R, AddMonoidWithOne R

instance (R : Type) [NormedRing R] : NormedAddCommMonoidWithOne R where
  __ := ‹NormedRing R›

?

[David Loeffler]

Are you saying I would need to add an explicit instance of NormedAddMonoidWithOne for every single pre-existing typeclass that extends both NormedAddGroup and AddMonoidWithOne? Then adding the new typeclass doesn't really achieve much. Is there not some way of automating this?

[Yaël Dillies]

David Loeffler said:

Are you saying I would need to add an explicit instance of NormedAddMonoidWithOne for every single pre-existing typeclass that extends both NormedAddGroup and AddMonoidWithOne?

No, only for the direct common children. Eg you don't need to add NormedField α → NormedAddMonoidWithOne α because typeclass search already knows NormedField α → NormedRing α.

[Yaël Dillies]

That should be very few typeclasses. In fact, I can't think of another one besides NormedRing!

[David Loeffler]

That should be very few typeclasses. In fact, I can't think of another one besides NormedRing!

That's very probably true for this example, but I think the question makes sense more generally.

<rant> To pick up on another point you made (about mixins): I found this one of the most opaque aspects of mathlib when I was first getting used to it: some typeclasses must be used together, while others must not be used together else you get craziness, and there seems to be absolutely no convention as to which; e.g. [NormedSpace ℝ V] requires a pre-existing NormedAddCommGroup structure, but you are in for a world of pain if you use it on a type that already has a [Module ℝ V] structure.</rant>

[Kim Morrison]

We all feel your pain, @David Loeffler. This design question is a difficult one, and far from completely settled. The trend has generally been towards converting things to mixins, but obviously it's a lot of work.

[Eric Wieser]

I tried to split NormedGroup from AddCommGroup long ago, but:

• As Kim says It's a lot of tedious work
• Inevitably proofs break for performance reasons; while unbundling might be faster in principle [citation needed], it won't be faster in the places that optimized the proof for the bundled spelling.
• it makes analysts sad because they now have to write

  lean variable [AddCommGroup V] [NormedAddCommGroup V] [Module K V] [NormedSpace K V]

  instead of what we have now

  lean variable [NormedAddCommGroup V] [NormedSpace K V]

[Johan Commelin]

I think we need a good way to handle your "it makes analysts sad". Because only then can we realistically try this out in practice.
variable? is a good start, but not enough, I think.

[Jireh Loreaux]

@Eric Wieser do we have examples where class abbrev really hurts performance? I ask because, while I thought it might be truly detrimental, it didn't seem to be much/any worse when I tried it in #16975 compared to just adding the relevant instance.

If it didn't significantly impact performance (which would still surprise me), the solution to "it makes analysts sad" would just be to class abbrev the important structures.

[David Loeffler]

Thanks for the comments folks! I am sure that a great deal of thought and energy has gone into trying to find a solution that keeps the pain to a minimum.

I'd be interested in your thoughts on the following particular issue. Suppose you have a series of definitions / theorems all applying in some given setting, described by a list of section-level typeclass variables. (E.g. you have a ring R and an R-module M and a linear map from M to R, ...) Then for one such lemma you want to slightly strengthen the assumptions, maybe "if we are in the above situation but R happens to be a normed ring, then...". If the stronger assumption is implemented as an extension class, rather than a mixin, the only option seems to be to throw away the existing section variables and rebuild the whole edifice of assumptions from scratch.

Is there any hope whatsoever of setting up some syntax to handle this situation? Something like

variable [NormedRing R] instead of [Ring R] in
lemma foo : ...

and having it re-build the existing typeclass assumptions with the more specific typeclass?

[Eric Wieser]

I think you can do that with omit [Ring R] in variable [NormedRing R] in, but you still have to rebuild everything on M

[David Loeffler]

Eric Wieser said:

I think you can do that with omit [Ring R] in variable [NormedRing R] in, but you still have to rebuild everything on M

I'm not sure that works. If I understand correctly, omit only reverses the effect of include, setting a variable back to "include if relevant" rather than "include always". But it doesn't explicitly forbid a typeclass variable from being included, so you can still end up in the dreaded situation of accidentally having two unrelated ring structures on the same type simultaneously.

[David Loeffler]

It took me a while to cook up an example, but here's one:

variable (R : Type*) [AddCommGroup R]

/- lemmas lemmas lemmas... -/

omit [AddCommGroup R] in
variable [NormedAddCommGroup R] in

example (a b : R) : ‖a + b‖ ≤ ‖a‖ + ‖b‖ := by
/- tactic state is now:
R : Type u_1
inst✝¹ : AddCommGroup R
inst✝ : NormedAddCommGroup R
a b : R -/
exact norm_add_le a b -- fails, wrong "+"!

Here the call to "norm_add_le" fails because Lean interprets the "+" in the theorem statement as the one from the AddCommGroup instance, while "norm_add_le a b" is a proof of the triangle ineq for the entirely unrelated "+" coming from the NormedAddCommGroup instance.

[Eric Wieser]

I don't understand that example, where did AddGroup come from?

[Eric Wieser]

(assuming it's a typo, I think I agree with your diagnosis)

[David Loeffler]

Sorry, that was a typo; I realised commutativity was irrelevant to my example but introduced an inconsistency in removing it. Edited.

[Johan Commelin]

Hmmm, thanks for that MWE. @Sebastian Ullrich is this intended behaviour or a bug?

[Johan Commelin]

Personally, I always thought omit meant "forbid".

[Sebastian Ullrich]

That sounds like a reasonable expectation, feel free to file an issue

[David Loeffler]

Sebastian Ullrich said:

That sounds like a reasonable expectation, feel free to file an issue

OK this is now lean#5595.

[Damiano Testa]

I like this, since it is going to automatically make include be "very" scoped, since there is no way to revert an include to "possibly include"!

[David Loeffler]

@Damiano Testa makes the fair point that this change would leave us with no way of precisely reverting the effect of an include. Some might find that desirable, but others might not. So maybe, rather than changing the behaviour of omit, we could retain the current behaviour of omit and have another keyword -- omit! or forget perhaps -- for entirely removing a variable from the context.

[Riccardo Brasca]

Having both versions seems very reasonable.

[Damiano Testa]

How about end h for moving h out of the scope? I find that lots of different ways of managing variables cause more problems than they solve.

[Damiano Testa]

So you can end a namespace or section, removing all variables in scope, or you can selectively remove a single (or list?) of variables with it as well.

[Ruben Van de Velde]

Wasn't omit supposed to be a temporary solution while we moved to sections?

[Damiano Testa]

Well, I think that the original suggested change would accelerate the process...

[Jireh Loreaux]

I really don't think we should have two versions of omit. It sounds like a recipe for pain and confusion. If variable issues are really getting to you, then it probably means you need more sections.

[David Loeffler]

If variableissues are really getting to you, then it probably means you need more sections.

Using sections does not solve the general problem (although it probably does solve as much of it as the omit! command would, which is not a perfect solution either). The section-based idiom would be something like

section Ring

variable {R M : Type*} [Ring R] [IsArtinian R] [Module R M] [NoZeroSMulDivisors R M] [etc etc etc...]

[...]

end Ring

section CommRing

variable {R M : Type*} [CommRing R] [IsArtinian R] [Module R M] [NoZeroSMulDivisors R M] [etc etc etc...]

...

and we have to re-declare the entire pile of instance variables at the start of the new section, because it's "not the same R" any more, even though CommRing extends Ring so the new situation is a special case of the old one.

[Eric Wieser]

One argument against sections is that it's harder to review diffs, as lemmas which haven't actually changed can appear as deleted and recreated in the diff. If you can leave them in the same place, then this issue goes away

[Eric Wieser]

(but this could be solved with something like leaff)

[Jireh Loreaux]

Eric Wieser said:

One argument against sections is ...

One argument in favor of sections is that lemmas with similar assumptions get grouped together, which I think is more important (and has more lasting impact), than the diff on GitHub. So, I don't buy your argument.

[Jireh Loreaux]

David Loeffler said:

we have to re-declare the entire pile of instance variables at the start of the new section

I agree, this can be annoying. Repeated cases of this may mean we want to refactor Mathlib (e.g., in this case Comm could become a mixin, although I don't actually think that's a good idea).

[David Loeffler]

What I'm hoping for here is precisely some sort of syntax that would allow us to treat an extension class like a mix-in, without actually refactoring it as such – e.g. temporarily "upgrading" a [Ring R] to a [CommRing R] or a [NormedRing R] or whatever, etc, while keeping the rest of the previously-declared instances in force.

[Damiano Testa]

I have often wanted a model where the fields of a class are automatically classes themselves and you can lump them together or take them apart at will...

[Alex Meiburg]

I could imagine a future where minimal data-carrying classes are the only things that aren't mixins. So e.g. you start with things like a Norm G, Preorder G, Topological Space G, Add G, Zero G... then NormedAddGroup G takes mixin arguments for Add/Neg/Sub/Zero/Norm. Then if you _also_ had an AddCommGroup or GroupWithOne in the context, they would share all their data fields so there wouldn't be unification failures.

Of course no one wants to start each file talking about rings with variable [Add G] [Sub G] [Mul G] [Zero G] [One G] [SMul Nat G] [SMul Int G] [Pow G Nat], so we could have a few classes that just bundle together commonly coexisting data. Like I could picture a GroupData G extends Mul G, One G, Inv G, Div G, Pow G Nat, Pow G Int, and then Group/CommGroup/Semiring/NormedGroup would all take a GroupData mixin.

But now you would only have to create an appropriate collection of ___Data classes to cover all your bases, as opposed to one for each combination of properties too, which is definitely a huge shrinkage

[Yury G. Kudryashov]

Does it make the exponential blow-up better or worse? If you have a complicated type (e.g., continuous linear maps taking values in the spaces of continuous multilinear maps, add 1 or 2 more layers), then sometimes lean falls to generate an instance (e.g., Norm), because the expression is too large.

[Yury G. Kudryashov]

These types naturally appear when you try to define, e.g., composition of bundled (multi)linear maps add a bundled map.

[Alex Meiburg]

I admit I don't know anything about that. It feels like it would be easier to manage the problem here (when you have overlapping typeclasses, the need to essentially create a bespoke new class), easier in the sense of the codebase - but I have no idea what the impact on runtime would look like