Zulip Chat Archive

Stream: maths

Topic: definition of module


view this post on Zulip Kevin Buzzard (Jul 14 2020 at 20:57):

When Mario was formalising the definition of a module way back, we had all these out_params and complicated discussions between him and Sebastian about how difficult things were. Now we have

@[protect_proj] class semimodule (R : Type u) (M : Type v) [semiring R]
  [add_comm_monoid M] extends distrib_mul_action R M :=
(add_smul : (r s : R) (x : M), (r + s)  x = r  x + s  x)
(zero_smul : x : M, (0 : R)  x = 0)

and it looks beautiful. To me, the only thing that looks a bit weird about this definition now is that we have (M) before [semiring R]. Is that just irrelevant? Did all the out_param issues get completely resolved?

view this post on Zulip Scott Morrison (Jul 15 2020 at 00:42):

I agree that changing the order of the argument would be okay. I think historically there was a preference to put all the type arguments together first, then all the typeclass arguments. I prefer the other style.

view this post on Zulip Johan Commelin (Jul 15 2020 at 04:06):

The benefit of this style is that you can write @semimodule R M _ _ and you have to do less counting for how many _ you need before you can plug in a type again. But that's the only benefit I see...

view this post on Zulip Scott Morrison (Jul 15 2020 at 04:12):

Oh, I guess that is nice.

view this post on Zulip Oliver Nash (Jul 15 2020 at 07:49):

I have occasionally wondered if we could have a version of@ that tells the elaborator that we will fill in the explicit arguments but not the typeclass ones.

view this post on Zulip Mario Carneiro (Jul 15 2020 at 12:56):

isn't that just not-@?

view this post on Zulip Johan Commelin (Jul 15 2020 at 12:57):

No, I think the question is to get a trick to convert {} into (), but leave [] implicit

view this post on Zulip Johan Commelin (Jul 15 2020 at 12:58):

So that you don't need 25 _s

view this post on Zulip Oliver Nash (Jul 15 2020 at 13:23):

I should have said “implicit” rather than “explicit”. Interpreting me literally, @Mario Carneiro is completely right, but yes, I intended to communicate what @Johan Commelin has explained.


Last updated: May 12 2021 at 06:14 UTC