haskell - 为什么 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 程序不应该出现段错误。