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

Question

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

{-# Language PatternSynonyms #-}

pattern x := y <- x @ y

这允许我一次在一个参数上运行多个模式匹配。常规的 as 绑定 ( @) 不允许左侧成为模式，但可以。

有了这个我做了以下玩具功能

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

我确信这不是实现这一点的最佳方法，但它是有关行为的最小工作示例。

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

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

>>> f []
[]

另一种模式可以阻止它！好吧，如果我按照其他顺序执行它们，那么它应该会中断，对吗？

>>> f []
[]

>>> f' []
[]

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

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

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

不……没有。这失败了。不管错误在哪一边，都会(_:_)以某种方式阻止错误。也许 ghc 更喜欢在视图模式之前匹配解构模式？为了测试这一点，我可以将模式替换(_:_)为(reverse -> _:_). 这样它必须先运行一个函数才能进行解构。

但经过测试，新模式并没有改变行为。这个假设可以被排除。

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

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

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

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

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

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

>>> f []
[]

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

那么懒惰假设似乎有道理？这对我来说仍然非常不透明，我希望有一个对 ghc 内部结构有更多经验的人来证实这个假设。

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

非常感谢 Discord 用户 lexi。到目前为止，他们对诊断有很大帮助。

Answer 1

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

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

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

懒惰带来f undefined回报42。这是因为变量模式x不需要对参数进行求值，因此undefined从来不需要。

相比之下，如果我们使用

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

thenf undefined会崩溃，因为该模式()要求对参数进行求值，直到它暴露()构造函数（在本例中，这意味着完全求值）。

相似地，

f :: String -> Int
f x = 42

将导致f undefined返回42，同时

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

在尝试评估so 以公开第一个列表构造函数（ 或）后，将导致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"大致是这样完成的：

• 评估输入值x直到 WHNF（公开其第一个构造函数）
  • 如果是[]，则失败
  • 如果是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"。由于我们调用fwith []，因此没有尝试视图模式，因此它不会崩溃。调用f "a"将改为 match x:_，尝试视图模式并崩溃。