如何用GADT进行存在量量化？
如何用GADT进行存在量量化？
提问于 2017-04-18 21:36:52
我有以下数据类型：
{-# 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创建一个允许我执行异构列表的类型。我该怎么做？
谢谢
回答 2
Stack Overflow用户
回答已采纳
发布于 2017-04-18 21:51:41
通常，具有多态构造函数的GADT具有一个类型参数，这样您就可以知道在构造它时使用了哪种类型，例如：
{-# LANGUAGE GADTs #-}
data Value a where
Str :: String -> ExType String
Number :: Int -> ExType Int
Other :: a -> ExType 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']Stack Overflow用户
发布于 2017-04-18 21:52:19
我不知道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.
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/43482610
复制相关文章
相似问题
腾讯云开发者
