Semantics of pattern matching

The following is a partial specification; nothing more is guaranteed. Informally, when patterns overlap, more specific patterns are preferred to more specific ones. Apart from that, the choice is unspecified. More formally:

Matching a value with a pattern involves evaluating the value sufficiently to compare its data constants and constructors with those in the pattern, in some consistent, top-to-bottom (but otherwise unspecified) order. This match may result in

success:

the value can be seen to be an instance of the pattern,

failure:

the value cannot be an instance of the pattern, because it has a different data constant or constructor in some position, or

non-termination:

the value cannot be sufficiently evaluated to decide between the above, in the particular order of checking used.

If the match succeeds, it supplies values for the variables of the pattern.

A pattern (or sub-pattern) consisting only of variables and pairs always matches a value of the appropriate type, even if computation of the value would not terminate. Such patterns are called irrefutable.

Now suppose a function has been defined by a series of definitions

--

f

p

_

i1

...

p

_

in

<=

e

_

i

;

for i = 1, ..., k, or is the expression

lambda

p

_

11

...

p

_

1n

=>

e

_

1

|

...

|

p

_

k1

...

p

_

kn

=>

e

_

k

(At present, anonymous functions are required to be unary.) An application of this function to n argument values will have zero or more possible values, as follows:

• If some patterns p_ ij successfully match the corresponding arguments for some i, and all more specific patterns (if any) fail, then a possible value is the value of e_ i, with the variables of p_ ij taking the values they matched.

• If the matching of some pattern does not terminate, under some order of checking, then non-termination is a possible value.

If there are no possible values, the value of the application is a run-time error. Otherwise, one of the possible values is chosen, in a deterministic (but otherwise unspecified) manner.