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

问题描述

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

  sceneRoot = proc inputs  - > （身份相机：&身份儿童）=输入
 returnA  - < （*）（map（rGet draw）children）。纯
  

我从ghc-7.6.3得到（很奇怪的）编译器错误

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

当我将模式放在 proc（...）模式。为什么是这样？

解决方案

考虑GADT

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

并执行代码

  foo :: S a  - > a  - >字符串
 foo s x = 
的案例s  - >>显示x 
  

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

如果我们执行

  foo undefined（\x :: Int  - > 4 :: Int）
  

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

现在考虑代码（让我们假装编译） p>

  bar :: S a  - > a  - >字符串
 bar sx =让S = s in show x 
  

以及执行 p>

  bar undefined（\x :: Int  - > 4 :: Int）
  

这应该怎么做？有人可能会认为它应该产生与 foo 相同的异常。如果是这种情况，那么参照透明度就意味着：

  let S = undefined :: S（Int-> Int）in show（\x :: Int  - > 4 :: Int）
  

失败同样的例外。这意味着 let 正在评估未定义的表达式，与
$非常不同b $ b

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

，它的计算结果为 5 。

确实， let 是 lazy ：它们不强制评估表达式，不像 case 。这就是为什么例如

  let（x，y）= undefined ::（Int，Char）in 5 
  

成功评估为 5 。

如果一个 e ，可能需要使 let S =在 e'中需要code> show ，但感觉很奇怪。另外，当评估时，让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屋！