Is there a way to implement constraints in Haskell's type classes?

Question

Is there some way (any way) to implement constraints in type classes?

As an example of what I'm talking about, suppose I want to implement a Group as a type class. So a type would be a group if there are three functions:

class Group a where
    product :: a -> a -> a  
    inverse :: a -> a 
    identity :: a

But those are not any functions, but they must be related by some constraints. For example:

product a identity = a 
product a (inverse a) = identity
inverse identity = identity

etc...

Is there a way to enforce this kind of constraint in the definition of the class so that any instance would automatically inherit it? As an example, suppose I'd like to implement the C2 group, defined by:

 data C2 = E | C 

 instance Group C2 where
      identity = E 
      inverse C = E

This two definitions uniquely determines C2 (the constraints above define all possible operations - in fact, C2 is the only possible group with two elements because of the constraints). Is there a way to make this work?

Answer 1

Type classes can contain definitions as well as declarations. Example:

class Equality a where
    (?=), (!=) :: a -> a -> Bool

    a ?= b = not (a != b)
    a != b = not (a ?= b)

instance Eq a => Equality a where
    (?=) = (==)

test = (1 != 2)

You can also specify special constraints (let's call them laws) in plain Haskell, but it's not guaranteed that the compiler will use them. A common example are monadic laws

Answer 2

Is there a way to enforce this kind of constraint?

No. Lots of people have been asking for it, including the illustrious Tony Hoare, but nothing appears on the horizon yet.

This problem would be an excellent topic of discussion for the Haskell Prime group. If anyone has floated a good proposal, it is probably to be found there.

P.S. This is an important problem!

Answer 3

In some cases you can specify the properties using QuickCheck. This is not exactly enforcement, but it lets you provide generic tests that all instances should pass. For instance with Eq you might say:

prop_EqNeq x y = (x == y) == not (x != y)

Of course it is still up to the instance author to call this test.

Doing this for the monad laws would be interesting.