2  Patterns, values, etc.

Most ML values can be defined as ground terms over some signatures. Signatures are introduced by data type definitions. For instance¹:

type mylist = Nil | One of int | Cons of int * mylist

Values of type mylist are built from three constructors Nil (of zero arity, i.e. constant constructor), One (unary) and Cons (binary). Most of ML values can be expressed in that setting. Booleans are a two (constant) constructor type, the integer type is defined as possessing infinitely many (or 2³¹) constant constructors, pairs are a type with a sole binary constructor (written with the infix operator “,”), etc.

More generally, our values are defined as (ground) terms over the constructor signatures. We make them explicit as follows:

In examples, we systematically omit () after constants constructors, so as to match Objective Caml syntax (we write Nil, true, 0, etc.). This simple definition of values as terms suffices to our purpose of studying pattern matching anomalies in call-by-value ML. However,

• A proper semantics for pattern matching in a lazy language should define partial values, which we do in Section 4.
• Although many values, including integers, strings, can be seen as terms built over known signatures (maybe of infinite size), not all values can be seen as such. For instance, consider functions or values of a type that exhibits parametric polymorphism. However, we are not interested in the exact nature of all the types and values of ML. Instead, we shall rely on the following informal axiom: given any type t, we assume the existence of at least one value that possesses t as a type.

Strictly speaking, the axiom does not hold, at least in Caml where one can define a type with no values in it:

type t_empty

Then we can define the following data type and matching:

type t = C of t_empty
let f x = match x with C y -> y

Semantically the above clause C y -> y is useless: no value exists that matches the pattern C y. But our checker will not flag the clause as such, since it assumes the existence of a value of type t_empty. Similarly, our checker will flag the following match as non-exhaustive:

type tt = A | B of t_empty
let g x = match x with A -> true

The non-exhaustiveness diagnostic is wrong, strictly speaking, since there does not exist a value B(v), where v has type t_empty. As a consequence, the match above matches all possible values of type tt. We view this issue as a minor one, considering that the non-empty type axiom holds for the vast majority of types.

Patterns are used to discriminate amongst values. More precisely a pattern describes a set of values with a common prefix. That is, patterns are terms with variables and a given pattern p describes its instances σ(p) where σ ranges over substitutions. However, we wish to stay close to programming practice and define patterns as follows:

Variables in fact do not appear in our definition of patterns. For our purpose, they can be replaced by the wildcard symbol “_”. One can see wildcards as variables whose exact names are irrelevant. Additionally, our patterns feature “or-patterns” as offered by modern implementations of the ML language.

Furthermore, it is important to remark that patterns are type correct, that is, we assume that patterns follow the sorting discipline enforced by some declarations of data types. In practice, the Objective Caml compiler performs pattern matching analysis after the typing phase, so that patterns do hold type annotations. In our formal treatment we avoid making those annotations explicit everywhere, this would be quite cumbersome and of little explanatory value. However, when appropriate, we sometime show type annotation as (p:t).

In the usual theory of terms, a term v (of type t) is an instance of a pattern p (of type t) when the pattern describes the prefix of the term. That is, when there exists a substitution σ such that σ(p) = v. In the case of linear patterns, where no variable appears more than once in a given pattern, the instance relation can be defined inductively and the exact names of variables are irrelevant.

It is important to notice again that pattern matching is defined in a typed context. In particular _ ≼ v does not holds for any value v, but only for value v of the specified type t, which can be made explicit with the notation (_:t). Moreover, as a consequence of our axiom “types are not empty”, any pattern p admits at least one instance.

In Definition 1 above we used the very convenient notations p^→  = (p₁⋯p_a) and v^→  = (v₁⋯v_a). Notations p^→  and v^→  stand for (row) vectors of patterns and values respectively. Observe that we just defined the instance relation on vectors. We shall also consider matrices of patterns P = (p_jⁱ), of size m × n where m is P height (number of rows) and n is P width (number of columns). Boundary cases deserve a few notations: matrices with no row (m = 0 and n ≥ 0) are written ∅; while non-empty matrices of empty rows (m > 0 and n = 0) are written ( ). Finally, we sometime denote row number i of matrix P as p^→ i.

We recall the definition of ML pattern matching in this convenient framework of matrices and vectors.

In other words, vector v^→ matches the first row it is an instance of, starting from the top of matrix P. Again, typing is implicit: all rows in P and v^→ must be of a common type.

Then, for instance we have:

1. Vector v^→  = (Nil Nil) matches the first row of P, since (Nil _) ≼ (Nil Nil) (because p₁¹ = Nil ≼ Nil = v₁) and p₂¹ = _ ≼ Nil = v₂).
2. Vector w^→  = (One(0) Nil) matches the second row of P, since we have
   1. (_   Nil) ≼ (One(0) Nil), that is w^→ is an instance of the second row of matrix P.
   2. (Nil _) ⋠(One(0) Nil) (because p₁¹ = Nil ⋠One(0) = w₁), that is, w^→ is not an instance of the first row of matrix P.
3. Vector z^→  = (One(1) One(1)) matches the fifth row of matrix P, since we have:
   1. Vector z^→  is an instance if p^→ 5 = (_   _) (as any value vector of the appropriate type is).
   2. Additionally, vector z^→  is not an instance of any of the first four rows of P. For instance, 0 ⋠1 implies One(0) ⋠One(1), which in turn implies that vector z^→  cannot be an instance of rows number 3 and 4 of matrix P.

As we have already noticed, a pattern can be interpreted as the set of its instances. Similarly, a matrix can be interpreted as the union of the instances of its rows.

ML pattern matching can be reformulated with this new definition as: vector v^→ matches row number i in matrix P, if and only if P^[1…i) ⋠v^→ and p^→ i ≼ v^→, where matrix P^[1…i) is the (i−1) × n matrix consisting of the rows of P that precede row number i.

1

In this paper, we use Objective Caml syntax