mixin algebraic typeclasses

Stream: mathlib4

[Yury G. Kudryashov]

BTW, if we have this syntax, then we can try to migrate to "all classes with many fields are in Prop". E.g.,

class Mul α where
  mul : α → α → α

class Semigroup α [Mul α] where
  mul_assoc : ∀ x y z : α, (x * y) * z = x * (y * z)

variable [[Semigroup α]]

[Thomas Murrills]

Hmm, if we moved to classes like that being in Prop, would demonstrating equality between e.g. two semigroups get more complicated? We’d have to use heterogenous equality if the Mul instances weren’t defeq, right?

[Yaël Dillies]

When is equality between semigroups demonstrated? This never happens, except possibly in Eckmann-Hilton.

[Johan Commelin]

@Yury G. Kudryashov Yes, Reid has been convincing me that we should make that refactor (after the port).

[Johan Commelin]

It would probably speed up a lot of TC inferences and avoid a whole list of problems that we are currently seeing.

[Eric Wieser]

I remember being told that that design is particularly prone to exponential blowup, but maybe all paths lead to blowup anyway. It would certainly be a good thing to try

[Thomas Murrills]

Yaël Dillies said:

When is equality between semigroups demonstrated? This never happens, except possibly in Eckmann-Hilton.

Are you saying we only talk about equalities between class instances when their data fields are defeq, though? Because this would affect much more than semigroups

[Reid Barton]

Eric Wieser said:

I remember being told that that design is particularly prone to exponential blowup, but maybe all paths lead to blowup anyway. It would certainly be a good thing to try

The idea would be to have just two levels, data and properties. With a bunch of unrelated data classes, and using extends or equivalent for properties.

[Eric Wieser]

It's very rare to have non-defeq instances

[Yaël Dillies]

