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

Question

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?

Answer 1

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:

5. 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).