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.
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 toF
rather than the output. – stephen tetleyF :: (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 anIn a
and anIn z
could be equal; but still, I would like to define an Eq instance. – Neil BrownF :: forall b. (a -> b) -> In a -> In b
- is this right or wrong? – stephen tetleyF :: 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