为什么GADT/存在类型数据构造函数不能在惰性模式中使用？

Question

今天在尝试使用延迟模式匹配existential GADT构造函数时，我遇到了一个编译器错误:

存在类型或GADT数据构造函数不能在惰性(~)模式内使用

为什么有这个限制？如果允许使用会发生什么“糟糕”的事情？

- Petr

Answer 1

请考虑

data EQ a b where
  Refl :: EQ a a

如果我们能够定义

transport :: Eq a b -> a -> b
transport ~Refl a = a

那么我们就可以拥有

transport undefined :: a -> b

从而获得

transport undefined True = True :: Int -> Int

如果尝试对未定义的内容进行头部规范化，可能会导致崩溃，而不是更加优雅的失败。

GADT 数据表示关于类型的证据，因此虚假的 GADT 数据会威胁类型安全性。 必须对它们进行严格验证以验证这些证据：在底部存在的情况下，不能信任未求值的计算。

- pigworker

---

相比于等式约束，存在类型如何？ GHC 也不允许使用它们 - 它们是否也存在问题？ - shachaf

Answer 2

对于“正常”的数据，您可以在模式匹配期间跳过检查构造函数，理解当您尝试使用模式中的数据时，它可能不存在，因此会抛出异常。

使用GADT，类型签名取决于哪个构造函数存在。我们需要在编译时知道类型；直到需要值之前不检查构造函数是没有用的。如果这样做，您可能会遇到类型不匹配错误。而这可能意味着您的程序崩溃并出现分段错误（或更糟）。Haskell程序应该永远不会发生分段错误。

- MathematicalOrchid