No, I'm saying that we don't talk about equality of typeclasses (except maybe docs#topological_space). This is (close to) evil. Instead, we talk about isomorphisms.

[Thomas Murrills]

Hmm, okay. I would have imagined there might be some issues where e.g. we have two non-defeq phrasings of a structure instance’s zero element, but now some rewrites of something which depends on that structure instance can’t be done, because the types have to change. But maybe we don’t want to ever do things like this, or maybe we have tools to handle it if we do…

[Johan Commelin]

In mathlib 3 we tried our very best to make sure that the data fields were always defeq. There are some known exceptions to this, but they typically cause trouble.

[Eric Wieser]

The only instances on the same type that I can think of which are not defeq are so because they're not equal at all

[Thomas Murrills]

I’m not actually worrying about having two declared instances which are equal but not defeq per se—I’m worried about needing to rewrite data within instances in the course of proving something about them, or in order to get something else working which depends on the instance but needs the data to be in a certain non-defeq form. But maybe I’m over-anticipating and this isn’t a real problem…or maybe this way of doing things would trivialize those problems somehow.

[Yury G. Kudryashov]

We have lemmas like docs#monoid.ext. Indeed, with this refactor it's not clear how to state them but they are very rarely used.

[Eric Wieser]

I think the statement would be that (m n : monoid_data M) [is_monoid m] [is_monoid n] (h : m.mul = n.mul) : m = n, if I understand @Reid Barton correctly

[Eric Wieser]

Probably with more @s

[Johan Commelin]

No, I think it would be

(m : monoid_data M) [h1 : is_monoid m] [h2 : is_monoid m] : h1 = h2

[Johan Commelin]

Note that in your example, m.one and n.one have no reason to be equal.

[Johan Commelin]

Or maybe that was somehow part of your h?

[Yury G. Kudryashov]

Yes, claiming equality of two proofs makes no sense.

[Johan Commelin]

Anyway, we should probably start thinking seriously about this refactor ~ 4 months from now.

[Yury G. Kudryashov]

Do you suggest that we have a MonoidData typeclass, not just Mul, One, Pow?

[Johan Commelin]

I would go with just Mul, One etc... But that will require better auto-implicit support.

[Yury G. Kudryashov]

Will this create the same problems with structure projections that we have now?

[Eric Wieser]

Johan Commelin said:

Note that in your example, m.one and n.one have no reason to be equal.

The whole point of docs#monoid.ext is to show that the ones are equal if the muls are

[Johan Commelin]

We can't do this refactor during the port, and we can't do the port without a good solution to lean4#2074... even though this refactor might make such a solution superfluous.

[Reid Barton]

Eric Wieser said:

The whole point of docs#monoid.ext is to show that the ones are equal if the muls are

If this is the point, then it can be stated in that form

[Eric Wieser]

Absolutely; but if monoid_data does exist, then it's probably handy to have that version too. If it doesn't, then monoid.ext isn't a reason to make monoid_data exist.

[Reid Barton]

If MonoidData does exist, it certainly shouldn't be a class... that is exactly how to get back to the current problems.

[Eric Wieser]

I think it avoids the current problem if MonoidData extends One, Mul instead of SemigroupData

[Eric Wieser]

Assuming the "current problem" is 2074

[Reid Barton]

The root issue is that there is more than one place to look to find out what a * b means

[Jireh Loreaux]

Doesn't this (i.e., MonoidData extending One, Mul) just amount to reverting to old structures? Or is the point that we generally have many more Prop fields than data fields, and we can lump all the Prop fields into a separate structure so we don't have to check them?

[Eric Wieser]

Yes, it's comparable to using old structures

[Reid Barton]

I don't recommend having MonoidData at all, and I don't understand why it came up

[Reid Barton]

Instead, Monoid is a mix-in indexed on One and Mul, and it's a proposition. As are the other 99999 classes you can put on top of One and Mul.

[Reid Barton]

You don't have to worry about diamonds here, because they are all propositions.

[Chris Hughes]

I guess another advantage is that it's usually going to be much quicker to find a Mul when you write x * y if there are no CommRing.toCommMonoid.toCommSemigroup.toSemigroup.toMul long paths to find and check equality of.

[Reid Barton]

Jireh Loreaux said:

Or is the point that we generally have many more Prop fields than data fields, and we can lump all the Prop fields into a separate structure so we don't have to check them?

More that we have many more Prop classes (e.g. CanionicallyLinearOrderedNonCommSemifield) than actual kinds of data.

[Eric Wieser]

My main fear with that design is seeing all the arguments to docs4#Function.Injective.ring every time we need a ring

[Reid Barton]

Right, it would need some language support and that's why it was never a real option in Lean 3.

[Reid Barton]

Er wait

[Sebastien Gouezel]

I would be really afraid of exponential blow-up if you don't bundle data. For instance, if you don't package zero, one, add, mul and neg into a RingData, then anything building on a ring would have these 5 dependencies. Which is really bad if you construct a ring depending on two rings and iterate this (say, taking a product of two rings, and then the ring of polynomials on this new ring, and then a quotient of this one).

[Eric Wieser]

[Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul ℕ β] [inst : SMul ℤ β] [Pow β ℕ] [NatCast β] [IntCast β] [Ring β]

[Reid Barton]

Oh, you mean the class arguments right?

[Reid Barton]

Yes.

[Reid Barton]

Not the axioms though.

[Sebastien Gouezel]

While having a RingData and a RingProp wouldn't lead to exponential blowup, while ensuring much shorter paths when checking that two multiplications coincide, say.

[Eric Wieser]

Even if we have magic to insert the 11 data typeclass arguments I have above, we also need to consider their presence in:

• The goal view
• The web docs
• Help tooltips

[Eric Wieser]

RingData + RingProp is I believe what Agda does

[Reid Barton]

Sebastien Gouezel said:

while ensuring much shorter paths when checking that two multiplications coincide, say

The claim is you should never have to do this (and should never do it).

[Eric Wieser]

Where the former has the latter as a field

[Reid Barton]

The reason that you have to do it in mathlib is that you might get * from a CommSemiring in one place and from a GroupWithZero in another place

[Reid Barton]

It's possible that adding RingData doesn't disturb this property meaningfully, I'm not sure.

[Reid Barton]

Maybe you want to arrange the instances the other way: rather than "if you have RingData then you have Mul", it should be "if you have Mul and Add and ... then you have RingData"

[Eric Wieser]

One possible downside of the 11-single-field-typeclass approach is that to synthesize prod.ring you now have to synthesize each data field individually, so do 24 typeclass searches

[Reid Barton]

That is way less than the amount of work the TC algorithm does today. Because each search will be constant time.

[Sebastien Gouezel]

I think there are two possible problems:

• what we have currently: very long paths which lead to non-obviously defeq stuff, coming from too much bundling
• exponential blow-up if there is not enough bundling (there was a paper that has already been mentioned on Zulip showing that, if the data fields of a ring are not bundled, then the product of 4 or 5 rings is essentially unmanageable).

RingData and RingProp do not solve perfectly either of the two issues, but they still seem to me to be a reasonable balance.

[Eric Wieser]

what we have currently: very long paths which lead to non-obviously defeq stuff, coming from too much bundling

This isn't non-obvious in lean3, is it? You just unfolds all the typeclass constructors and projections, then you equate all the fields. It's only non-obvious with new-style structures because there isn't always a constructor to unfold.

[Eric Wieser]

I think there are two possible problems:

RingProp (either with RingData or separate arguments) also solves a third one, which is "I can't add another property to monoids without duplicating the whole heirarchy for rings"; for instance, idem_semiring doesn't have non-assoc versions because it generates a tonne of boilerplate. [SemiringData R] [NonAssocSemiring R] [IdemSemiring R] solves that.

[Notification Bot]

61 messages were moved here from #mathlib4 > simp normal form: ofNat or Nat.cast? by Eric Wieser.

[Eric Wieser]

I think my preference would be

class IsMonoid (M) [One M] [Mul M] [Pow M Nat] ... : Prop where
    one_mul m : 1 * m = 1
    mul_one m : m * 1 = 1
    mul_assoc a b c : a * b * c = a * (b * c)

class Monoid (M) extends One M, Mul M, Pow M Nat, IsMonoid M

/-- needed so that we can still be lazy and write `Monoid M`, but the lemmas still apply to wackier cases where all the typeclasses are separate -/
instance Monoid.reassemble [One M] [Mul M] [Pow M Nat] [IsMonoid M] : Monoid M := sorry

[Johan Commelin]

@Sebastien Gouezel Are you thinking of https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html ?

[Gabriel Ebner]

This is an interesting proposal, but we should almost certainly not think about it during the port.

[Gabriel Ebner]

I don't see any exponential blow-up issues, Ralf's set up is different.

[Gabriel Ebner]

RingData/RingProp combines the worst features of both approaches. We both get complicated projections in operations, as well as all the UX issues. I don't think that's a good idea.

[Eric Wieser]

Something we might want to consider in the port, if lean4#2074 remains tricky to resolve, would be forward-porting old-style classes

[Gabriel Ebner]

That is way less than the amount of work the TC algorithm does today. Because each search will be constant time.

This point is way overstated. You'll still need to search for Monoid (R × S)/etc. if you want to apply simp lemmas, etc. And that would work the same as it does now.

[Gabriel Ebner]

UX issues

One kind of UX issue has already been mentioned: inputting the TC arguments. This will require some core changes (because it needs to work in def etc.). So this will be a bit difficult right now. But I think longer time we want extensible binders anyhow.

[Gabriel Ebner]

But there's also another UX issue. Namely if you have 2 field arguments you'll suddenly have 24 (?) extra elements in your local context. We'd need some way to manage that (everywhere!, error messages, infoview, etc.)

[Gabriel Ebner]

Unbundled classes would make some things nicer though. For example it would make NormedSpace look syntactically the same as Field. That is, you don't need to know that A is a normed field and B is a seminormed additive commutative group to even write NormedSpace A B.

[Eric Wieser]

I'm of the opinion that we should unbundled the normed_ring classes to match what we did with topological_ring

[Eric Wieser]

I think that's been discussed elsewhere though (edit: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/normed_field/near/297799021)

[Adam Topaz]

Just a quick comment to mention that I very much support this refactor. One benefit that hasn't been discussed yet: I think this change would make it much smoother to build some sort of hierarchy builder, and for such a hypothetical builder to interface nicely with the existing hierarchy

[Eric Wieser]

port-status#analysis/normed/group/basic is maybe far enough away that we could still try this

[Eric Wieser]

#18462 is one file into the attempt

[Thomas Murrills]

One possibility for managing the instances might be to have the special syntax Yury proposed be shorthand (both forwards and backwards) for a special kind of sigma type which magically plays nicely with TC search and delaborates to its succinct special-syntax form. (I don’t know anything about how TC search works, but I’m guessing this might require some special-casing to handle it.)

So instead of actually adding instances to the context macro-style like auto-implicits, special syntax around Semigroup α would be roughly equivalent to (m : Mul α) × Semigroup α m (m present here just to show dependence), except this special version of × would both delaborate to the special syntax around Semigroup α in infoviews etc. and signal to TC search that it ought to look here for instances (something it maybe would already do, I don’t know).

We could also maybe adjust the inference rules for this special kind of “pseudobundling” (“instance bundling”?) type former if we encounter other problems—it gives us a thing to hold responsible, sort of. And given its restricted use, maybe it could be optimized behind the scenes in ways a fully general sigma type couldn’t.

But, I really don’t know the details here, so I’m just throwing this out there! If it’s impractical, at least it narrows down what is practical. :)

