问题描述
当我尝试以 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 错误消息，“我的大脑刚刚爆炸了"?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，WP2