Ambiguous type variables with Haskell functional dependencies

Question

I was playing around with the FunctionalDependencies-Extension of Haskell, along with MultiParamTypeClasses. I defined the following:

class Add a b c | a b -> c where
    (~+) :: a -> b -> c
    (~-) :: a -> b -> c
    neg :: a -> a
    zero :: a

which works fine (I've tried with instances for Int and Double with the ultimate goal of being able to add Int and Doubles without explicit conversion).

When I try to define default implementations for neg or (~-) like so:

class Add ...
    ...
    neg n = zero ~- n

GHCi (7.0.4) tells me the following:

Ambiguous type variables `a0', `b0', `c0' in the constraint:
  (Add a0 b0 c0) arising from a use of `zero'
Probable fix: add a type signature that fixes these type variable(s)
In the first argument of `(~-)', namely `zero'
In the expression: zero ~- n
In an equation for `neg': neg n = zero ~- n

Ambiguous type variable `a0' in the constraint:
  (Add a0 a a) arising from a use of `~-'
Probable fix: add a type signature that fixes these type variable(s)
In the expression: zero ~- n
In an equation for `neg': neg n = zero ~- n

I think I do understand the problem here. GHC does not know which zero to use, since it could be any zero yielding anything which in turn is fed into a ~- which we only know of, that it has an a in it's right argument and yields an a.

So how can I specify that it should be the zero from the very same instance, i.e. how can I express something like:

neg n = (zero :: Add a b c) ~- n

I think the a, b and c here are not the a b c form the surrounding class, but any a b and c, so how can I express a type which is a reference to the local type variables?

Answer 1

Pull neg and zero out into a superclass that only uses the one type:

class Zero a where
    neg :: a -> a
    zero :: a

class Zero a => Add a b c | a b -> c where
    (~+) :: a -> b -> c
    (~-) :: a -> b -> c

The point is that your way, zero :: Int could be the zero from Add Int Int Int, or the zero from Add Int Double Double, and there is no way to disambiguate between the two, regardless of whether you're referring to it from inside a default implementation or an instance declaration or normal code.

(You may object that the zero from Add Int Int Int and the zero from Add Int Double Double will have the same value, but the compiler can't know that someone isn't going to define Add Int Char Bool in a different module and give zero a different value there.)

By splitting the typeclass into two, we remove the ambiguity.

Answer 2

You cannot express the zero function as part of the Add class. All type variables in the class declaration must be encountered in the type declaration for each function of the class; otherwise, Haskell won't be able to decide which type instance to use because it is given too few constraints.

In other words, zero is not a property of the class you are modelling. You are basically saying: "For any three types a, b, c, there must exist a zero value for the type a", which makes no sense; you could pick any b and c and it would solve the problem, hence b and c are completely unusable, so if you have an Add Int Int Int or an Add Int (Maybe String) Boat, Haskell does not know which instance to prefer. You need to separate the property of negation and "zeroness" into a separate class(es) of types:

class Invertible a where
  invert :: a -> a

neg :: Invertible a => a -> a
neg = invert

class Zero a where
  zero :: a

class Add a b c | a b -> c where
  (~+) :: a -> b -> c
  (~-) :: a -> b -> c

I don't see why you would then even need the Invertible and Zero constraints in Add; you can always add numbers without knowing their zero value, can you not? Why express neg as a requirement for ~+; there are some numbers that should be addable without them being negatable (Natural numbers for instance)? Just keep the class concerns separate.