Writing an instance of Eq for Fix (Haskell)

Question

I'm using Fix to define some datatypes for a project I'm working on. I need those datatypes to be instances of the equality typeclass Eq for unit testing. I'm stumped on how to write an instance of Eq for Fix or more specifically List defined in terms of Fix.

My Fix:

-- Fixed point of a Functor  
newtype Fix f = In (f (Fix f))                                                               
                                                                                             
out :: Fix f -> f (Fix f)                                                                    
out (In f) = f  

My List in terms of Fix:

data ListF a r = NilF | ConsF a r 

instance Functor (ListF a) where                                                          
       fmap _ NilF = NilF                                                                
       fmap f (ConsF a r) = ConsF a (f r)                                                
                                                                                            
type ListF' a = Fix (ListF a) 

Answer 1

@chi's answer is great but gives you a Show instance instead of an Eq instance.

Writing an Eq instance directly for ListF' is actually pretty straightforward. You were probably just overthinking it:

instance Eq a => Eq (ListF' a) where
  In (ConsF a as) == In (ConsF b bs) | a == b, as == bs      = True
  In NilF         == In NilF                                 = True
  In _            == In _                                    = False

You can stop there, but if you factor out the newtype unwrapping:

instance Eq a => Eq (ListF' a) where
  In f == In g = eqListF f g
    where eqListF (ConsF a as) (ConsF b bs) | a == b, as == bs      = True
          eqListF NilF         NilF                                 = True
          eqListF _            _                                    = False

and turn eqListF into an instance:

instance Eq a => Eq (ListF' a) where
  In f == In g = f == g

instance (Eq a, Eq r) => Eq (ListF a r) where
  ConsF a as == ConsF b bs | a == b, as == bs      = True
  NilF       == NilF                               = True
  _          == _                                  = False

it starts to become clearer how you get to a "generic" solution (for Fix f), though it's tough to figure this out unless you've already seen Eq1 somewhere.

class Eq1 f where
  liftEq :: (a -> a -> Bool) -> (f a -> f a -> Bool)
instance Eq1 f => Eq (Fix f) where
  In f == In g = liftEq (==) f g

instance (Eq a) => Eq1 (ListF a) where
  liftEq (===) (ConsF a as) (ConsF b bs) | a == b, as === bs   = True
  liftEq _     NilF         NilF                               = True
  liftEq _     _            _                                  = False

Note that the === in the third-last line is bound to the == being lifted by liftEq.

As per @chi's answer, it's actually possible to avoid using the awkward Eq1 instance by taking advantage of the relatively new QuantifiedConstraints extension. The rewritten instances look like this, and the Eq instance for ListF is much more natural than the Eq1 instance above:

instance (forall a. Eq a => Eq (f a)) => Eq (Fix f) where
  In f == In g = f == g

instance (Eq a, Eq l) => Eq (ListF a l) where
  ConsF a as == ConsF b bs | a == b, as == bs   = True
  NilF       == NilF                            = True
  _          == _                               = False

Update: And, as per @DanielWagner's comment, the compiler can do all this for you. If you derive the Eq instance for ListF in the usual manner:

data ListF a r = NilF | ConsF a r deriving (Eq)

then with StandaloneDeriving, the compiler will derive the Eq instance for ListF' a directly:

{-# LANGUAGE StandaloneDeriving #-}
deriving instance Eq a => Eq (ListF' a)

and, what's more remarkable, it will derive the general case:

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
deriving instance (Eq (f (Fix f))) => Eq (Fix f)

without requiring any additional instances.

Here's full code for the fully manual versions, first using the traditional Eq1 approach (and taking the class Eq1 from Data.Functor.Classes).

{-# LANGUAGE FlexibleInstances #-}

import Data.Functor.Classes

newtype Fix f = In { out :: f (Fix f) }

data ListF a r = NilF | ConsF a r
type ListF' a = Fix (ListF a)

instance Eq1 f => Eq (Fix f) where
  In f == In g = liftEq (==) f g

instance (Eq a) => Eq1 (ListF a) where
  liftEq (===) (ConsF a as) (ConsF b bs) | a == b, as === bs    = True
  liftEq _     NilF         NilF                               = True
  liftEq _     _            _                                  = False

consF a b = In (ConsF a b)
nilF = In NilF

main = do
  print $ nilF == (nilF :: ListF' Char)
  print $ consF 'a' nilF == consF 'a' nilF
  print $ consF 'a' nilF == consF 'b' nilF
  print $ consF 'a' nilF == consF 'a' (consF 'b' nilF)

then using the QuantifiedConstraints version:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Functor.Classes

newtype Fix f = In { out :: f (Fix f) }

data ListF a r = NilF | ConsF a r
type ListF' a = Fix (ListF a)

instance (forall a. Eq a => Eq (f a)) => Eq (Fix f) where
  In f == In g = f == g

instance (Eq a, Eq l) => Eq (ListF a l) where
  ConsF a as == ConsF b bs | a == b, as == bs   = True
  NilF       == NilF                            = True
  _          == _                               = False

consF a b = In (ConsF a b)
nilF = In NilF

main = do
  print $ nilF == (nilF :: ListF' Char)
  print $ consF 'a' nilF == consF 'a' nilF
  print $ consF 'a' nilF == consF 'b' nilF
  print $ consF 'a' nilF == consF 'a' (consF 'b' nilF)

and finally the compiler-derived version.

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Functor.Classes

newtype Fix f = In { out :: f (Fix f) }

data ListF a r = NilF | ConsF a r deriving (Eq)
type ListF' a = Fix (ListF a)

deriving instance (Eq (f (Fix f))) => Eq (Fix f)

consF a b = In (ConsF a b)
nilF = In NilF

main = do
  print $ nilF == (nilF :: ListF' Char)
  print $ consF 'a' nilF == consF 'a' nilF
  print $ consF 'a' nilF == consF 'b' nilF
  print $ consF 'a' nilF == consF 'a' (consF 'b' nilF)