如何使用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存在。因此，只需从其类型构造函数和数据构造函数的结果类型中删除类型参数即可。

{-# 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.