21

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

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 (...)。为什么是这样？它是不健全的，还是只是未实现？

4

1 回答 1

12

考虑 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不是 a newtype)。

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

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

和执行

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

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

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

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

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

评估为5。

事实上， a 中的模式let是惰性的：它们不强制对表达式求值，不像case. 这就是为什么例如

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

成功评估为5.

有人可能想let S = e in e'评估e是否show需要a e'，但感觉很奇怪。此外，在评估let S = e1 ; S = e2 in show ...时，是否评估e1、e2或两者都不清楚。

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

于 2014-05-08T11:25:55.857 回答