[Yury G. Kudryashov]

The paper about exponential blowup promotes canonical structures as a solution. What is this and how is it different?

[Thomas Murrills]

What do you mean by canonical structures?

[Adam Topaz]

https://hal.inria.fr/hal-00816703v1/document

[Adam Topaz]

Seems to just be fully bundled structures

[Thomas Murrills]

Are canonical structures what we’re doing now?

[Adam Topaz]

No, most (all?) algebraic typeclasses are semibundled

[Thomas Murrills]

Because I’m just proposing something entirely equivalent to “add all typeclass arguments to the context” (via tensor-hom) in order to help with the “frontend” problem of 24 instances suddenly showing up in the context

[Adam Topaz]

Well, maybe canonical structures means bundled structures plus some unification hints? I don't know, I haven't read the paper too closely

[Thomas Murrills]

I want to be clear that what I’m suggesting is still the unbundled approach being discussed here, where all the data fields are typeclass arguments

[Thomas Murrills]

It’s just that instead of having [[Semigroup α]] → … mean [Mul α] → [Semigroup α] → …, it means roughly [Mul α] × [Semigroup α] → … for a special version of × which lets us delaborate appropriately and keep things clean in the infoview (so that we don’t actually see the Mul instance visually in the context)

[Thomas Murrills]

