4  Lazy pattern matching

4.1  Lazy pattern matching in theory

In previous sections we only considered strict ML. In a strict language we can define ML pattern matching as a predicate operating on terms, which also are the values of program expressions. In other words, pattern matching apply to completely evaluated expressions, or normal forms.

Studying pattern matching in a lazy language such as Haskell requires a more sophisticated semantical setting. Essentially, lazy language manipulate values that are known partially and, more significant to our study, pattern matching operates on such incomplete values.

Definition 1 of the instance relation for patterns and values apply unchanged to partial values (we have _ ≼ Ω, value Ω possesses all types). Thus we keep the same notation ≼, and maintain Definition 3 of the instance relation for matrices.

However we cannot keep Definition 2 of ML pattern matching.

More generally, partial values and computation interact. Let us consider some expression e. If the root symbol of expression e is a constructor c, then expression e is a head-normal form and we express the “current value” of e as c(v₁,v₂, … ,v_a) — see Huet and Lévy [1991] for a more precise treatment in the context of term rewriting systems. Otherwise, the “current value” of expression e is Ω. Then, we consider various “current values” along the evaluation of e. As constructors cannot be reduced, those values are increasing according to the following precision ordering.

To be of practical use, a predicate P that defines pattern matching must be monotonic. That is, when P(v) holds, P(w) also holds for all w such that v ≼_Ωw. With monotonic predicates, matching decisions do not change during computations. One should notice that, given any pattern p, the predicate p ≼ v is monotonic in v. Example 3 shows that the predicate P ⋠v^→ is not monotonic in general.

We thus need a new definition of pattern matching. For the moment, we leave most of lazy pattern matching unspecified.

We call P the disambiguating predicate and now look for sufficient conditions on P that account for our intuition of pattern matching in a lazy language.

1. Pattern matching is deterministic, in the sense that at most one clause is matched. Hence, for all P and v^→, we assume:

   P(P,

   → v

   ) =⇒ P ⋠

   → v

   .

2. Matching the first row of a matrix reduces to the instance relation. Hence, for all v^→, we assume:

   P(∅,

   → v

   ) = True.

3. We require predicate P to be monotonic in its value component. That is, given any matrix P, for all value vectors v^→ and w^→, we assume:

   P(P,

   → v

   ) ∧

   → v

   ≼Ω

   → w

   =⇒ P(P,

   → w

   ).

The three conditions above are our basic restrictions on P. We further define U_P and M_P as U and M (Definition 6) parameterized by P.

Now, given a definition of lazy pattern matching, we face the temptation to assume that the computation of U described in Section 3.1 still works for U_P. More precisely, by finding additional sufficient conditions on predicate P we aim at proving U_P = U_rec. Thus, we re-examine the proof of Proposition 2 in the context of lazy pattern matching.

Base cases follow from basic restrictions.

1. By our first basic restriction and since ( ) ≼ (), we have P(( ), ()) = False. Thus we have U_P(( ), ()) = False.
2. By our second basic restriction, we directly get U_P(∅, q^→ ) = True.

To prove the inductive cases, it suffices to reformulate the key properties of Lemma 1, replacing P ⋠v^→ by P(P, v^→). However, key properties now are rather assumed than established.

It is not obvious that assuming key properties suffices to prove that U_P can be computed as U is, since Ω does not show in the proof of Proposition 2. Indeed, monotonicity plays some part here.

As an immediate consequence of the proposition above, the useless clause problem is now solved in the lazy case (see second item in Proposition 1). However, the exact formulation of exhaustiveness needs a slight change. Reconsider Example 3.

case e of True -> 1 | _ -> 2

By definition of ≼, True ≼ Ω does not hold, hence Ω cannot match first clause. However, P((

), Ω) does not hold either, by monotonicity. Hence, there is no row that filters value Ω and Definition 4 would flag this matching as non-exhaustive, a clear contradiction with our intuition of exhaustiveness. Thus, we now directly define an exhaustive matrix P from the condition U_P(P, (_⋯_)) = False. That is, P is exhaustive, if and only if for all vectors v^→, P(P, v^→) does not hold. By this new definition, the example is exhaustive: for any value v in {Ω,False, True}, we have _ ≺ v. Thus we have:

Hence, by our first basic restriction, for all v, P(P, v) does not hold.

4.2  Lazy pattern matching, à la Laville

Laville’s definition of lazy pattern matching Laville [1991] stems directly from the need of a monotonic P: if we decide that some term is evaluated enough not to match a pattern, then we want this to remain true when the term is evaluated further. By definition, matrix P and value v^→  are incompatible, written P #v^→ , when making v^→  more precise cannot produce an instance of P. That is, P #v^→  means

