Is there a way to have multiple instances for bijective functional dependencies?

Question

I have a class with a bijective functional dependency:

class Add1 a b | a -> b , b -> a where
    add1 :: a -> b
    sub1 :: b -> a

and some other classes and data types:

class NonNegative a
class NonPositive a

data Succ a = Succ a
data Prev a = Prev a

If I try to define two instances:

instance NonNegative a => Add1 a (Succ a)
instance NonPositive a => Add1 (Prev a) a

I get the error:

    Functional dependencies conflict between instance declarations:
      instance NonNegative a => Add1 a (Succ a)
        -- Defined at BijectiveFD.hs:13:10
      instance NonPositive a => Add1 (Prev a) a
        -- Defined at BijectiveFD.hs:14:10
   |
13 | instance NonNegative a => Add1 a (Succ a)
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Either instance alone works fine. Is there some way to define both instances?

---

My full code is:

{-# LANGUAGE FunctionalDependencies #-}

class NonNegative a 
class NonPositive a

class Add1 a b | a -> b , b -> a where 
    add1 :: a -> b 
    add1 = u
    sub1 :: b -> a
    sub1 = u 
u = undefined

instance NonNegative a => Add1 a (Succ a) 
instance NonPositive a => Add1 (Prev a) a 

data Zero = Zero 

instance NonNegative Zero
instance NonPositive Zero

data Succ a = Succ a
data Prev a = Prev a

instance (NonNegative a) => NonNegative (Succ a)
instance (NonPositive a) => NonPositive (Prev a)

Answer 1

In Haskell, the instance declaration:

instance Foo a => Bar a

looks like it defines a Bar instance for every a with a Foo instance, but it doesn't. Instead, it defines a Bar instances for every possible a and additionally adds the requirement that, if you try to use that instance in a program, you'll also need a Foo instance.

This means that when you write:

instance NonNegative a => Add1 a (Succ a)
instance NonPositive a => Add1 (Prev a) a

you aren't defining instances only for types a that have NonNegative and NonPositive instances. You're defining instances for all types a, as if you'd written:

instance Add1 a (Succ a)       -- (1)
instance Add1 (Prev a) a       -- (2)

without the constraints. If you consider these constraint-less instances, you can see why there's a fundep conflict. The problem is that "every a" includes something like Prev Bool, so the first instance says that there's a specific instance:

instance Add1 (Prev Bool) (Succ (Prev Bool))   -- special case of (1)

while the second instance, when specialized to a ~ Bool, says that there's an instance:

instance Add1 (Prev Bool) Bool                 -- special case of (2)

These two instances conflict, because the first argument Prev Bool is supposed to uniquely determine the second argument, according to your fundeps, and that's not what's happening here.

What you could do instead is represent the NonNegative and NonPositive properties using a data type rather than a type class:

data NonNegative a = NonNegative a
data NonPositive a = NonPositive a

This allows you to write instances:

instance Add1 (NonNegative a) (NonNegative (Succ a))
instance Add1 (NonPositive (Prev a)) (NonPositive a)

with implementations that look like:

instance Add1 (NonNegative a) (NonNegative (Succ a)) where
  add1 (NonNegative x) = NonNegative (Succ x)
  sub1 (NonNegative (Succ x)) = NonNegative x
instance Add1 (NonPositive (Prev a)) (NonPositive a) where
  add1 (NonPositive (Prev x)) = NonPositive x
  sub1 (NonPositive x) = NonPositive (Prev x)

It's not clear if this is of much practical use, but I think it matches what you're trying to do in your code example.

Some code to illustrate the approach:

{-# LANGUAGE FunctionalDependencies #-}

class Add1 a b | a -> b , b -> a where
    add1 :: a -> b
    sub1 :: b -> a

data Zero = Zero                            deriving (Show)
data NonNegative a = NonNegative a          deriving (Show)
data NonPositive a = NonPositive a          deriving (Show)

data Succ a = Succ a                        deriving (Show)
data Prev a = Prev a                        deriving (Show)

instance Add1 (NonNegative a) (NonNegative (Succ a)) where
  add1 (NonNegative x) = NonNegative (Succ x)
  sub1 (NonNegative (Succ x)) = NonNegative x
instance Add1 (NonPositive (Prev a)) (NonPositive a) where
  add1 (NonPositive (Prev x)) = NonPositive x
  sub1 (NonPositive x) = NonPositive (Prev x)

main = do
  print $ sub1 . add1 . add1 . add1 $ NonNegative Zero
  print $ sub1 $ NonPositive Zero