Kenny Lau (Apr 21 2018 at 01:44):
Should we show that every group is inhabited? Should we generalize it to has_one and has_zero? Which one will ring choose?
Mario Carneiro (Apr 21 2018 at 02:03):
I'm inclined to say no.
inhabited is more of a programming notion, a way to acquire a "default" value when it doesn't matter what value is picked. The value has no semantic meaning, so it doesn't matter if one or zero is picked. But I don't think that a typeclass search for
inhabited should go on an algebraic quest to prove that it's an R-module just because that implies it's inhabited. It would be better to have the types themselves register as inhabited, to keep it simple.
Kenny Lau (Apr 21 2018 at 02:04):
Last updated: May 11 2021 at 12:15 UTC