Zulip Chat Archive

Stream: general

Topic: encoding of modules

Jeremy Avigad (Oct 18 2019 at 18:23):

@Mario Carneiro Assia asked me why we now use [ring R] [add_comm_group M] [module R M] instead of bunding everything into the module structure. As I recall, this decision had to do with type class problems e.g. with expressions x + y where there is no trace of the ring structure, making it hard to find the right module, though not hard to find the relative group. Do you have a better explanation?

Kevin Buzzard (Oct 18 2019 at 18:38):

Just to remark that we also use [comm_ring R] [topological_space R] [topological_ring R] instead of bundling everything into the topological ring structure. But is this a different issue?

Johan Commelin (Oct 18 2019 at 19:03):

@Jeremy Avigad I think it is to support the possibility that Mis a module over several different rings. In such cases you wouldn't want the additive group structure to change, but only the scalar multiplication. Hence the two step process.

Johan Commelin (Oct 18 2019 at 19:05):

Before this refactor, we had a setup where R was an out_param. (And it still didn't really support having two scalar rings on the same M, IIRC.) But this out_param caused lots of headaches and issues with type-class search. At the time I was even more of a newbie then I am nowadays, so I really didn't understand what was going on. All I knew was that it was impossible to use modules in any non-trivial way. Then Mario and Kenny refactored it, and nowadays they are quite pleasant to use.

Johan Commelin (Oct 18 2019 at 19:06):

Of course want could define Module R (and in fact this has recently been done by @Robert Spencer), and write M : Module R. This has the benefit that you can (and we have) a category structure on Module R. But the problem is that it makes it harder to talk about \C as an \R-module, etc... Also changing the scalar ring is not so transparent anymore.

Jeremy Avigad (Oct 19 2019 at 16:23):

Thanks, Johan. I'll pass that along.

Jeremy Avigad (Oct 20 2019 at 18:08):

I think I remember another issue: when R was marked as an out_param, it led to looping, maybe because every ring is an instance of a module or because some modules give rise to rings. Anyhow, it would be good if the reasons for the decision were documented in algebra/module.

Kevin Buzzard (Oct 20 2019 at 18:53):

Yes every ring is a module over itself and also over every subring of itself

Kevin Buzzard (Oct 20 2019 at 19:00):

I found this all very interesting. We did all this very inefficiently because of poor communication. I can quite believe that the definition of a module over a ring was there even in 2017 when I started on Lean, but there was nothing nontrivial proved about them. Then when I started pushing for things like noetherian modules, and @Kenny Lau and @Johan Commelin and I started actually trying to do MSc level algebra we were instantly hit by outparam problems which we didn't understand because we're mathematicians. Some initial hacks were tried but somehow the set-up just couldn't be made to work. I was trying to prove things like the Hilbert Basis theorem and other mathematicians were doing other things and it was only then that it became clear what we actually wanted. Mario acted as interpreter between us and Sebastian and it was eventually decided to do a huge module refactor, which took Mario a long time and I imagine was a huge effort. There is some sort of moral there. Maybe it's just that if a mathematician wants a structure they had better be very clear as early as possible about what they want to do with it. This is hard though because "we just want to do maths with it", and this isn't a good enough answer

Jeremy Avigad (Oct 20 2019 at 23:06):

@Mario Carneiro Do you remember what the problems were and how the refactor solved them? If there are lessons here to be learned, we shouldn't squander the opportunity.

Mario Carneiro (Oct 20 2019 at 23:08):

The problem was the out_param. I think we've gotten better at it, but you have to be careful when you use these classes because it's easy to get the binders wrong in theorems. Once we figured that out it mostly worked, except for the inherent limitation that a module could only have one base ring

Jeremy Avigad (Oct 20 2019 at 23:12):

What do you mean, "get the binders wrong in theorems"? What did we get better at?

Mario Carneiro (Oct 20 2019 at 23:13):

In short, you can give module the type module (R : out_param Type) {_: out_param (ring R)} (M : Type) : Type extends add_comm_group M, and then in theorems you use the binders {R : Type} {_ : ring R} {M : Type} [module R M]

Mario Carneiro (Oct 20 2019 at 23:13):

people want to put ring R in an instance binder and that causes ring ? typeclass searches which causes looping

Mario Carneiro (Oct 20 2019 at 23:15):

It took a while after the definition of module for this to hit us because there weren't any ring constructions yet, but when they got introduced this caused lots of unrelated typeclass problems to fail

Jeremy Avigad (Oct 20 2019 at 23:19):

Oh, I get it. But actually we use class module (α : Type u) (β : Type v) [ring α] [add_comm_group β] extends semimodule α β where add_comm_group is on the outside. And what goes wrong if we put everything but the two types on the inside?

Mario Carneiro (Oct 20 2019 at 23:30):

with the non-out_param version, the add_comm_group has to come outside

Mario Carneiro (Oct 20 2019 at 23:32):

Otherwise, if you have a parent coercion from module to add_comm_group, you get a search like add_comm_group G <- module ? G <- ring ?

Jeremy Avigad (Oct 20 2019 at 23:48):

O.k., so if I understand correctly, in hindsight, we could have kept the original encoding of module (with everything but the types on the inside), as long as we were careful not to mark R for type class inference in the instances. Alternatively, we can do what is in the library now.

As far as you can tell, are both equally good? It would be more consistent with everything else we are doing to put it all on the inside.

Mario Carneiro (Oct 20 2019 at 23:50):

They are equally good, but they make some different assertions about mathematical practice and the original approach turned out not to be a reasonable assumption

Mario Carneiro (Oct 20 2019 at 23:50):

that is, a module has only one base ring

Mario Carneiro (Oct 20 2019 at 23:51):

That's the real reason we switched. Kevin had some examples of module structures he wanted that didn't fit the mold, and finsupp already had some module constructions that didn't work and had to be defs

Mario Carneiro (Oct 20 2019 at 23:53):

This is basically the fundamental assumption that licenses using typeclasses. If it's not true, then you have to do things some other way - you have to be more explicit about what you want because it matters which one you get

Jeremy Avigad (Oct 21 2019 at 00:06):

Thanks! That's really helpful.

Kevin Buzzard (Oct 21 2019 at 06:44):

If the hours of work which Mario put in just so we could have R[X]R[X] simultaneously being a module over both RR and R[X]R[X] ultimately taught us something then it would be good to somehow record this

Jeremy Avigad (Oct 21 2019 at 11:45):

Mario, one last question. You wrote "In short, you can give module the type module (R : out_param Type) {_: out_param (ring R)} (M : Type) : Type extends add_comm_group M, and then in theorems you use the binders {R : Type} {_ : ring R} {M : Type} [module R M]". What does marking an ordinary implicit argument as out_param do? I thought out_param only has an effect on variables marked for class inference.

Sebastien Gouezel (Oct 21 2019 at 11:58):

More general question: is there any documentation on the current behavior of out_param anywhere?

Patrick Massot (Oct 21 2019 at 12:03):

Of course there is! You can start with https://github.com/leanprover/lean/search?q=is_class_out_param&unscoped_q=is_class_out_param

Mario Carneiro (Oct 21 2019 at 12:22):

@Jeremy Avigad I might be misremembering, as I haven't had occasion to use it in a while, but I believe it starts out the search with a metavariable even if you give it a value (i.e. it searches for module ? ? M inst_M instead of module R ? M inst_M)

Sebastian Ullrich (Oct 21 2019 at 17:52):

Yes, it allows typeclass inference to start even when the corresponding argument still contains metavariables, then replaces that argument with a temporary metavariable for the search (so that it really is only an output of the search), and finally unifies inferred and given argument values. It does not influence the actual search.

Last updated: Aug 03 2023 at 10:10 UTC