How to handle transfer to bundled homs

Stream: maths

[Chris Hughes]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

@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]

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]

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]

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]

We need non-linear typechecking. :-)

[Johan Commelin]

Does that help?

[Scott Morrison]

"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]

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]

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

[Johan Commelin]

We could do that (-;

[Johan Commelin]

Sounds like a pretty ugly hack

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

oh, duh

[Johan Commelin]

So what is the type of coeff n?

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

that doesn't seem so bad

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Johan Commelin]

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

[Scott Morrison]

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]

But maybe that's what it takes...

[Johan Commelin]

Anyway, I need to run to supervise an LA exam

[Johan Commelin]

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

[Scott Morrison]

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]

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

[Scott Morrison]

good luck!

[Scott Morrison]

Yeah, I agree it's worrying.

[Johan Commelin]

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

[Chris Hughes]

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

[Chris Hughes]

Oh but this is power series not polynomials.

[Johan Commelin]

It's still true, but it needs more work

[Mario Carneiro]

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

[Johan Commelin]

That's Scott's constant_term

[Chris Hughes]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Chris Hughes]

Rings and abelian groups and modules

[Chris Hughes]

The file Kenny wrote on direct limit.

[Johan Commelin]

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]

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]

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

[Kevin Buzzard]

I mean, having both long term.

[Kevin Buzzard]

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]

I think we want mainly bundled homs and occasionally unbundled.

[Chris Hughes]

But I think direct_limit should use bundled.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Algebraic closures would be a marvellous place to test it out

[Scott Morrison]

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]

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]

I would really like to address that soon.

[Johan Commelin]

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]

It can figure out those metavariables from φ

[Johan Commelin]

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]

I think unfortunately both unbundled and bundled have major downsides.

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Patrick Massot]

Ok, you thought about this already...

[Johan Commelin]

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]

Lean doesn't like the example

[Patrick Massot]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Chris Hughes]

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

[Chris Hughes]

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]

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]

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Chris Hughes]

line 176 of field_theory/mv_polynomial.

[Chris Hughes]

Not in the diff.

[Chris Hughes]

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

[Chris Hughes]

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]

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

[Johan Commelin]

Never mind, I should shut up

[Johan Commelin]

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

[Johan Commelin]

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

[Yury G. Kudryashov]

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.