- A+

I was trying to implement Integers at the type level in Haskell. To start I implemented natural numbers with

`data Zero data Succ a `

I then extended this to the integers with

`data NegSucc a `

I decided to then create an `Increment`

class that would increment integers. Here is how I did that:

`{-# Language FunctionalDependencies #-} {-# Language UndecidableInstances #-} {-# Language MultiParamTypeClasses #-} {-# Language FlexibleInstances #-} import Prelude () -- Peano Naturals -- data Zero data Succ a class Peano a instance Peano Zero instance (Peano a) => Peano (Succ a) -- Integers -- data NegSucc a -- `NegSucc a` is -(a+1) so that 0 can only be expressed one way class Integer a instance (Peano a) => Integer a instance (Peano a) => Integer (NegSucc a) -- Arithmetic Operations -- class Increment a b | a -> b instance (Peano a) => Increment a (Succ a) instance Increment (NegSucc Zero) Zero instance (Peano a) => Increment (NegSucc (Succ a)) (NegSucc a) `

However when I run this GHC complains that `Functional dependencies conflict between instance declarations`

, and cites all three of my increment instances. This error doesn't make much sense to me, I don't see any conflict between the separate declarations. What confuses me even further is that if I change the first instance to two separate instances

`instance (Peano a) => Increment (Succ a) (Succ (Succ a)) instance Increment Zero (Succ Zero) `

The compiler stops complaining altogether. However the rules that define `Peano a`

tell me that these two things should be the same.

Why do I get a functional dependency conflict when I write the single line version but none when I write the two line version?

*This answer is an expansion of this comment, which lead me to understanding what was going on*

In Haskell type classes are an open class, this means that new instances of the class can be made after the declaration.

This means that we cannot infer that `NegSucc a`

is not a member of `Peano`

, because it is always possible that it could be declared one later.

`instance Peano (NegSucc a) `

Thus when the compiler sees

`instance (Peano a) => Increment a (Succ a) instance Increment (NegSucc Zero) Zero `

it cannot know that `NegSucc Zero`

will not be an instance of `Peano`

. If `NegSucc Zero`

is an instance of `Peano`

it would increment to both `Zero`

and `Succ (NegSucc Zero)`

, which is a functional dependency conflict. So we must throw an error. The same applies to

`instance (Peano a) => Increment (NegSucc (Succ a)) (NegSucc a) `

Here `(NegSucc (Succ a))`

could also be an instance of `Peano`

.

The reason it looks as if there is no conflict is that we implicitly assume that there are not other instances of `Peano`

than the ones that we know of. When I transformed the single instance to two new isntances I made that assumption formal.

In the new code

`instance (Peano a) => Increment (Succ a) (Succ (Succ a)) instance Increment Zero (Succ Zero) `

it is not possible to add anything to preexisting type classes to cause a type to match multiple conflicting instances.