how to deal with "underbundling"

Stream: general

[Eric Rodriguez]

I've noticed that there are lots of definitions made, which later on are proved to be a foo_hom (100, 200, 300+ lines later). This is all well and good, but it ends up duplicating the API in ways that aren't great. I'd like to propose that we instead try and get the strongest bundling possible, and leave all auxilliary earlier definitions as either private or duplicated in the case when they aren't directly provable by the bundled definition results. I'm currently thinking of absolute_values like docs#complex.abs, docs#padic_norm for this, which need a lot of duplicated API because of this (and also API that doesn't apply on either side!)

[Riccardo Brasca]

I usually suggest in PRs to introduce foo' as a plain function, prove stuff like foo'_add and then define foo as bundled hom. I agree that foo' should never be used.

[Wrenna Robson]

I was worrying about this the other day with reference to hamming_dist, which still feels like it has too much duplication. But really (because that has domain nat) to fix that I would some kind of generalisation of dist...

[Eric Wieser]

Sometimes the level of bundling depends on other ambient typeclasses though, and it's easier to make the fully-unbundled form simp-normal than it is to do that with the minimally-unbundled one.

[Eric Rodriguez]

this is true, for example docs#has_neg.has_abs vs docs#absolute_value.abs

[Eric Rodriguez]

but sometimes this can be an issue with other things (the one I hate the most is docs#polynomial.map_ring_hom, caused solely because dot notation doesn't work for bundled morphisms)

[Eric Rodriguez]

(or wait, did that finally get fixed?)

[Eric Wieser]

Arguably docs#polynomial.map should relax its assumptions to only require f : R → S

[Kevin Buzzard]

I guess so! And it should also be renamed map'. And then map can be the one which eats a ring hom and emits a ring hom.