为什么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程序绝不应该是段错误的.