奇怪的 ghc 错误消息，“我的大脑刚刚爆炸”？

Question

当我尝试以 proc 语法（使用 Netwire 和 Vinyl）对 GADT 进行模式匹配时：

sceneRoot = proc inputs -> do
            let (Identity camera :& Identity children) = inputs 
            returnA -< (<*>) (map (rGet draw) children) . pure

我收到了来自 ghc-7.6.3 的（相当奇怪的）编译器错误

我的大脑刚刚爆炸 我无法处理存在或 GADT 数据构造函数的模式绑定。 相反，使用 case-expression 或 do-notation 来解压缩构造函数。 在模式中： Identity cam :& Identity childs

当我将模式放入 proc (...) 模式时，我得到了类似的错误。为什么是这样？它是不健全的，还是只是未实现？

Answer 1

考虑 GADT

data S a where
  S :: Show a => S a

以及代码的执行

foo :: S a -> a -> String
foo s x = case s of
            S -> show x

在基于字典的 Haskell 实现中，人们会期望值 s 携带一个类字典，并且 case 从所述字典中提取 show 函数以便可以执行 show x。

如果我们执行

foo undefined (\x::Int -> 4::Int)

我们得到一个例外。在操作上，这是意料之中的，因为我们无法访问字典。 更一般地说，case (undefined :: T) of K -> ... 会产生错误，因为它会强制评估 undefined（前提是 T 不是 newtype）。

现在考虑代码（让我们假设它可以编译）

bar :: S a -> a -> String
bar s x = let S = s in show x

和执行

bar undefined (\x::Int -> 4::Int)

这应该怎么做？有人可能会争辩说它应该产生与foo 相同的异常。如果是这种情况，参考透明度将意味着

let S = undefined :: S (Int->Int) in show (\x::Int -> 4::Int)

同样失败。这意味着let 正在评估undefined 表达式，这与例如

let [] = undefined :: [Int] in 5

计算结果为5。

确实，let 中的模式是惰性：它们不会强制对表达式求值，这与case 不同。这就是为什么例如

let (x,y) = undefined :: (Int,Char) in 5

成功计算为5。

如果e' 中需要show，则可能想让let S = e in e' 评估e，但这感觉很奇怪。此外，在评估 let S = e1 ; S = e2 in show ... 时，不清楚是评估 e1、e2 还是两者兼而有之。

GHC 目前选择用一个简单的规则来禁止所有这些情况：消除 GADT 时没有惰性模式。