这种 GADT 的使用是否完全等同于存在类型？答案

【问题标题】：Is this use of GADTs fully equivalent to existential types?这种 GADT 的使用是否完全等同于存在类型？
【发布时间】：2018-03-05 14:31:27
【问题描述】：

data Foo = forall a. MkFoo a (a -> Bool)
         | Nil

可以轻松转换为 GADT：

data Foo where 
    MkFoo :: a -> (a -> Bool) -> Foo
    Nil :: Foo

它们之间有什么区别：代码可以编译但不能编译，或者给出不同的结果？

【问题讨论】：

【解决方案1】：

它们几乎是等价的，尽管不完全一样，具体取决于您打开的扩展程序。

首先，请注意，您无需启用GADTs 扩展即可将data .. where 语法用于存在类型。启用以下较小的扩展就足够了。

{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE ExistentialQuantification #-}

有了这些扩展，你就可以编译了

data U where
    U :: a -> (a -> String) -> U

foo :: U -> String
foo (U x f) = f x

g x = let h y = const y x
      in  (h True, h 'a')

如果我们用

替换扩展名和类型定义，上面的代码也可以编译

{-# LANGUAGE ExistentialQuantification #-}
data U = forall a . U a (a -> String)

然而，上面的代码不能在GADTs 扩展打开的情况下编译！这是因为GADTs 也开启了MonoLocalBinds 扩展，这使得g 的上述定义无法编译。这是因为后一个扩展阻止了h 接收多态类型。

【讨论】：

【解决方案2】：

来自the documentation：

请注意，GADT 风格的语法概括了存在类型（存在量化数据构造函数）。例如，这两个声明是等价的：
data Foo = forall a. MkFoo a (a -> Bool)
data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }

（强调对等词）

【讨论】：

【解决方案3】：

后者实际上不是 GADT - 它是一种使用 GADT 语法声明的存在量化数据类型。因此，它与前者相同。

它不是 GADT 的原因是没有类型变量可以根据构造函数的选择进行改进。这是 GADT 添加的关键新功能。如果您有这样的 GADT：

data Foo a where
    StringFoo :: String -> Foo String
    IntFoo :: Int -> Foo Int

然后，每个构造函数上的模式匹配揭示了可以在匹配子句中使用的附加信息。例如：

deconstructFoo :: Foo a -> a
deconstructFoo (StringFoo s) = "Hello! " ++ s ++ " is a String!"
deconstructFoo (IntFoo i)    = i * 3 + 1

请注意，从类型系统的角度来看，那里正在发生一些非常有趣的事情。 deconstructFoo 承诺它将适用于a 的任何选择，只要它传递了Foo a 类型的值。但是第一个等式返回一个String，第二个等式返回一个Int。

这是常规数据类型无法做到的，这是 GADT 提供的新功能。在第一个等式中，模式匹配将约束 (a ~ String) 添加到其上下文中。在第二个等式中，模式匹配添加了(a ~ Int)。

如果您尚未创建模式匹配可导致类型优化的类型，则您没有 GADT。您只需使用 GADT 语法声明的类型。这很好 - 在很多方面，它是比基本数据类型语法更好的语法。对于最简单的情况，它更冗长。

【讨论】：