group.inhabited

Stream: general

[Kenny Lau]

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]

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]

ok