模式匹配中的评估顺序是否有任何保证？

Question

以下

(&&) :: Bool -> Bool -> Bool
False && _ = False
True && False = False
True && True = True

具有所需的短路属性 False && undefined ≡ False。第一个子句在正确的参数中是非严格的，保证在尝试其他任何事情之前进行检查。

显然，如果我更改顺序甚至取消函数化，它仍然有效

both :: (Bool,Bool) -> Bool
both (True,False) = False
both (True, True) = True
both (False, _) = False

Prelude> both (False, undefined)
False

但这真的有标准保证吗？与子句的顺序不同，模式的评估顺序在这里不是很清楚。我真的可以确定匹配 (True,False) 将在 (False,_) 确定后立即中止，然后再评估 snd 元素吗？

Answer 1

是的，保证对表达式 both (False, undefined) 的求值不会发散，因为数据构造函数的匹配保证从左到右匹配构造函数的组件，并且模式一旦出现某些错误就会失败子模式失败。由于元组的第一个元素是 False，一旦第一个元素不匹配，两个 (True, ...) 分支的模式都会失败。

根据 Haskell 2010 Report, section 3.17.2，给出了模式匹配的非正式语义：

Matching the pattern con pat1 … patn against a value, where con is a constructor defined by data, depends on the value:

If the value is of the form con v1 … vn, sub-patterns are matched left-to-right against the components of the data value; if all matches succeed, the overall match succeeds; the first to fail or diverge causes the overall match to fail or diverge, respectively.

If the value is of the form con′ v1 … vm, where con is a different constructor to con′, the match fails.

If the value is ⊥, the match diverges.

由于元组语法只是数据构造函数的一种特例语法糖，因此上述内容适用。

有关模式匹配的更完整处理，请参阅 section 3.17.3 of the Haskell 2010 Report，它给出了模式匹配的形式语义（具体而言，图 3.2 属于此问题）。

另一个感兴趣的资源是论文Pattern-driven Reduction in Haskell，它指定语义作为Haskell具体语法（the function mP in figure 3, page 7 is relevant to the question).

模式匹配中的评估顺序是否有任何保证？

Is there any guarantee about the evaluation order within a pattern match?

haskell

pattern-matching

strictness