definition of module

Stream: maths

[Kevin Buzzard]

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]

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]

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]

Oh, I guess that is nice.

[Oliver Nash]

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]

isn't that just not-@?

[Johan Commelin]

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

[Johan Commelin]

So that you don't need 25 _s

[Oliver Nash]

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.