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

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

但这实际上是由标准保证的吗？与条款的顺序不同,模式的评估顺序在这里并不十分清楚.在确定snd元素之前,我是否可以确定匹配(True,False)将在(False,_)确定后立即中止？

Answer 1

是的,保证评估表达式both (False, undefined)不会发散,因为保证数据构造函数的匹配从左到右与构造函数的组件匹配,并且一旦某个子模式失败,模式就会失败.由于元组的第一个元素是False,(True, ...)只要第一个元素无法匹配,两个分支的模式就会失败.

根据Haskell 2010报告的3.17.2节,它给出了模式匹配的非正式语义:

5. 将模式con pat1 ... patn与值匹配,其中con是由数据定义的构造函数,取决于值:
   • 如果该值的形式为con v1 ... vn,则子模式从左到右与数据值的组件匹配; 如果所有匹配成功,则整体匹配成功; 第一个失败或分歧导致整体匹配失败或分歧.
   • 如果值的形式为con'v1 ... vm,其中con是与con'不同的构造函数,则匹配失败.
   • 如果值为⊥,则匹配发生偏差.

由于元组语法只是数据构造函数的特例语法糖,因此适用.

有关模式匹配的更全面处理,请参阅Haskell 2010报告的第3.17.3节,该报告给出了模式匹配的形式语义(具体来说,图3.2与此问题有关).

另一个感兴趣的资源是Haskell中的模式驱动减少,它将语义指定为Haskell具体语法的抽象语法表示的解释器(用Haskell编写)(mP图3中的函数,第7页与问题相关).