Gabriel Ebner said:

But there's also another UX issue. Namely if you have 2 field arguments you'll suddenly have 24 (?) extra elements in your local context. We'd need some way to manage that (everywhere!, error messages, infoview, etc.)

This is the only problem I’m attempting to address here—I’m not proposing any fundamental change to what’s been proposed (which I like now! :) )

[Gabriel Ebner]

The adhoc bundling proposal has similar issues as the current inheritance scheme. Namely you get huge instance terms in the operations. (Think of a definition about rings referencing a definition about (add) groups, which references a definition about monoids, and then you unfold them all)

[Gabriel Ebner]

Another thing to remember is the two vector spaces over the same field issue. The operations can and do overlap between the type classes.

[Thomas Murrills]

Hmm, if I’m understanding correctly (we’ll see!) I’m not sure I see why you’d have to unfold them—they’d still be present in the context just as they would be if inserted by the “auto-implicit” proposal, but in a special ×-like type former instead of forallE. But it’s possible I don’t understand the problem as well as I thought I did.

Also I was thinking maybe TC search could special case on such a type former so that it could zoom right to the instance it needed—the type former could hold at-the-ready information about where each relevant instance was, since this kind of thing is all it would be used for.

No idea if that kind of thing is really possible or, more importantly, bears on the real issue, since now I’m a bit uncertain about my understanding of the actual issue. I wouldn’t have thought applying tensor-hom would change the computational properties!

[Gabriel Ebner]

