GADT против MultiParamTypeClasses

Я пытаюсь понять GADTs, и я рассмотрел пример GADT в руководстве GHC. Насколько я могу судить, можно сделать то же самое с MultiParamTypeClasses:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
    FlexibleInstances, UndecidableInstances #-}

class IsTerm a b | a -> b where
  eval :: a -> b

data IntTerm  = Lit Int
              | Succ IntTerm
data BoolTerm = IsZero IntTerm
data If p a   = If p a a
data Pair a b = Pair a b

instance IsTerm IntTerm Int where
  eval (Lit i)      = i
  eval (Succ t)     = 1 + eval t

instance IsTerm BoolTerm Bool where
  eval (IsZero t)   = eval t == 0

instance (IsTerm p Bool, IsTerm a r) => IsTerm (If p a) r where
  eval (If b e1 e2) = if eval b then eval e1 else eval e2

instance (IsTerm a c, IsTerm b d) => IsTerm (Pair a b) (c, d) where
  eval (Pair e1 e2) = (eval e1, eval e2)

Обратите внимание, что у нас есть те же самые конструкторы и один и тот же код для eval (спрэд пересекает определения экземпляров), как в примере GHC GADTs.

Итак, что же все пух вокруг GADTs? Есть ли что-нибудь, что я могу сделать с GADTs, что я не могу сделать с MultiParamTypeClasses? Или они просто предоставляют более сжатый способ делать то, что я мог бы сделать с MultiParamTypeClasses вместо этого?

Ответ 1

Вы можете поместить значения GADT одного типа, но с различными конструкторами в контейнер удобно,

map eval [Lit 1, If (IsZero (Lit 3)) (Lit 4) (Succ (Lit 6))]

прост, но получить то же самое с использованием разных типов, а MPTC с функциональными зависимостями затруднительно. В вашем методе класса типа Multiparameter Lit и If являются конструкторами разных типов, поэтому для размещения их в одном контейнере нужен тип оболочки. Тип обертки, насколько я вижу, должен быть экзистенциальным типом à la

data Wrap t = forall a. (IsTerm a t) => Wrapper a

instance IsTerm (Wrap t) t where
    eval (Wrapper e) = eval e

чтобы обеспечить безопасность определенного типа и возможность map функционировать как eval над списком. Итак, вы на полпути или больше назад к GADT, минус удобство.

Я не уверен, что что-то GADT позволяет вам делать то, чего вы не можете достичь без них, но некоторые вещи пожертвовали бы много элегантности.

Ответ 2

GADTs просто позволяет вам предоставить более естественный способ определения конструктора и позволяет использовать сопоставление на уровне типа и конструкторах вместе (это то, что вы не можете обойтись без него, я думаю).

{-# LANGUAGE GADTs #-}
data Term a = (a ~ Bool) => IsZero (Term Int)
            | (a ~ Int) => Lit Int
eval :: Term a -> a
eval (IsZero t) = eval t == 0
eval (Lit a) = a