Constraints on a Haskell typeclass for the definition of a group

Question

I came up with this typeclass definition for a Group, but I found a counterexample type that is not actually a group.

Here is the class definition and an instance that is the 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, those type signatures for Group are necessary, but not sufficient for a type to really be a group, here's 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 encode the sufficient rules for a type to be a group in the Group typeclass in Haskell?

Answer 1

You are right that it is possible to write instances of the Group typeclass which violates the group laws, because in fact there's nothing in the code actually stating them.

This happens the same way for instance for the Monad class, where the monadic laws are not written nor enforced in any way. You can write an unlawful Monad instance, as you can write an unlawful Group instance.

This is actually the best you can get in Haskell, at least without increasing the complexity of the type signature too much. In fact, to express the group laws in the type you will probably need a fully dependently typed language, which Haskell is not.

In cases like this, laws are usually written in comments, maybe stated as rewrite rules, and programmers are usually disciplinate enough to respect them.