Zulip Chat Archive

Stream: new members

Topic: Type classes to bundled structures


Nicolò Cavalleri (Jul 25 2021 at 16:53):

I read somewhere that mathlib has been moving from type classes to bundled structures. I don't understand what this mean, can someone explain this to me and make me an explicit example?

Kevin Buzzard (Jul 25 2021 at 16:54):

we use monoid_hom not is_monoid_hom, and have been doing so for some time.

Nicolò Cavalleri (Jul 25 2021 at 16:57):

Ok I believe I joined the community after this change had already happened... before there was a class is_monoid_hom? Why would you ever do that? I mean what was the advantage of that?

Kevin Buzzard (Jul 25 2021 at 16:58):

there is a class is_monoid_hom! In the undeprecate branch I'm changing it to a structure. You seem to be speaking as if it is well-known how to do monoid homomorphisms in Lean's type theory. This was not always the case.

Kevin Buzzard (Jul 25 2021 at 17:00):

We tried is_monoid_hom first, and then monoid_hom, and the latter worked better so that's the one we've been using.

Nicolò Cavalleri (Jul 25 2021 at 17:01):

Oh I see I guess I just have the perspective from the future but I would see things differently if I were not used to bundled morphisms

Kevin Buzzard (Jul 25 2021 at 17:02):

Right. When we were building the algebra hierarchy I was asking questions like "so how do we do group homomorphisms", expecting the answer to be well-known, and it turned out that the answer was that one has to experiment to find out. I was very surprised! As a mathematician I just expected everything to be very well-understood, but this was not the case at all.

Kevin Buzzard (Jul 25 2021 at 17:03):

Even if you look at how they're done in Coq, this doesn't tell you how to do them in Lean, because they emphasize canonical structures and we emphasize type class inference etc.

Nicolò Cavalleri (Jul 25 2021 at 17:03):

I still don't see why would you make is_monoid_hom a class instead of a structure : Prop in case you want it to be a proposition instead of bundling it

Kevin Buzzard (Jul 25 2021 at 17:04):

Because you want the composite of two monoid homomorphisms to automatically be a monoid homomorphism.

Kevin Buzzard (Jul 25 2021 at 17:05):

However it turned out that type class inference would often not fire, and then it turned out that dot notation was super-powerful, and so the bundled version won.

Kevin Buzzard (Jul 25 2021 at 17:05):

There are still many is_monoid_homs in mathlib, although there are far fewer in the undeprecate branch.

Kevin Buzzard (Jul 25 2021 at 17:06):

There are also many is_ring_hom, is_submonoid, is_subgroup, is_subring and is_subfields.

Kevin Buzzard (Jul 25 2021 at 17:06):

I'll push the many hours of work I've done on this branch today so you can see an update :-)

Kevin Buzzard (Jul 25 2021 at 17:07):

https://github.com/leanprover-community/mathlib/compare/undeprecate

Yakov Pechersky (Jul 25 2021 at 17:12):

Consider something like polynomial.coeff p n. The way that coeff is defined is separate from the proofs that it's a hom. So one might use is_ring_hom to prove some lemmas, let's say about sums. Sometimes the definition of the function (the data) can come much earlier than the proofs that it's a hom.

Yakov Pechersky (Jul 25 2021 at 17:13):

Another example is matrix.adjugate. Proving that it's a monoid_hom is more complex than just defining the adjugate.


Last updated: Dec 20 2023 at 11:08 UTC