9

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

{-# Language PatternSynonyms #-}

pattern x := y <- x @ y

这允许我一次跨一个参数运行多个模式匹配。常规 as binding ( @) 不允许左侧成为模式，但确实如此。

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

{-# 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 中并且永远不会发生错误。似乎有些情况。如果我替换(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 的内部有更多经验来证实这个假设。

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

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

4

1 回答 1

2

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

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

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

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:_，尝试视图模式并崩溃。

于 2021-10-13T12:05:25.683 回答