Zulip Chat Archive

Stream: general

Topic: group.inhabited


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:04):

ok


Last updated: May 11 2021 at 12:15 UTC