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

下列

(&&) :: 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 元素之前就确定了？

是的，可以保证计算表达式both (False, undefined)不会发散，因为数据构造函数上的匹配保证从左到右与构造函数的组件匹配，并且一旦某些子模式失败，该模式就会失败。由于元组的第一个元素是False，该模式对于两者都会失败(True, ...)一旦第一个元素无法匹配就分支。

Per the Haskell 2010 报告，第 3.17.2 节 https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-600003.17.2，它给出了模式匹配的非正式语义：

5. Matching the pattern con pat1 … patn against a value, where con is a constructor defined by data, depends on the value:
   • 如果值的形式为con v1 … vn，子模式从左到右与数据值的组成部分进行匹配；如果所有匹配都成功，则整体匹配成功；第一个失败或发散会分别导致整个匹配失败或发散。
   • 如果值的形式为con′ v1 … vm，其中 con 是一个不同的构造函数con′，匹配失败。
   • 如果值为 ⊥，则匹配发散。

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

要更全面地处理模式匹配，请参阅Haskell 2010 报告第 3.17.3 节 https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-610003.17.3，它给出了模式匹配的形式语义（具体来说，图 3.2 属于这个问题）。

另一个有趣的资源是论文Haskell 中的模式驱动归约 http://programatica.cs.pdx.edu/P/journal-wrs2002.pdf它将语义指定为 Haskell 具体语法的抽象语法表示的解释器（用 Haskell 编写）（函数mP图 3 第 7 页与该问题相关）。