If you have def g [(_ : Mul α) × Group α] (x : α) := .. and def f [(_ : Mul α) × (_ : Zero α) × GroupWithZero α] (x : α) := g x, then this elaborates to @g ⟨inst.1, inst.2.2⟩ x. And if you unfold e.g. @f ⟨inst.2.1, inst.2.2⟩ x, then you'd get @g ⟨⟨inst.2.1, inst.2.2⟩.1, ⟨inst.2.1, inst.2.2⟩.2.2⟩ x. Which is kind of the same situation we're in right now, but also what the original proposal here aims to avoid.

[Gabriel Ebner]

Which kind of makes me wonder: how would you write def squarefree [monoid R] (r : R) : Prop := ∀ x : R, x * x ∣ r → is_unit x without unused arguments? (Because obviously this definition only depends on * and 1, but not on the fact that these operations form a monoid.)

[Sebastien Gouezel]

Gabriel Ebner said:

I don't see any exponential blow-up issues, Ralf's set up is different.

Isn't there exponential blowup in the following situation? Say we go to fully unbundled, where a ring is given by [Zero α] [One α] [HasAdd α] [HasMul α] [HasNeg α] [HasSub α] [HasNSMul α] [HasZSMul α] [RingProp α] (so 9 classes). Then, if you start from a ring R and then build its polynomial ring R[X], the very definition of the type and all its operations depend on these 9 classes. Then, if you build the fraction field of R[X], say Frac (R[X]), the very definition of this type and all its operations depend on the ring structure on R[X]. And if you build the space of R-linear maps from Frac (R[X]) to R, again this depends on everything before. Isn't there something like 9^3 complexity coming up here?

[Thomas Murrills]

Gabriel Ebner said:

If you have def g [(_ : Mul α) × Group α] (x : α) := .. and def f [(_ : Mul α) × (_ : Zero α) × GroupWithZero α] (x : α) := g x, then this elaborates to @g ⟨inst.1, inst.2.2⟩ x. And if you unfold e.g. @f ⟨inst.2.1, inst.2.2⟩ x, then you'd get @g ⟨⟨inst.2.1, inst.2.2⟩.1, ⟨inst.2.1, inst.2.2⟩.2.2⟩ x. Which is kind of the same situation we're in right now, but also what the original proposal here aims to avoid.

oh, I see!! I was naively assuming two differences:

1) that we wouldn’t look for an instance of terms of this new product per se, which I’ll call ×', but instead look for instances of its components—that is, morally, instead of g : [A ×' B] → … we’d have “g : [A] ×' [B] → …” as far as TC search was concerned, and we’d be able to elaborate to @g ⟨instA, instB⟩ … directly

2) that e.g. f would only unfold if its first argument were an explicit constructor application, and that it would inline the components of the product right where they needed to be instead of using a projection to extract them. So @f ⟨a, b⟩ x would unfold directly to @g ⟨a, b.2⟩ x.

I don’t know if it’s possible to create such special-cased behavior for some new such ×' type former (or its constructor), but from the way you’re talking, I’m guessing it either isn’t possible or would be impractically difficult 🙃

[Thomas Murrills]

Gabriel Ebner said:

Which kind of makes me wonder: how would you write def squarefree [monoid R] (r : R) : Prop := ∀ x : R, x * x ∣ r → is_unit x without unused arguments? (Because obviously this definition only depends on * and 1, but not on the fact that these operations form a monoid.)

Should we in fact discard the requirement that it’s a monoid in that definition? It would be really nice if definitions/lemmas could be “automatically as fully general as possible”, but it would probably be bad UX to have (in general) a ton of low-level instance arguments and no idea at a glance whether a given lemma applies to your structure.

But the mathematical potential of maximal generalizability is really exciting. I wonder if it’s worth insisting that the lemma indeed only actually depend on what it needs to (no Monoid M argument) and tackling this as a (difficult) UI issue somehow.

One rough vision of such a UI-based approach: you write [Monoid M] or something as the argument at first, then a code action lets you replace it automatically with the instances you actually use in the definition/proof. That code action also figures out what the minimal structures in some hierarchy are that have these instances. (Maybe Monoid is the lowest, or maybe you have a MagmaWithOne or something.) It then annotates your def/lemma with those minimal structures somehow (by including them as arguments to a special attribute?) and this annotation is (only) used to help locate and describe this def/lemma in other places (documentation, dropdowns, etc.).

