Определение экземпляра Eq для GADT на Haskell - PullRequest
Новая
       13

Определение экземпляра Eq для GADT на Haskell

15 голосов
/ 17 мая 2011

У меня есть 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) и одного типа, сделайте сравнение на равенство», ноЯ не уверен, как я мог написать это.

Ответы [ 2 ]

11 голосов
/ 17 мая 2011

Я очень подозрительно отношусь к вашему равенству, поскольку он действительно проверяет только половину F, но если это то, что вы действительно хотите, вот как вы можете это сделать. Обратите внимание, что приведение служит тестом на равенство типов, поскольку вы можете сравнивать два F только в том случае, если типы экзистенциально количественно a внутри одинаковы. 

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

8 голосов
/ 17 мая 2011

В какой-то момент вам нужно проверить, равны ли две вещи разного типа.Есть два способа сделать это:

  1. Класс Typeable.
  2. A 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.

...