Defining Eq instance for Haskell GADTs

16
votes

I have a GADT that's a lot like this:

data In a where
  M :: MVar a -> In a
  T :: TVar a -> In a
  F :: (a -> b) -> In a -> In b

It wraps various input primitives, but the last constructor also allows for a Functor instance:

instance Functor In where
  fmap f (F g v) = F (f . g) v
  fmap f x = F f x

The point of this type, BTW, is to support:

read :: In a -> IO a
read (M v) = takeMVar v
read (T v) = atomically (readTVar v)
read (F f v) = f <$> read v

What I want to be able to do is define the obvious Eq instance on this type, something like:

instance Eq (In a) where
  (M x) == (M y) = x == y
  (T x) == (T y) = x == y
  (F _ x) == (F _ y) = x == y
  _ == _ = False

The problem is the third case, which fails because x and y don't necessarily have the same type at that point. I understand that. In my own code I can make a long work-around, but it feels like there should be a way to define Eq directly. In my mind the solution is something like "keep drilling through the F constructors until you hit M or T, then if they're the same constructor (i.e. both M or both T) and same type, do the equality comparison", but I'm not sure how I could write that.

2
haskellgadt
Shouldn't x and y in line three of the EQ instance both have type In a - it would only be after application that their types diverge as the "b" of (a -> b) is an forall? That said, equality then seems ill-defined for this type because you are checking half the input to F rather than the output. - stephen tetley
I think you misread the type; the a is a forall, the b is the known type (is F :: (b -> a) -> In b -> In a clearer?). The equality is based on whether it's the same TVar/MVar, regardless of the pure function that might be applied to the result (I'll augment the question to explain the motivation). Which does actually mean that an In a and an In z could be equal; but still, I would like to define an Eq instance. - Neil Brown
Hi Neil - quite possibly I misunderstood the type, mentally I'd translate it to this F :: forall b. (a -> b) -> In a -> In b - is this right or wrong? - stephen tetley
It should be read as F :: forall a. (a -> b) -> In a -> In b The type used in the right-most item is the known type, all others are implicitly forall-ed (that's the intuition, not sure if it's always technically correct). - Neil Brown

2 Answers

11
votes

I'm highly suspicious about your equality since it only really tests half of the F, but if that's what you really want, here's how you can do it. Note that the cast serves as a test for type equality, since you can only compare the two Fs if the types of the existentially quantified a inside are the same.

data In a where
  M :: MVar a -> In a
  T :: TVar a -> In a
  F :: (Typeable a) => (a -> b) -> In a -> In b
  deriving (Typeable)


instance Eq (In a) where
  (M x) == (M y) = x == y
  (T x) == (T y) = x == y
  (F _ x) == (F _ y) = Just x == cast y
  _ == _ = False

Or maybe this isn't what you want either? Reading your motivation again it seems like you want a function where an In Int can be equal to an In Double.

How would you like these two to compare F floor r and F id r (if r is M x :: In Double)?

9
votes

At one point, you need to test whether two things of different type are equal. There are two ways to do that:

  1. The Typeable class.
  2. A GADT data Equal a b where Eq :: Equal a a.

Since MVar and TVar don't support 2, you will have to use the Typeable class. In other words, you will have to augment your data type with Typeable constraints.

Fortunately, you have some freedom as to where to put the constraints. For instance, you can put them as follows:

data In a where
    M :: Typeable a => MVar a -> In a
    T :: Typeable a => TVar a -> In a
    F :: (a -> b) -> In a -> In b

equal :: In a -> In b -> Bool
equal (M x) (M y)     = Just x == cast y
equal (T x) (T y)     = Just x == cast y
equal (F _ x) (F _ y) = x `equal` y
equal _ _             = False

instance Eq (In a) where
    (==) = equal

This way, you get to keep the Functor instance.