Stream: general

Topic: ring_hom.comp

Kevin Buzzard (Dec 10 2020 at 11:53):

Amelia just pointed out to me that in docs#ring_hom.comp two of the semiring instances are [] and one is {}. This surprised me! Why do we do it like this? There's no mention of this phenomenon in the module doc.

Anne Baanen (Dec 10 2020 at 12:03):

Something similar also happens in docs#linear_map.comp and docs#linear_map.map_neg. Presumably finding the arguments by unification gives (used to give?) less diamonds than doing it by typeclass search?

Eric Wieser (Dec 10 2020 at 12:28):

https://leanprover-community.github.io/mathlib_docs/notes.html#implicit%20instance%20arguments

Eric Wieser (Dec 10 2020 at 12:29):

As for why one is different to the others, it's probably an accident. Keeping track of which variables are currently in your scope is really hard!

Kevin Buzzard (Dec 10 2020 at 13:26):

Oh -- so when this is happening there should be a library note? Thanks! Yes, I figured out (in the sense of "Amelia explained it to me") how it could work in principle but then I was confused why it was happening in some places but not others.

Reid Barton (Dec 10 2020 at 13:29):

Non-obvious design decisions like this are what comments are for generally, and library notes are supposed to be a mechanism to deduplicate and cross-link repeating issues

Kevin Buzzard (Dec 10 2020 at 13:31):

This seems to be a repeating issue though -- we first discovered it in the lifting property liftq for quotient modules, and then in mkq, and then in comp.

Reid Barton (Dec 10 2020 at 13:33):

right, so it would be good to reference implicit instance arguments where it comes up, and then add specific comments about why it pertains to some but not all of the classes involved

Reid Barton (Dec 10 2020 at 13:34):

Here it's not really clear whether it's intentional, though it seems likely...

Eric Wieser (Dec 10 2020 at 13:34):

Maybe I'll try and tweak docgen to add backreferences from the notes section...

Eric Wieser (Dec 10 2020 at 13:35):

But the note _is_ there already: https://leanprover-community.github.io/mathlib_docs/algebra/ring/basic.html#ring_hom.to_monoid_with_zero_hom

Eric Wieser (Dec 10 2020 at 13:35):

It's just not repeated for every single definition in the file

Chris Hughes (Dec 14 2020 at 21:27):

@Anne Baanen its not about diamonds, it's just faster to find it by unification than type class inference.

Last updated: May 15 2021 at 23:13 UTC