Previous Up Next

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$.

Previous Up Next