Writing an instance of Eq for Fix (Haskell)-CodePudding

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)

CodePudding user response：

One possible approach is using undecidable instances to create "recursive instances", so to speak.

{-# LANGUAGE UndecidableInstances #-}

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

instance Show (f (Fix f)) => Show (Fix f) where
   showsPrec p (In x) = showParen (p > 10) $
      ("In "   ) . showsPrec 11 x

data ListF a r = NilF | ConsF a r 
    deriving Show

Above, we define showsPrec so to add parentheses only when needed. The magic number 10 corresponds to the application precedence level, and showParen conditionally adds parentheses.

Note that the functor must be declared with deriving Show for this to work.

Note the tricky constraint resolution here. When checking Show ListF', GHC reduces that to Show (Fix ListF), then to Show (ListF (Fix ListF)), then to Show (Fix ListF) again but now "ties the knot" and produces a "recursive instance" instead of getting stuck in an infinite loop.

Alternatively, QuantifiedConstraints also works, avoiding the instance-level recursion. (We still need undecidable instances, though.)

instance (forall a. Show a => Show (f a)) 
         => Show (Fix f) where
   showsPrec p (In x) = showParen (p > 10) $
      ("In "   ) . showsPrec 11 x

CodePudding user response：

@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

Anyway, here's full code, 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)

And here's 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)