奇怪的 ghc 错误消息，“我的大脑刚刚爆炸了"? [英] Odd ghc error message, "My brain just exploded"?

问题描述

当我尝试以 proc 语法(使用 Netwire 和 Vinyl)对 GADT 进行模式匹配时:

sceneRoot = proc 输入 ->做让(身份相机:& 身份儿童)= 输入返回A-<(<*>) (map (rGet draw) children).纯的

我从 ghc-7.6.3 得到(相当奇怪的)编译器错误

<前>我的脑袋刚刚爆炸我无法处理存在或 GADT 数据构造函数的模式绑定.相反，使用 case-expression 或 do-notation 来解压缩构造函数.在模式中:身份凸轮:&身份孩子

当我将模式放入 proc (...) 模式时，我遇到了类似的错误.为什么是这样?它是不健全的，还是没有实施?

解决方案

考虑 GADT

data S a whereS :: 显示一个 =>萨

和代码的执行

foo :: S a ->->细绳foo s x = case sS->显示 x

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

如果我们执行

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

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

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

bar :: S a ->->细绳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/code>，但感觉很奇怪.此外，在评估 let S = e1 时；S = e2 in show ... 不清楚是否评估 e1、e2 或两者.

GHC 目前选择通过一个简单的规则禁止所有这些情况:消除 GADT 时没有惰性模式.

When I try to pattern-match a GADT in an proc syntax (with Netwire and Vinyl):

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

I get the (rather odd) compiler error, from ghc-7.6.3

  My brain just exploded
    I can't handle pattern bindings for existential or GADT data constructors.
    Instead, use a case-expression, or do-notation, to unpack the constructor.
    In the pattern: Identity cam :& Identity childs

I get a similar error when I put the pattern in the proc (...) pattern. Why is this? Is it unsound, or just unimplemented?

解决方案

Consider the GADT

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

and the execution of the code

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

In a dictionary-based Haskell implementation, one would expect that the value s is carrying a class dictionary, and that the case extracts the show function from said dictionary so that show x can be performed.

If we execute

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

we get an exception. Operationally, this is expected, because we can not access the dictionary. More in general, case (undefined :: T) of K -> ... is going to produce an error because it forces the evaluation of undefined (provided that T is not a newtype).

Consider now the code (let's pretend that this compiles)

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

and the execution of

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

What should this do? One might argue that it should generate the same exception as with foo. If this were the case, referential transparency would imply that

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

fails as well with the same exception. This would mean that the let is evaluating the undefined expression, very unlike e.g.

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

which evaluates to 5.

Indeed, the patterns in a let are lazy: they do not force the evaluation of the expression, unlike case. This is why e.g.

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

successfully evaluates to 5.

One might want to make let S = e in e' evaluate e if a show is needed in e', but it feels rather weird. Also, when evaluating let S = e1 ; S = e2 in show ... it would be unclear whether to evaluate e1, e2, or both.

GHC at the moment chooses to forbid all these cases with a simple rule: no lazy patterns when eliminating a GADT.

这篇关于奇怪的 ghc 错误消息，“我的大脑刚刚爆炸了"?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！