## Stream: maths

### Topic: definition of module

#### 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?

#### 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.

#### 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...

#### Scott Morrison (Jul 15 2020 at 04:12):

Oh, I guess that is nice.

#### 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.

#### Mario Carneiro (Jul 15 2020 at 12:56):

isn't that just not-@?

#### Johan Commelin (Jul 15 2020 at 12:57):

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

#### Johan Commelin (Jul 15 2020 at 12:58):

So that you don't need 25 _s

#### 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