Zulip Chat Archive

Stream: general

Topic: Parameter implicitness in `derive` handlers

Eric Wieser (Oct 15 2020 at 09:12):

When I do

variables (G : Type*) (k : Type*) [semiring k]

@[derive [inhabited, add_comm_monoid]]
def add_monoid_algebra := G →₀ k

this results in a definition add_monoid_algebra.inhabited : Π (k : Type ?) (G : Type ?) [_inst_1 : semiring k], inhabited (add_monoid_algebra k G). Can derive be told to put k and G in {}?

Floris van Doorn (Oct 15 2020 at 19:23):

It probably could. Is that desirable? Since it's an instance, it won't be called to often manually, and I'm not sure if the heuristic "make all arguments implicit" is better than "use the same explicitness as in the main declaration".

Eric Wieser (Oct 15 2020 at 19:51):

In this case, it's because all the manual instances in the file use implicit parameters, so it feels inconsistent to switch them to derived instances

Eric Wieser (Oct 15 2020 at 19:52):

Frankly it feels like mathlib should have a convention for arguments to instances, and derive should match whatever that conclusion is

Floris van Doorn (Oct 15 2020 at 19:55):

Instances are almost never be written explicitly, so it tends to not matter whether the arguments are explicit. I have no good intuition whether I would want arguments explicit or implicit. My guess would be "explicit, unless a later argument depends on it."

Mario Carneiro (Oct 15 2020 at 19:59):

I generally try to use explicit arguments for instances, although they often inherit implicit from the variables declaration and it's not a big deal like Floris said. The primary advantage of being explicit is that it's easier to see what's going on when you print them out

Mario Carneiro (Oct 15 2020 at 20:00):

also it's generally less typing if for whatever reason you need to specify a typeclass instance

Last updated: Aug 03 2023 at 10:10 UTC