如何用GADT进行存在量化？

Question

我有以下数据类型:

{-# LANGUAGE ExistentialQuantification #-}

data ExType = forall a. One a | forall a. Two a | forall a. Three a

有了这个,我就能够创建异构列表:

[One 3, Two "hello", One 'G']

有人告诉我,GADT是实现这一目标的新方法.GADT可以隐含地做我上面要做的事情.到目前为止,我还没有能够使用GADT创建一个允许我进行异构列表的类型.我该怎么做呢？

谢谢

Answer 1

通常,具有多态构造函数的GADT将具有类型参数,以便您可以知道在构造它时使用的类型,例如:

{-# LANGUAGE GADTs #-}
data Value a where
  Str :: String -> ExType String
  Number :: Int -> ExType Int
  Other :: a -> ExType a

然而,存在类型所做的关键是掩埋这种类型,这样你就无法知道a它是用什么构造的,只是a存在它所包含的某种类型.因此,只需从类型构造函数中删除type参数,然后从数据构造函数的结果类型中删除.

{-# LANGUAGE GADTs #-}
data ExType where
  One :: a -> ExType
  Two :: a -> ExType
  Three :: a -> ExType

foo :: [ExType]
foo = [One 3, Two "hello", One 'G']

Answer 2

我不知道GADT是否是新的黑色 - 但这是你使用这种语法的例子.

{-# LANGUAGE ExplicitForAll     #-}
{-# LANGUAGE GADTs              #-}

data ExType where
  One :: forall a. a -> ExType
  Two :: forall a. a -> ExType
  Three :: forall a. a -> ExType

lst :: [ExType]
lst = [One 3, Two "hello", Three 'A']

请注意,最好使用GADT的派生实例{-# LANGUAGE StandaloneDeriving #-},但即使是基本的东西Eq也会因为约束而无效forall a.