GADTs和GADTSyntax之间的区别

Question

当我使用 GADT 语法定义一个新类型时，"普通"代数数据类型和广义代数数据类型之间有什么确切的区别？我认为这与所定义的数据构造函数的类型签名有关，但从未找到确切的定义。

此外，这种差异的后果是什么，为什么要显式启用 GADTs？我读到它们使类型推断变得不可判定，但为什么我们不能将类型构造函数视为具有该类型签名的函数，并将其插入推断算法中呢？

- pgmcr

Answer 1

正常的代数数据类型（无论是否在GADT语法中定义）上的模式匹配只会将值信息注入到主体中。对于GADT的模式匹配还可以注入类型信息。

例如，

data NonGADT a where
  Agnostic :: a -> NonGADT a

data GADT a where
  IntSpecific :: Int -> GADT Int
  CharSpecific :: Char -> GADT Char

所有这些构造函数在某种意义上具有相同的签名 a -> □ADT a，因此从类型检查器的角度来看，当对它们进行模式匹配时，编译器需要处理的就是这个签名。

extractNonGADT :: NonGADT a -> a
extractNonGADT v = case v of
   Agnostic x -> x

extractGADT :: GADT a -> a
extractGADT v = case v of
   IntSpecific x -> x
   CharSpecific x -> x

区别在于extractGADT可以利用内部类型实际上被限制为一个的事实，来执行类似以下的操作：

extractGADT' :: GADT a -> a
extractGADT' v = case v of
   IntSpecific x -> x + 5
   CharSpecific x -> toUpper x

一个标准的Hindley-Milner编译器无法处理这个问题：它会假设a在整个定义中是相同的。实际上，从技术上讲，在GHC中它也是相同的，只是代码的某些部分有额外的约束a ~ Int或a ~ Char。但是仅仅添加处理这些约束是不够的：这些额外的信息不能逃离作用域（因为它们是错误的），这需要进行额外的检查。

- leftaroundabout

---

关于Hindley-Milner部分：我是否正确理解HM不能统一x + 5和toUpper x的类型？ - pgmcr

是的。问题在于即使试图统一它们。 - leftaroundabout

注意，使用GADTs可以编写具有多个类型的术语，其中没有一个比其他更一般。有关更多信息，请参阅此问题。因此，我们不能指望完全进行类型推断。 - chi

Answer 2

区别在于返回类型的多态性。如果完全多态，您可以使用语法，但任何特殊化都需要 GADTs 语法。例如：

Foo :: Int -> Bar a b c

因为 a、b 和 c 都是不同的类型变量，所以这适用于 GADTSyntax 扩展。但如果你要写其中任何一个，你需要使用 GADTs。

Foo :: Int -> Bar Int b c
Foo :: Int -> Bar a b b
Foo :: Eq a => Int -> Bar a b c
-- (actually, ExistentialQuantification is enough for this last one, but GADTs also works)

由于这样的复杂类型，我们失去了项具有主类型的属性。您仍然可以使用标准类型推断，但有时它将不得不做出任意选择，这可能导致类型错误，即使一切都是类型安全的；为了避免这种情况，GHC简单地拒绝进行任意选择，并尽早报告错误。

- Daniel Wagner