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

Question

今天，在与存在 GADT 构造函数进行匹配时尝试使用惰性模式时，我遇到了编译器错误：

存在或 GADT 数据构造函数不能在惰性 （~） 模式中使用

为什么会有这种限制？如果允许，会发生什么"坏"的事情？

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

然后是崩溃，而不是您在尝试头部规范化undefined时遇到的更优雅的失败。

GADT 数据代表有关类型的证据，因此伪造的 GADT 数据会威胁到类型安全。有必要严格要求他们来验证证据：你不能相信在底部存在的情况下未评估的计算。

Answer 2

对于"正常"数据，您可以在模式匹配期间跳过检查构造函数，前提是当您尝试使用模式中的数据时，它可能不存在，从而向您抛出异常。

使用 GADT 时，类型签名可能会根据存在的构造函数而更改。我们需要在编译时了解类型;在需要值之前不检查构造函数是不好的。如果这样做，则可能会出现类型不匹配错误。这可能意味着您的程序因分段错误（或更糟）而崩溃。Haskell程序永远不应该出现段错误。