The first basic restriction follows by letting w^→ be v^→ in the definition of P #v^→, the second restriction follows from ∅ ⋠w^→ for all w^→, and monotonicity is a consequence of the transitivity of ≼_Ω.

Incompatibility is the most general P in the following sense: for any predicate P, any matrix and any value vector v^→, we have.

For, if P and v^→ are compatible (i.e. not incompatible), then there exists w^→, with v^→ ≼_Ωw^→ and P ≼ w^→. Thus, by the first basic restriction, P(P, w^→) does not hold, and, by the monotonicity of P, P(P, v^→) does not hold either.

Incompatibility is easily computed by the following rules.

It is routine to show that incompatibility meets key properties. Hence, by Proposition 3, algorithm U_rec is correct with respect to Laville’s semantics.

Laville’s definition is quite appealing as a good, implementation independent, definition of lazy pattern matching. However, there is a slight difficulty: predicate P #v^→ is not sequential in the sense of Kahn and Plotkin [1978] in v^→ for any matrix P. This means that its compilation on an ordinary, sequential, computer is problematic Maranget [1992], Sekar et al. [1992]. As a consequence, the Haskell committee adopted another semantics for pattern matching. Their definition is aware of the presence of Ω and solves the difficulty by specifying left-to-right testing order.

4.3  Pattern matching in Haskell

By interpreting the Haskell report Hudak et al. [1998] we can formulate a pattern matching predicate for this language. Matching can yield three different results: it may either succeed, fail or diverge. Furthermore, matching of arguments is performed left-to-right. We encode “success”, “failure” and “divergence” by the three values T, F and ⊥, and define the following H function.

Where the extended (left-to-right) boolean connectors are defined as follows.

We ignore some of Haskell patterns such as irrefutable patterns. We also ignore or-patterns at the moment. From this definition one easily shows the following two properties on vectors:

We then interpret the many program equivalences of section 3.17.3 in the Haskell report as expressing a downward search for a pattern of which v^→ is an instance of:

Informally, H(P, v^→ ) = T means “v^→ is found to match some row in P in the Haskell way”, H(P, v^→ ) = F means “no row of P is found to be matched”, and H(P, v^→ ) = ⊥ means “v^→ is not precise enough to make a clear decision”. We can now formulate the Haskell way of pattern matching in our setting.

One easily checks that predicate H(P, v^→ ) = F meets all basic restrictions and key properties (decomposing along first columns is instrumental). Hence, save for or-patterns, algorithm U_rec also computes the utility of pattern matching in Haskell.

4.4  Or-patterns in Haskell

As this work is partly dedicated to specific warnings for or-patterns, we wish to enrich Haskell matching with or-patterns. The H function is extended to consider or-patterns, sticking to left-to-right bias:

Semantical consequences are non-negligible, since the equivalence H(p^→, v^→ ) = T  ⇐⇒ p^→ ≼ v^→ does not hold any more, as can be seen by considering H((True∣_), Ω) = ⊥.

However, the left-to-right implication still holds, and the following definition of Haskell pattern matching makes sense.

The definition above is not the application of the generic definition 8 to P(P,v^→ ) = (H(P, v^→ ) = F ), because we have written H(p^→ i, v^→ ) = T  in place of the instance relation p^→ i ≼ v^→ . However, as illustrated by the following lemma, H(q^→ , v^→ ) = T and q^→  ≼ v^→  are closely related.

The lemma above suffices to relate Haskell matching to generic lazy matching, and thus to compute the utility of Haskell matching.

It is time to clearly stress on some important consequence of propositions U = U_rec, U_P = U_rec and U_H = U_rec: all our utility predicates are in fact equal. This suggests a quite powerful and elegant“semantical” proof technique, which we immediately demonstrate.

First observe that proving the irrelevance of column order for Haskell matching by induction on matrix and pattern structure would be quite cumbersome.

Also notice that the lemma above is not obvious, since Haskell matching depends upon column order in a strong sense. For instance, let P, q^→ , P′ and q^→ ′ be as follows.

Matrix P′ (resp. vector q^→ ′) is P (resp. q^→ ) with columns swapped. The sets of matching values are as follows.

Swapping the components of the elements of M_H(P, q^→ ) does not yield M_H(P′, q^→ ′), since (Ω  False) does not belong to M_H(P′, q^→ ′). However, some of the values of the M_H sets above are related by the permutation. Moreover, the equality U_H=U can be seen as telling us that there is at least one such value.

From now on, we simply write U for any utility predicate, regardless of semantics. We also write “algorithm U” for U_rec.