ExitWithValue

Normally, exiting from an abstraction is done simply by ``falling off'' (one of) the tip(s) of the expression tree of the abtraction's body. This operation is captured by the simple operational semantics of each of the three RETURN instructions. Namely, when executing a RETURN instruction, the runtime performs the following three-step procedure; it

1. pops the result from its result stack;^3.3
2. restores the (previously saved) runtime state;
3. pushes the result popped in Step 1 onto the restored state's own result stack.

However, it is also often desirable, under certain circumstances, that computation may not be let to proceed further at its current level of nesting of exitable abstractions. Then, computation may be allowed to return right away from this current nesting (i.e., as if having fallen off this level of exitable abtraction) when the conditions for this to happen are met. Exiting an abstraction thus must also return a specific value that may be a function of the context. This is what the $\ExitWithValue {v}$ kernel construction:

$$\ExitWithValue {v}$$ (3.11)

expresses. This kernel construction is provided in order to specify that the current local computation should terminate without further ado, and exit with the value denoted by the specified expression.

Now, there are several notions in the above paragraphs that need some clarification. For example, what an ``exitable'' abstraction is, and why worry about a dedicated construct in the kernel language for such a notion if it does nothing more than what is done by a RETURN instruction.

First of all, from its very name $\ExitWithValue {v}$ assumes that computation has entered that from which it must exit (with or without any value). This from thing is an exitable abstraction; that is, the latest $\lambda$-abstraction having the property of being exitable. Not all abstractions are exitable. For example, any abstraction that is generated as part of the target of some other kernel expression's syntacting sugar (e.g., $\Let {x_1=e_1;\ldots;x_n=e_n;}{e}$ or $\Comprehension {\oplus}{e}{\IN {x_1}{e_1},\ldots,\IN {x_n}{e_n}}$, and more generally any construct that hide implicit abstractions within), will not be deemed exitable.

Secondly, exiting with a value $\KRNL {v}$ means that the type $\TYPE {T}$ of $\KRNL {v}$ must be congruent with what the return type of the abstraction being exited is. In other words:

$$\typerule {\gammahastype {v}{\textit{T}},\;\; \gammahastype {\Phi... ...ype {T'}{T}}}<tex2html_comment_mark>112 {\gammahastype {\ExitWithValue {v}}{T}}$$ (3.12)

where $\Phi$ denotes the type of the latest exitable abstraction in the context $\Gamma$.

The above scheme indicates the following necessities:

1. The typing rules for an abstraction deemed exitable must record in its typing context $\Gamma$ the value of $\Phi_\Gamma$, the type in $\Gamma$ of the latest exitable abstraction, if any such exists; (if none does, a static semantics error is triggered to indicate that it is impossible to exit from anywhere before first entering somewhere), and,
2. the runtime system must also keep track (in a stack) of the states of the saved each time a closure coming from an exitable abstraction is entered; (dually, this state stack must also be popped upon ``falling off'' (i.e., normally exiting) an exitable closure), and,
3. NL_RETURN instructions (for each runtime sort) must be defined as their corresponding RETURN instructions except that the runtime state to restore is the one popped out of the exitable state stack.