Zulip Chat Archive

Stream: general

Topic: how to deal with "underbundling"

Eric Rodriguez (Sep 01 2022 at 16:41):

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 (Sep 01 2022 at 17:07):

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 (Sep 01 2022 at 17:40):

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 (Sep 01 2022 at 19:11):

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 (Sep 01 2022 at 19:12):

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

Eric Rodriguez (Sep 01 2022 at 19:13):

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 (Sep 01 2022 at 19:13):

(or wait, did that finally get fixed?)

Eric Wieser (Sep 02 2022 at 07:49):

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

Kevin Buzzard (Sep 02 2022 at 08:46):

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.

Last updated: Dec 20 2023 at 11:08 UTC