GADT 和 GADTS 语法之间的差异

Question

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

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

Answer 1

普通代数数据类型（无论是否在 GADT 语法中定义）的模式匹配仅将值信息注入主体中。GADT 上的模式匹配还可以注入类型信息。

\n

例如，

\n

data NonGADT a where\n  Agnostic :: a -> NonGADT a\n\ndata GADT a where\n  IntSpecific :: Int -> GADT Int\n  CharSpecific :: Char -> GADT Char\n

\n

所有这些构造函数在某种意义上都具有相同的签名a -> \xe2\x96\xa1ADT a，因此编译器在对涉及它们的模式匹配的函数进行类型检查时需要使用先验的签名。

\n

extractNonGADT :: NonGADT a -> a\nextractNonGADT v = case v of\n   Agnostic x -> x\n\nextractGADT :: GADT a -> a\nextractGADT v = case v of\n   IntSpecific x -> x\n   CharSpecific x -> x\n

\n

不同之处在于，extractGADT可以利用内部类型实际上仅限于单一类型的事实来执行类似的操作

\n

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

\n

标准 Hindley-Milner 编译器无法处理此问题：它会假设a整个定义中的 处处相同。事实上，从技术上来说，GHC 中也到处都是相同的，只是代码的某些部分分别有额外的约束a ~ Int或a ~ Char范围。但为此添加处理还不够：不允许这些附加信息逃脱范围（因为它不是真的），这需要额外的检查。

\n