(I mean, we might not actually need the second step. Maybe that could be kept track of/inferred differently. But just to give a concrete example.)

[Yury G. Kudryashov]

What is the asymptotics of the term blow-up we have now? E.g., if you want [LinearOrderedField α] [LinearOrderedField β] : Add (α × β)?

[Gabriel Ebner]

Isn't there exponential blowup in the following situation? Say we go to fully unbundled [...]. Then, if you start from a ring R and then build its polynomial ring R[X], the very definition of the type and all its operations depend on these 9 classes. [...] Isn't there something like 9^3 complexity coming up here?

The punchline here is that defining the type R[x] only requires 0, defining addition only requires 0 and +, etc. The worst case can still be very exponential, but it should be much more reasonable in practice.

[Gabriel Ebner]

We already get exactly the same terms internally when checking that ring-to-semiring commutes with polynomials (when showing that R[x] is a semiring given that R is a ring).

[Gabriel Ebner]

Yet another UX issue: how would we define these unbundled instances? instance : Semiring Nat obviously no longer works.

[Johan Commelin]

Why not? We currently already have instance : Zero Nat up to instance : Mul Nat. So then instance : Semiring Nat would work, right?

[Johan Commelin]

In mathlib 3, it happens very often that notation instances are defined before defining instances of actual algebraic structures.

[Gabriel Ebner]

You also need nsmul, nat cast, etc. There's a lot of cases where just have a instance : Field Foo := fieldBecauseReasons and it would be unwieldy to write all fields by hand.

[Johan Commelin]

fair enough

[Thomas Murrills]

We could have “default instance arguments” in place of default fields:

class Foo α [Bar α := bar] [Baz α := baz] where
…

Plus an instance! (instances?) command which 1) allowed field-like specification of fields of instance arguments, and created instances for those arguments 2) used these default values to create instances when unspecified. (The default values wouldn’t be used in other places.)

instance! : Semigroup α where
  mul := …
  mul_assoc := …
  …

As for fieldBecauseReasons—in the new style, the necessary data instances would be present explicitly in the type of fieldBecauseReasons, right? Maybe we could extract them and set them as instances via instance! with a bit of meta code.

[Sebastien Gouezel]

Gabriel Ebner said:

Isn't there exponential blowup in the following situation? Say we go to fully unbundled [...]. Then, if you start from a ring R and then build its polynomial ring R[X], the very definition of the type and all its operations depend on these 9 classes. [...] Isn't there something like 9^3 complexity coming up here?

The punchline here is that defining the type R[x] only requires 0, defining addition only requires 0 and +, etc. The worst case can still be very exponential, but it should be much more reasonable in practice.

The example of polynomials is not good, indeed, because you don't need all the information to build the new type. But my point is that it happens very often that you need all the information to build the new type (for instance when you take the fraction ring, or tensor products), and so the exponential behavior will definitely come up in practice. You can look up in mathlib how the Clifford algebra is defined as a quotient of the tensor algebra, which is itself a quotient of the free algebra, which is itself built as a quotient made from the information from a semiring. Unbundling everything would make this a nightmare performancewise, if I understand correctly.

[Reid Barton]

I don't see why it makes a big difference, especially as each of those steps is a named construction with its own instances.

[Reid Barton]

Instead of one definition per layer you have (say) five, and they refer to the five definitions of the previous layer in the same way that the fields of one definition referred to the fields of the previous definition.

[Yury G. Kudryashov]

I see why it's bad if you want to unfold all these definitions in a lemma but probably this means that we should have more irreducible definitions (either as in irreducible_def or as in one-field structure).

[Reid Barton]

In the example of the Coq blog post I think it makes a difference whether you work with G x G x G x G x G or G2 := G x G, G3 = G x G2, G4 = G x G3, G5 = G x G4.

[Reid Barton]

Because the second forces you to do the correct sharing, that you could fail to do for the first

[Reid Barton]

Of course if you unfold everything you're in for a bad time either way, so I agree with Yury that more irreducibility would be a good idea