This expresses general conditional branches on the value of $⟨$exp$\mathrm{⟩}$. $⟨$match$\mathrm{⟩}$ is of the form

  $\mathrm{⟨}$pat${}_{\mathrm{1}}$$\mathrm{⟩}$ => $\mathrm{⟨}$exp${}_{\mathrm{1}}$$\mathrm{⟩}$
| $\mathrm{\cdots }$
| $\mathrm{⟨}$pat${}_n$$\mathrm{⟩}$ => $\mathrm{⟨}$exp${}_n$$\mathrm{⟩}$

where each $⟨$pat${}_i$$\mathrm{⟩}$ is a pattern containing data constructors and $⟨$exp${}_i$$\mathrm{⟩}$ is the expression to be evaluated if $⟨$pat${}_i$$\mathrm{⟩}$ is matched against the value of $⟨$exp$\mathrm{⟩}$.

Each pattern $⟨$pat${}_i$$\mathrm{⟩}$ is a data pattern consisting of constructors and variables, as described in Chapter 20. This set of patterns must satisfy the following restrictions:

• •

  All variables occurring in a pattern must be distinct.

• •

  Every pattern must have the same type as the type of $⟨$exp$\mathrm{⟩}$.

• •

  For any $i$ such that $2lei\le n$, $⟨$pat${}_i$$\mathrm{⟩}$ must not be redundant. In other words, the set of data covered by $⟨$pat${}_i$$\mathrm{⟩}$ must not be a subset of the union of the sets of data covered by $⟨$pat${}_{\mathrm{1}}$$\mathrm{⟩}$, $\mathrm{\dots }$, $⟨$pat${}_{i\mathrm{-}\mathrm{1}}$$\mathrm{⟩}$.

For example, the following violates the third rule.

# fn x => case x of (X, 1, 2) => 1 | (1, X, 2) => 2 | (1, 1, 2) => 3;
(interactive):6.8-6.65 Error: match redundant and nonexhaustive
      (X, 1, 2) => ...
      (1, X, 2) => ...
  --> (1, 1, 2) => ...

Under these restrictions, this entire expression has the same type as each expression $⟨$exp${}_i$$\mathrm{⟩}$.

This case expression is evaluated as follows. It tries to match the value of $⟨$exp$\mathrm{⟩}$ with each pattern from $⟨$pat${}_{\mathrm{1}}$$\mathrm{⟩}$ to $⟨$pat${}_n$$\mathrm{⟩}$ in this order. For the first matched pattern $⟨$pat${}_i$$\mathrm{⟩}$, it binds variables in $⟨$pat${}_i$$\mathrm{⟩}$ to their corresponding part of the value and evaluates $⟨$exp${}_i$$\mathrm{⟩}$ to the result value. If no pattern matches with the value, it raises Match exception.