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 (распространение по определениям экземпляров), что и в примере GADTs GHC.

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


haskell gadt
person user1078763    schedule 12.06.2012    source источник
comment
В вашем примере вы можете построить If (Lit 3) (IntTerm 1) (IntTerm 2). Рассмотрите возможность использования data If a = If BoolTerm a a.   -  person ony    schedule 12.06.2012
comment
GADT не предлагают ничего, что нельзя было бы смоделировать с помощью экзистенциальных типов и равенства типов. Но ваш конкретный пример не является примером этого.   -  person augustss    schedule 12.06.2012
comment
GADT закрываются во время определения, что может быть очень большой разницей.   -  person Ptharien's Flame    schedule 13.06.2012

Ответы (2)


arrow_upward
13
arrow_downward

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

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

прост, но получить то же самое, используя разные типы и MPTC с функциональными зависимостями, как минимум сложно. В вашем подходе к классу многопараметрического типа 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 можно сделать что-то такое, чего вы не смогли бы достичь без них, но некоторые вещи могут принести в жертву много элегантности.

person Daniel Fischer    schedule 12.06.2012

arrow_upward
0
arrow_downward

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
person ony    schedule 12.06.2012