为什么我的模式会阻止两侧的错误

Question

为了开始这整个事情，我正在使用一个模式同义词，定义如下：

{-# Language PatternSynonyms #-}
pattern x := y <- x @ y

这允许我一次跨参数运行多个模式匹配。 正则绑定(@)不允许左手边成为模式，但这确实如此。

有了这个，我使以下玩具功能

{-# Language ViewPatterns #-}
f ((_:_) := (head -> y)) =
[ y ]
f [] =
[]

我敢肯定，这不是实现这一点的最佳方式，但它是相关行为的最小工作示例。

这有一个接受单个参数的函数。 它使用定义的同义词将参数与两个模式进行匹配。 第一种模式匹配任何非空列表，并且不进行绑定。 第二个在列表上运行 head 函数，并将y绑定到结果。

所以问题是head会导致错误还是其他模式会阻止它？

>>> f []
[]

另一种模式阻止它！好吧，如果我以其他顺序执行它们，那么它应该会损坏吗？

f' ((head -> y) := (_:_)) =
[ y ]
f' [] =
[]

>>> f' []
[]

不！它仍然有效。 所以现在我的问题是：第二种模式有什么作用吗？ 也许视图模式具有某种智能行为，它调用函数并在发生错误时使模式失败......

f'' (head -> y) =
[ y ]
f'' [] =
[]

>>> f'' []
[*** Exception: Prelude.head: empty list

不。。。其实不然。 此操作失败。 不知何故，无论错误在哪一边，(_:_)都会阻止错误。 也许 ghc 更喜欢在视图模式之前匹配解构模式？ 为了测试这一点，我可以将模式(_:_)替换为(reverse -> _:_)。 这样，它必须先运行一个函数，然后才能进行解构。

但是经过测试后，新模式不会改变行为。可以排除这种假设。

所以也许是懒惰？ 如果列表为空，则无法评估x，因此它位于 thunk 中并且永远不会发生错误。 似乎有些情况。 如果我用(undefined -> x)替换(head -> x)，我们的行为就不会改变。

但是，如果我将其替换为(undefined -> "yo")：

f ((undefined -> "yo") := (x:_)) = [x]
f [] = []

>>> f []
*** Exception: Prelude.undefined

undefined确实会得到评估。 这似乎表明该模式正在迫使评估与"yo"进行比较。 如果我现在切换顺序：

f ((x:_) := (undefined -> "yo")) = [x]
f [] = []

>>> f []
[]

它不会被评估。 看来现在我们正在短路模式匹配。

所以懒惰假说似乎有意义吗？ 这对我来说仍然非常不透明，我希望有人对ghc的内部结构有更多经验来证实这个假设。

所以我的问题是现在发生了什么？ 是懒惰吗？ 它是如何工作的？

非常感谢不和谐的用户 lexi。到目前为止，他们在诊断中帮助很大。

Answer 1

你确实在观察懒惰的影响。

让我们从一个更基本的例子开始：

f :: () -> Int
f x = 42

懒惰使f undefined回归42.这是因为变量模式x不需要计算参数，因此从不要求undefined。

相比之下，如果我们使用

f :: () -> Int
f () = 42

然后f undefined确实崩溃了，因为模式()要求计算参数，直到它公开()构造函数(在这种情况下，这意味着完全评估)。

同样地

f :: String -> Int
f x = 42

将导致f undefined返回42，而

f :: String -> Int
f (x:xs) = 42

将导致f undefined崩溃，在尝试评估undefined以公开第一个列表构造函数(:或[])。

我们也有

f :: String -> Int
f "yo" = 42
f x    = 0

使f undefined崩溃：毕竟模式"yo"意味着('y':'o':[])所以它会强制undefined，试图将其与第一个:相匹配。更详细地说，以下所有调用都将崩溃：

f undefined
f (undefined:anything)
f ('y':undefined)
f ('y':undefined:anything)
f ('y':'o':undefined)

在这里，anything可以根据需要undefined或任何其他字符串/字符。

相比之下，以下所有调用都将返回0，因为定义中的第一个模式无法匹配(不会崩溃！

f []
f ('a':anything)
f ('y':'a':anything)
f ('y':'o':anything:anything)

同样，anything可以根据需要undefined或任何其他字符串/字符。

这是因为"yo"的模式匹配大致是这样完成的：

• xWHNF 之前评估输入值(公开其第一个构造函数)
  • 如果是[]，则失败
  • 如果y:ys，则评估y直到 WHNF
    • 如果y是'y'以外的另一个字符，则失败
    • 如果y'y'，则评估ys直到 WHNF
      • 如果是"[]"，则失败
      • 如果是z:zs，则z评估直到 WHNF
        • 如果z是'o'以外的另一个字符，则失败
        • 如果z'o'，则评估zs直到 WHNF
          • 如果是[]，那就成功！！
          • 如果h:hs，则失败

请注意，在每个"评估..直到WHNF"点中，我们可能会因为底部而崩溃(或陷入无限计算)。

本质上，模式匹配从左到右进行并停止，仅根据需要评估输入，并在知道结果(失败/成功)后立即停止。这不一定会强制对输入进行全面评估。在失败时，如果我们发现早期故障点，我们甚至不一定评估输入与模式一样深。当你写的时候，这确实是发生的情况：

看来现在我们正在短路模式匹配。

现在，视图模式遵循相同的原则。模式undefined -> x不会评估输入undefined，因为x不需要知道undefined的结果即可成功。相反undefined -> x:xs、undefined -> []和undefined -> "yo"确实需要知道结果，因此他们会根据需要对其进行评估。

关于您的示例：

f ((_:_) := (head -> y))

在这里，head -> y总是成功的。就其本身而言，它可以将y绑定到底部值，但这可以通过最左侧的_:_模式阻止。

f' ((head -> y) := (_:_))

在这里，head -> y总是成功的。就其本身而言，它会将y绑定到底部值，如果输入[]，这实际上会发生，但这不会强制输入，因此到目前为止没有导致崩溃。之后，我们尝试最左边的_:_模式，但失败了。结果：失败，但没有崩溃。

f'' (head -> y) = [ y ]

同样，head -> y总是成功，并将y绑定到底部(如果输入[])。模式匹配将成功，f''的结果[ head [] ]。例如，我们可以获取此列表的长度，但我们不能在不崩溃的情况下打印其内容。

f ((undefined -> "yo") := (x:_)) = [x]
f [] = []

如上所述，undefined -> "yo"崩溃。从未尝试过x:_模式。

f ((x:_) := (undefined -> "yo")) = [x]

在这里，我们首先匹配x:_，只有当成功时，我们才会尝试undefined -> "yo".由于我们调用f[]，视图模式没有尝试，所以它不会崩溃。调用f "a"将改为匹配x:_，尝试视图模式并崩溃。