Defining Eq instance for Haskell GADTs

Question

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.

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, May 17 '11 at 09:36
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, May 17 '11 at 09:48
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, May 17 '11 at 10:02
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, May 17 '11 at 11:48

augustss · Accepted Answer · 2013-04-09T07:57:08.733

11

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)?

edited Apr 09 '13 at 07:57

answered May 17 '11 at 10:39

augustss

22,884
5
56
93

1

I want `F floor r == F id r` to be `True`. I really want Eq to be defined as: is the inner MVar/TVar the same between the two instances of `In a`. This means that I want `fmap f x == x` for all `f` (or at least, all `f :: a -> a`). Your method does get the most of the behaviour I want, but the `Typeable` constraint wipes out my `Functor` instance. – Neil Brown May 17 '11 at 11:46
1

So then you can't use `==` since it requires both arguments to have the same type. You need to write your own function which is more flexible. – augustss May 17 '11 at 13:19

score 9 · Answer 2 · answered May 17 '11 at 12:20

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

The Typeable class.
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.

Another option would be to make 'M' and 'T' carry an additional "unique" object such as an extra 'MVar ()' that was created at the same time, and test those objects for equality instead of the "real" ones. — mokus, May 19 '11 at 15:50
Mokus's suggestion is my long work-around, I just thought there might be an easier way. But both answers have convinced me that the "easy" way didn't really exist, as I hadn't thought it through enough. Thanks both for your help, I accepted one answer but both were useful. — Neil Brown, May 26 '11 at 14:09

Defining Eq instance for Haskell GADTs

2 Answers2