Most ML values can be defined as ground terms over some signatures. Signatures are introduced by data type definitions. For instance1:
type mylist = Nil | One of int | Cons of int * mylist
Values of type
mylist are built from three
Nil (of zero arity, i.e. constant
One (unary) and
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 231) 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
This simple definition of values as terms suffices to
our purpose of studying pattern matching anomalies in call-by-value
Strictly speaking, the axiom does not hold, at least in Caml where one can define a type with no values in it:
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
But our checker will not flag the clause as such,
since it assumes the existence of a value of type
Similarly, our checker will flag the following match as
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
As a consequence, the match above matches all possible values of
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→ = (p1⋯pa) and v→ = (v1⋯va). 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 = (pji), 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:
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.
|(p1i⋯pni) ≼ (v1⋯vn).|
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.