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.
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
)?
At one point, you need to test whether two things of different type are equal. There are two ways to do that:
Typeable
class.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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With