## Stream: maths

### Topic: How to handle transfer to bundled homs

#### Chris Hughes (Sep 13 2019 at 09:22):

It's seems to have been decided that using bundled ring homs and group homs is going to be the mathlib style. Currently the library is not set up to make it easy for people to write new code using bundled homs, and it is quite a major refactor to update the library to do this. I think perhaps the bulk of the refactor has to be done in one go, as soon as the ideal file is updated, a bunch more stuff will have to be updated as well. Because of this I'm a little bit cautious about merging stuff that will make this refactor harder.

What's the best way of handling this? Should we refuse to merge anything that uses unbundled homs, or will a more gradual approach work?

#### Johan Commelin (Sep 13 2019 at 14:46):

Thanks for starting this discussion. I think people said that the refactor could be done slowly and gradually, even though the total effort would be more than when everything's done in one go.

#### Johan Commelin (Sep 13 2019 at 14:47):

I realize that the amount of unbundled stuff being added to the library might grow faster than the amount of parts in the library being refactored... so the process might never converge.

#### Chris Hughes (Sep 13 2019 at 14:52):

Giving bundled versions of the lemmas in the most used parts of the library might help the process converge faster. I'm thinking of ideals, subgroups, and maybe polynomial.eval and map

#### Johan Commelin (Sep 16 2019 at 14:32):

Does anyone else have 2 cents to contribute? @Kevin Buzzard @Mario Carneiro

#### Kevin Buzzard (Sep 16 2019 at 18:28):

I don't have a clue. I think I might have been at least partially to blame for the fact that we have both bundled and unbundled versions of some things, but I was just annoyed that everyone seemed to think that bundled was the way to go and yet unbundled was what we had.

#### Mario Carneiro (Sep 16 2019 at 22:08):

I think it would be good to expand the library as needed when writing new bundled hom code is difficult. That should require a lot less up front work than a full conversion

#### Scott Morrison (Sep 17 2019 at 00:50):

Let’s just make sure there are lots of big “deprecated” warnings everywhere old stuff is being used, and hope that people don’t PR too much stuff extending the use of deprecated code...

#### Johan Commelin (Sep 17 2019 at 04:23):

That's exactly what this thread is about. For an example, see my PR on order of power series: #1292
(1) It sets up a bunch of maps and proves that they are is_add_group_homs and occasionally, under suitable conditions they are actually is_ring_homs... (In particular, coeff 0 is a ring hom, whereas in general coeff n is only additive.)
(2) Moreover, a bunch of these maps are already defined before the algebraic structure on their source is there. They are used in setting up this structure.

Both of these points are awkard to pull of in the bundled setting. What do we do with this PR? Because it doubles down on unbundled homs instead of easing the transition to bundled homs.

#### Scott Morrison (Sep 17 2019 at 05:05):

I don't really understand what could be awkward. Of course you can define the maps-merely-as-functions before the algebraic structure is there, but surely you can define an is_ring_hom neither earlier nor later than you can define a ring_hom. Is the point that you need then to restate some earlier results, so they are about the coercion of the ring_hom, rather than about the bare function?

#### Johan Commelin (Sep 17 2019 at 05:29):

@Scott Morrison Yep, you have to restate a bunch of stuff to address (2). I agree that this is not a big problem, only annoying. But (1) is more of an issue. Suppose we have addressed (2), so that for n : ℕ we have a coeff n : power_series R →+ R. Then there is not a very nice way to magically have coeff 0 become a →*+.

#### Scott Morrison (Sep 17 2019 at 05:30):

Ah, I see, that indeed is horrible, and I've been encountering exactly the same issue with functors and monoidal functors while working on enriched categories recently.

#### Scott Morrison (Sep 17 2019 at 05:31):

Sometimes life just gives you a functor, and your job is to add the structure of a monoidal functor. At the moment I have a horrible hack.

#### Scott Morrison (Sep 17 2019 at 05:32):

