为Haskell GADT定义Eq实例

Question

我有一个很像这样的GADT:

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

它包装了各种输入原语,但最后一个构造函数也允许一个Functor实例:

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

这种类型的重点是BTW,它支持:

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

我想要做的是在这种类型上定义明显的Eq实例,例如:

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

问题是第三种情况,它失败了,因为x和y在那一点上不一定具有相同的类型.我明白那个.在我自己的代码中,我可以进行长时间的解决,但感觉应该有一种直接定义Eq的方法.在我看来,解决方案就像"继续钻进F构造函数直到你击中M或T,然后如果它们是相同的构造函数(即M或两者都是T)和相同的类型,进行相等比较",但我我不知道怎么写那个.

Answer 1

我对你的平等非常怀疑,因为它只测试了F的一半,但如果那是你真正想要的,那么你就是这样做的.注意,强制转换用作类型相等的测试,因为如果存在量化a内部的类型相同,则只能比较两个F.

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

或许这不是你想要的？再次阅读你的动机似乎你想要一个In Int可以等于一个的函数In Double.

你想怎么比较这两个F floor r和F id r(如果r是M x :: In Double)？

Answer 2

有一点,你需要测试两种不同类型的东西是否相等.有两种方法可以做到这一点:

1. 该Typeable班.
2. 一个GADT data Equal a b where Eq :: Equal a a.

由于MVar并且TVar不支持2,您必须使用Typeable该类.换句话说,您必须使用Typeable约束来扩充数据类型.

幸运的是,你可以自由地确定约束的位置.例如,您可以按如下方式放置它们:

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

这样,您就可以保留Functor实例.