A case expression has the form
case <expr0> of <id1> : <type1> => <expr1>; ... <idn> : <typen> => <exprn>; esac
Case expressions provide runtime type tests on objects. First, \(\rm expr0\) is evaluated and its dynamic type \(\rm C\) noted (if \(\rm expr0\) evaluates to \(\rm void\) a run-time error is produced). Next, from among the branches the branch with the least type \(\rm <typek>\) such that \(\rm C \leq <typek>\) is selected. The identifier \(\rm <idk>\) is bound to the value of \(\rm <expr0>\) and the expression \(\rm <exprk>\) is evaluated. The result of the \(\rm case\) is the value of \(\rm <exprk>\). If no branch can be selected for evaluation, a run-time error is generated. Every \(\rm case\) expression must have at least one branch.
For each branch, let \(\tt T_i\) be the static type of \(\rm <expri>\). The static type of a \(\rm case\) expression is \(\tt\bigsqcup_{1 \leq i \leq n} T_i\). The identifier \(\rm id\) introduced by a branch of a \(\rm case\) hides any variable or attribute definition for \(\rm id\) visible in the containing scope.
The \(\rm case\) expression has no special construct for a "default" or "otherwise" branch. The same affect is achieved by including a branch
x : Object => ...
because every type is \(\leq\) to \(\rm Object\).
The \(\rm case\) expression provides programmers a way to insert explicit runtime type checks in situations where static types inferred by the type checker are too conservative. A typical situation is that a programmer writes an expression \(\tt e\) and type checking infers that \(\tt e\) has static type \(\tt P\). However, the programmer may know that, in fact, the dynamic type of \(\tt e\) is always \(\tt C\) for some \(\tt C \leq P\). This information can be captured using a case expression:
case e of x : C => ...
In the branch the variable \(\tt x\) is bound to the value of \(\tt e\) but has the more specific static type \(\tt C\).