I came up with a typeclass definition for Group , but I found a counterexample type that is not really a group.
Here is a class definition and an instance that is a group ℤ₂:
class Group g where
iden :: g
op :: g -> g -> g
inv :: g -> g
data Z2T = Z0 | Z1
instance Group Z2T where
iden = Z0
Z0 `op` Z0 = Z0
Z0 `op` Z1 = Z1
Z1 `op` Z0 = Z1
Z1 `op` Z1 = Z0
inv Z0 = Z1
inv Z1 = Z0
However, these type signatures for are Groupnecessary but not sufficient for the type to really be a group, here is my counterexample that compiles:
data NotAGroup = N0 | N1
instance Group NotAGroup where
iden = N0
N0 `op` N0 = N0
N1 `op` N0 = N0
N0 `op` N1 = N0
N1 `op` N1 = N0
inv N0 = N0
inv N1 = N0
How can I code enough rules for a type that should be a group in a class Groupin Haskell?
source
share