I've defined functorial and monoidal as typeclasses on functions, as unbundled versions of functor and monoidal_functor. But then at some point I find myself with F : Functor C D, and writing monoidal (F.obj) --- that is, I unbundle a bundled functor, and use a typeclass to express that I know a monoidal structure on it. Yuck!

#### Scott Morrison (Sep 17 2019 at 05:34):

We need non-linear typechecking. :-)

Does that help?

#### Scott Morrison (Sep 17 2019 at 05:35):

"I promise that eventually I'll show that this is a ->*+, and in the meantime only use the coercion to ->, and after a little while the coercion to ->+"

#### Johan Commelin (Sep 17 2019 at 05:35):

I mean, once you bundle coeff into an add_hom... you kind of promise that you don't suddenly want to treat it as a ring hom

#### Johan Commelin (Sep 17 2019 at 05:35):

So you want the type of coeff n to depend on n?

#### Johan Commelin (Sep 17 2019 at 05:36):

We could do that (-;

#### Johan Commelin (Sep 17 2019 at 05:36):

Sounds like a pretty ugly hack

#### Scott Morrison (Sep 17 2019 at 05:36):

Sorry, I don't undestand what you're saying about depending on n.

#### Johan Commelin (Sep 17 2019 at 05:37):

For n > 0 you will not get a ring hom. But for n = 0 you do get a ring hom.

oh, duh

#### Johan Commelin (Sep 17 2019 at 05:37):

So what is the type of coeff n?

#### Scott Morrison (Sep 17 2019 at 05:37):

I see, sorry, I wasn't paying attention.

#### Scott Morrison (Sep 17 2019 at 05:38):

well, don't we jsut define constant_term : power_series R ->*+ R?

#### Scott Morrison (Sep 17 2019 at 05:39):

and a lemma that coeff 0 = (constant_term : power_series R ->+ R)?

#### Scott Morrison (Sep 17 2019 at 05:40):

(oof, do you separately need (coeff 0 : power_series R -> R) = (constant_term : power_series R -> R)?)

#### Scott Morrison (Sep 17 2019 at 05:40):

But I think the general answer here is that you make a "first pass" development, that mostly stays private, and then restate it all as public API at the end.

#### Scott Morrison (Sep 17 2019 at 05:41):

Rather than pretend it's possible to make the sausage in front of everyone.

#### Johan Commelin (Sep 17 2019 at 05:41):

Yeah, but in this case you need even a "third pass" defining constant_term...

#### Scott Morrison (Sep 17 2019 at 05:41):

and maybe the lesson we're learning is that unbundled morphisms are good for the private development, and bundled morphisms are good for the API

#### Johan Commelin (Sep 17 2019 at 05:41):

But maybe that's what it takes...

#### Johan Commelin (Sep 17 2019 at 05:42):

Anyway, I need to run to supervise an LA exam

#### Johan Commelin (Sep 17 2019 at 05:42):

Wish me luck... we'll have to grade them afterwards :face_palm:

#### Scott Morrison (Sep 17 2019 at 05:43):

Why is that? In the private development we prove is_add_group_hom (internals.coeff n) and is_ring_hom (internals.coeff 0), and then in the public API we provide
coeff (n : nat) : power_series R ->+ R := add_group_hom.of (internals.coeff n), and constant_term : power_series R ->+* R := ring_hom.of (internals.coeff 0).

#### Johan Commelin (Sep 17 2019 at 05:44):

Back in the day the whole concept of constant_term wasn't necessary

good luck!

#### Scott Morrison (Sep 17 2019 at 05:44):

Yeah, I agree it's worrying.

#### Johan Commelin (Sep 17 2019 at 05:45):

My point is... the file will probably become 2 times as long

#### Chris Hughes (Sep 17 2019 at 05:51):

coeff 0 is eval 0 so we could just make eval 0 our canonical way of talking about the constant term.

#### Chris Hughes (Sep 17 2019 at 05:52):

Oh but this is power series not polynomials.

#### Johan Commelin (Sep 17 2019 at 06:03):

It's still true, but it needs more work

#### Mario Carneiro (Sep 17 2019 at 06:41):

Why not have coeff_0? Then there is no problem with it having a different type

#### Johan Commelin (Sep 17 2019 at 07:09):

That's Scott's constant_term

#### Chris Hughes (Sep 18 2019 at 15:18):

Do we want two versions of everything like is_ring_hom.ker in the meantime whilst the gradual refactor is happening?

#### Kevin Buzzard (Sep 18 2019 at 15:20):

That's a good question. I want to say no -- we should just develop the bundled theory and stop supporting unbundled ring homs completely, moving them to bundled ring homs whenever we can be bothered. Is this a very naive viewpoint?

#### Chris Hughes (Sep 18 2019 at 15:22):

Looking at something like direct_limit, transferring to bundled homs is quite a hard refactor at the moment. Currently a directed system is just a set of functions, and then there's a hypothesis that they're all ring homs. It will have to become a set of morphisms in a category.

#### Chris Hughes (Sep 18 2019 at 15:23):

This approach means the refactor has to be done in one go. Who's going to do that?

#### Kevin Buzzard (Sep 18 2019 at 15:23):

Are we talking about direct limits in arbitrary categories or direct limits in the category of rings?

#### Chris Hughes (Sep 18 2019 at 15:24):

Rings and abelian groups and modules

#### Chris Hughes (Sep 18 2019 at 15:24):

The file Kenny wrote on direct limit.

#### Johan Commelin (Sep 18 2019 at 15:26):

I'm not sure we can get away with only one of the two. Category theory has bundled homs and bundled funtors all over the place. Yet Scott confessed that he introduced functorial and monoidal.

#### Johan Commelin (Sep 18 2019 at 15:27):

I intuitively tend to agree with his "slogan" that unbundled stuff is good for setting things up, but that bundled stuff is good for API's that users should see.

#### Kevin Buzzard (Sep 18 2019 at 15:28):

I thought there was some sort of philosophical objection to having both? Having both doesn't bother me...

#### Kevin Buzzard (Sep 18 2019 at 15:28):

I mean, having both long term.

#### Kevin Buzzard (Sep 18 2019 at 15:29):

And the general rule can be to not develop any new API for the unbundled stuff unless you're doing foundational things like direct_limit.

#### Chris Hughes (Sep 18 2019 at 15:31):

I think we want mainly bundled homs and occasionally unbundled.

#### Chris Hughes (Sep 18 2019 at 15:32):

But I think direct_limit should use bundled.

#### Johan Commelin (Sep 18 2019 at 15:35):

Well... it's there already, if you don't bind bundling some objects along the way...

#### Johan Commelin (Sep 18 2019 at 15:35):

If we wait a couple of days, the new concrete category infrastructure due to @Yury G. Kudryashov seems very promising.

#### Johan Commelin (Sep 18 2019 at 15:35):

Algebraic closures would be a marvellous place to test it out

#### Scott Morrison (Sep 18 2019 at 23:38):

I'm actually coming around to the idea that we want both bundled and unbundled versions of everything, even though we have to pay in the form of writing extra glue code. The glue code seems to work very well; that is, it only needs to be written once when setting up a new bundled/unbundled pair, and then it's pretty straightforward for the user.

#### Scott Morrison (Sep 18 2019 at 23:39):

Regarding direct_limit --- there's actually some duplication now between the direct_limits file, and the algebra/category/CommRing/(co)limits.lean files.

#### Scott Morrison (Sep 18 2019 at 23:40):

I would really like to address that soon.

#### Johan Commelin (Sep 20 2019 at 11:24):

This is what I don't like about bundled homs: I write

∀ n, coeff n φ = coeff n ψ


and I get red squiggles under coeff saying:

function expected at
coeff n
term has type
mv_power_series ?m_1 ?m_2 →+ ?m_2


#### Johan Commelin (Sep 20 2019 at 11:25):

It can figure out those metavariables from φ

#### Johan Commelin (Sep 20 2019 at 11:25):

But it won't do that. So we need to hand hold it. And that means we have to explicitly provide a bunch of types all the time...

#### Chris Hughes (Sep 20 2019 at 11:26):

I think unfortunately both unbundled and bundled have major downsides.

#### Johan Commelin (Sep 20 2019 at 11:26):

Would this be an example of type class search failure that Leo wants to see?

#### Patrick Massot (Sep 20 2019 at 11:27):

Johan, can you get a minimized version of this that we could give to Leo and Daniel for Lean 4 miraculous resolution?

#### Johan Commelin (Sep 20 2019 at 11:27):

Specifically: a coercion is not kicking in. And it's well-understood why it doesn't.

#### Johan Commelin (Sep 20 2019 at 11:31):

Voila, a minimal example:

section
variables {α : Type} [monoid α]

def my_id : α →* α :=
{ to_fun := id, map_one' := rfl, map_mul' := λ _ _, rfl }

example (a : α) : my_id a = a := rfl

end


#### Johan Commelin (Sep 20 2019 at 11:31):

Lean doesn't like the example

#### Patrick Massot (Sep 20 2019 at 11:32):

It's not minimal since →* is not in core, right?

#### Johan Commelin (Sep 20 2019 at 11:40):

Aha... are there examples of bundled functions in core?

#### Patrick Massot (Sep 20 2019 at 11:41):

Probably not, but you can include (a minimized version of) the definition.

#### Chris Hughes (Sep 20 2019 at 11:41):

Just define monoid_hom in your minimal example, it's only about three lines.

#### Chris Hughes (Sep 20 2019 at 11:45):

There's a mysterious (to me) failure of has_coe_to_fun in #1404. Is this also well understood? It's not at all obvious to me why removing some decidable_eq assumptions should break this lemma.

#### Mario Carneiro (Sep 20 2019 at 11:54):

I think Leo mentioned this issue in his request (coercions are not fired unless all metavariables are instantiated), but let's make a minimal example to show this off

#### Mario Carneiro (Sep 20 2019 at 11:55):

This can be fixed in lean 4 but we have to make the problem clear

#### Chris Hughes (Sep 20 2019 at 11:55):

The one in #1404 doesn't fire even with type annotations.

#### Mario Carneiro (Sep 20 2019 at 11:56):

could you summarize the problem? I don't see it in the commit

#### Chris Hughes (Sep 20 2019 at 11:59):

line 176 of field_theory/mv_polynomial.

Not in the diff.

#### Chris Hughes (Sep 20 2019 at 11:59):

But the coe_to_fun in that statement is broken even with type annotations.

#### Chris Hughes (Sep 20 2019 at 12:00):

maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

#### Johan Commelin (Sep 20 2019 at 12:54):

Next issue... bundled homs were supposed to make map_add easier for simp.

#### Johan Commelin (Sep 20 2019 at 12:55):

Never mind, I should shut up

#### Johan Commelin (Sep 23 2019 at 14:20):

I've bundled the homs in the order PR: #1292

#### Johan Commelin (Sep 23 2019 at 14:21):

In the end, I think it wasn't even too painful.

#### Yury G. Kudryashov (Sep 28 2019 at 20:09):

I think, the problem is that currently the type of coe_fn f can depend on f, not only its type. On the one hand, this way we can coerce to function something like

structure bundled_fun :=
(dom : Type)
(codom : Type)
(to_fun : dom → codom)


On the other hand, if we have coe_fn f x, then Lean can't start looking at x before it knows f. I see two possible solutions:

• Define something like
lean structure has_simple_coe_to_fun (α : Type*) (β : out_param Type*) := (coe : α → β) 
and try it before has_coe_to_fun

• Introduce convention (similar to, e.g., Python) that coe_fn f is a notation for f.to_fun.

Sure, each approach has its pros and cons. Hope, someone will come with a better idea.

Last updated: May 09 2021 at 09:11 UTC