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
[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
(), but leave
Johan Commelin (Jul 15 2020 at 12:58):
So that you don't need 25
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