Specifying typeclasses for 'obvious' cases

Stream: new members

[Tom]

In addition to @Kyle Miller 's comment, I have a stupid question: Why does Lean insist on specifying type classes even for "obvious" cases? E.g. when I write +, Lean already knows I mean "HAdd"; and similar with e.g. OfNat. While I am ok and in general in favor of the "explicit is better than implicit" mantra, there are times when I can't think of any reason why things could be ambiguous (and e.g. Rust can figure out its traits!). Since there are no separate interface files (like e.g. in ML/OCaml), I don't see why those instances couldn't just be added automatically to the function signature based on the function body.

[Kyle Miller]

Maybe this would be better in a different thread? Are you asking "why can't Lean auto-add instance arguments?"

[Notification Bot]

2 messages were moved here from #new members > Why return type of partial function MUST inhabited? by Kyle Miller.

[Tom]

Happy to start another thread. It seems you were proposing to add some form of "Inhabited" by default, so my question seemed related.

[Tom]

Ah, I see you beat me to it, thanks. :smile:

[Kyle Miller]

The feature was to auto-derive instances from pre-existing instances, no automatic adding of new arguments.

[Tom]

I see; I guess my question is not "related" but stands on its own then.

[Kyle Miller]

For your question, it's similar to your questions from about a month ago: typeclasses aren't just constraints, and you can't just add in the extra arguments without breaking things.

[Kyle Miller]

For example, you might want your HAdd to come from a particular Field instance, not the random one added in because you used +

[Edward van de Meent]

Tom said:

E.g. when I write +, Lean already knows I mean "HAdd"; and similar with e.g. OfNat

because you often don't want HAdd, HMul, etc... you want something like Add, Mul, Group, Ring, etc... And detecting which of these is intended is nigh-impossible at best.