GADT 和 GADTS 语法之间的区别

Question

当我使用 GADT 语法定义新类型时，“普通”代数数据类型和广义代数数据类型之间到底有什么区别？我认为这与定义的数据构造函数的类型签名有关，但永远找不到确切的定义。

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

Answer 1

区别在于返回类型的多态性。如果它是完全多态的，则可以使用该语法，但任何专门化都需要 GADT 语法。例如：

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 干脆拒绝做出这些任意选择，并尽早报告错误。

Answer 2

普通代数数据类型上的

模式匹配（无论它是否在 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

。但为此添加处理是不够的：决不能允许这些附加信息逃脱范围（因为它不会是真的），并且这需要额外的检查。