Zulip Chat Archive

Stream: maths

Topic: How to handle transfer to bundled homs


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 16 2019 at 14:32):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 →*+.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Scott Morrison (Sep 17 2019 at 05:34):

We need non-linear typechecking. :-)

view this post on Zulip Johan Commelin (Sep 17 2019 at 05:35):

Does that help?

view this post on Zulip 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 ->+"

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 17 2019 at 05:35):

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

view this post on Zulip Johan Commelin (Sep 17 2019 at 05:36):

We could do that (-;

view this post on Zulip Johan Commelin (Sep 17 2019 at 05:36):

Sounds like a pretty ugly hack

view this post on Zulip Scott Morrison (Sep 17 2019 at 05:36):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 17 2019 at 05:37):

oh, duh

view this post on Zulip Johan Commelin (Sep 17 2019 at 05:37):

So what is the type of coeff n?

view this post on Zulip Scott Morrison (Sep 17 2019 at 05:37):

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

view this post on Zulip Scott Morrison (Sep 17 2019 at 05:38):

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

view this post on Zulip Scott Morrison (Sep 17 2019 at 05:38):

that doesn't seem so bad

view this post on Zulip Scott Morrison (Sep 17 2019 at 05:39):

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

view this post on Zulip 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)?)

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 17 2019 at 05:41):

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

view this post on Zulip Johan Commelin (Sep 17 2019 at 05:41):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 17 2019 at 05:41):

But maybe that's what it takes...

view this post on Zulip Johan Commelin (Sep 17 2019 at 05:42):

Anyway, I need to run to supervise an LA exam

view this post on Zulip Johan Commelin (Sep 17 2019 at 05:42):

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

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Sep 17 2019 at 05:44):

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

view this post on Zulip Scott Morrison (Sep 17 2019 at 05:44):

good luck!

view this post on Zulip Scott Morrison (Sep 17 2019 at 05:44):

Yeah, I agree it's worrying.

view this post on Zulip Johan Commelin (Sep 17 2019 at 05:45):

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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Sep 17 2019 at 05:52):

Oh but this is power series not polynomials.

view this post on Zulip Johan Commelin (Sep 17 2019 at 06:03):

It's still true, but it needs more work

view this post on Zulip Mario Carneiro (Sep 17 2019 at 06:41):

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

view this post on Zulip Johan Commelin (Sep 17 2019 at 07:09):

That's Scott's constant_term

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Sep 18 2019 at 15:24):

Rings and abelian groups and modules

view this post on Zulip Chris Hughes (Sep 18 2019 at 15:24):

The file Kenny wrote on direct limit.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Sep 18 2019 at 15:28):

I mean, having both long term.

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Sep 18 2019 at 15:31):

I think we want mainly bundled homs and occasionally unbundled.

view this post on Zulip Chris Hughes (Sep 18 2019 at 15:32):

But I think direct_limit should use bundled.

view this post on Zulip Johan Commelin (Sep 18 2019 at 15:35):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 18 2019 at 15:35):

Algebraic closures would be a marvellous place to test it out

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 18 2019 at 23:40):

I would really like to address that soon.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 20 2019 at 11:25):

It can figure out those metavariables from φ

view this post on Zulip 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...

view this post on Zulip Chris Hughes (Sep 20 2019 at 11:26):

I think unfortunately both unbundled and bundled have major downsides.

view this post on Zulip Johan Commelin (Sep 20 2019 at 11:26):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Sep 20 2019 at 11:27):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 11:27):

Ok, you thought about this already...

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 20 2019 at 11:31):

Lean doesn't like the example

view this post on Zulip Patrick Massot (Sep 20 2019 at 11:32):

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

view this post on Zulip Johan Commelin (Sep 20 2019 at 11:40):

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

view this post on Zulip Patrick Massot (Sep 20 2019 at 11:41):

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

view this post on Zulip Chris Hughes (Sep 20 2019 at 11:41):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 20 2019 at 11:55):

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

view this post on Zulip Chris Hughes (Sep 20 2019 at 11:55):

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

view this post on Zulip Mario Carneiro (Sep 20 2019 at 11:56):

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

view this post on Zulip Chris Hughes (Sep 20 2019 at 11:59):

line 176 of field_theory/mv_polynomial.

view this post on Zulip Chris Hughes (Sep 20 2019 at 11:59):

Not in the diff.

view this post on Zulip Chris Hughes (Sep 20 2019 at 11:59):

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

view this post on Zulip 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')

view this post on Zulip Johan Commelin (Sep 20 2019 at 12:54):

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

view this post on Zulip Johan Commelin (Sep 20 2019 at 12:55):

Never mind, I should shut up

view this post on Zulip Johan Commelin (Sep 23 2019 at 14:20):

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

view this post on Zulip Johan Commelin (Sep 23 2019 at 14:21):

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

view this post on Zulip 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