encoding of modules

Stream: general

[Jeremy Avigad]

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

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]

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

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]

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]

Thanks, Johan. I'll pass that along.

[Jeremy Avigad]

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]

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

[Kevin Buzzard]

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]

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

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

that is, a module has only one base ring

[Mario Carneiro]

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]

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]

Thanks! That's really helpful.

[Kevin Buzzard]

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

[Jeremy Avigad]

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]

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

[Patrick Massot]

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]

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

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.