14

我正在努力掌握GADTs,并且我查看了GHC 手册中的GADT 示例。据我所知,可以用以下方法做同样的事情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)

请注意,我们有与 GHC 示例中完全相同的构造函数和完全相同的代码eval(跨实例定义传播)GADTs

那么所有的绒毛是GADTs什么?有什么我可以做而GADTs我不能做的事情MultiParamTypeClasses吗?还是他们只是提供了一种更简洁的方式来做我可以做的事情MultiParamTypeClasses

4

2 回答 2

13

您可以方便地将相同类型但具有不同构造函数的 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 是否允许您做任何没有它们您无法实现的事情,但有些事情会牺牲很多优雅。

于 2012-06-12T10:49:39.357 回答
0

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
于 2012-06-12T12:53:45.017 回答