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

编程入门行业动态更新时间:2024-10-26 18:20:36

本文介绍了模式匹配中的评估顺序是否有任何保证？的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！问题描述

以下

（&&）：:: Bool - >布尔 - > Bool False&& _ = False True&& False = False True&& True = True

具有所需的短路特性 False&&未定义≡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，...）分支只要第一个元素不匹配。

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

将模式 con pat1 ... patn 与数值匹配，其中 con 是由数据定义的构造函数，具体取决于以下值：

如果值的形式为 con v1 ... vn ，则子模式会从数据的组件左对齐值;如果所有比赛都成功，整体比赛成功;第一个失败或分歧会导致整体匹配失败或分歧。

如果值的格式为 con'v1 ... vm ，其中con与 con'不同的构造函数，匹配失败。

如果值为⊥，则匹配发生变化。由于元组语法只是数据构造函数的特例语法糖，因此，以上都适用。
要更全面地处理模式匹配，请参阅 Haskell 2010 Report的第3.17.3节，它给出了模式匹配的正式语义（具体来说，图3.2与这个问题有关）。

另一个感兴趣的资源是模式Haskell的驱动减少，它指定了语义a （Haskell编写的）Haskell的具体语法的抽象语法表示（图3中的函数 mP ，与问题相关）。

The following
(&&) :: Bool -> Bool -> Bool False && _ = False True && False = False True && True = True
has the desired short-circuit property False && undefined ≡ False. The first clause, which is non-strict in the right argument, is guaranteed to be checked before anything else is tried.

Apparently, it still works if I change the order and even uncurry the function
both :: (Bool,Bool) -> Bool both (True,False) = False both (True, True) = True both (False, _) = False Prelude> both (False, undefined) False
but is this actually guaranteed by the standard? Unlike with the order of clauses, the order of evaluation of the patterns is not so clear here. Can I actually be sure that matching (True,False) will be aborted as soon as (False,_) is determined, before the snd element is evaluated at all?
解决方案
Yes, it is guaranteed that evaluating the expression both (False, undefined) will not diverge since matching on data constructors is guaranteed to match left-to-right against the components of the constructor and the pattern fails as soon as some sub-pattern fails. Since the first element of the tuple is False, the pattern will fail for both (True, ...) branches as soon as the first element fails to match.

Per the Haskell 2010 Report, section 3.17.2, which gives an informal semantics of pattern matching:
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.

Since the tuple syntax is just a special-case syntactic sugar for a data constructor, the above applies.

For a fuller treatment of pattern matching, see section 3.17.3 of the Haskell 2010 Report, which gives a formal semantics of pattern matching (specifically, figure 3.2 pertains to this question).

Another resource of interest is the paper Pattern-driven Reduction in Haskell which specifies the semantics as an interpreter (written in Haskell) of an abstract syntax representation of Haskell's concrete syntax (the function mP in figure 3, page 7 is relevant to the question).