In Figures 6 to 11 we summarize the typing rules for our two-level calculus. They define judgements of the form where is a set of type assumptions, 2Eis a two-level term, and is its type under assumptions A. We write AS to assert that holds ( ) and AM to assert that holds ( ). abbreviates for some .
The first group of typing rules (Fig. 6) deals
with the first-order fragment of the language. The rules [VAR] and [WEAK]
together provide the functionality of the standard axiom
.
We explicitly include the weakening rule here, as it can
drop assumptions on variables that have no influence on the (type of the) expression. In
a later set of rules (see Fig. 7
and 8) we will constrain the types in the assumption so
as to
guarantee properties of the free variables of lambda abstractions.
The rules for lifting of static base
values in a dynamic context [LIFT], for the conditional [COND,
COND-D], and for top-level function calls [CALL, CALL-D] are standard for
continuation-based specialization [4,23], save for
the fact that [CALL-D] (the memoizing call) demands that the types of all its
arguments are memoizable. However, the
treatment of constants and operators is more liberal than usual: The standard rules
for them [7]
The next set of rules (Fig. 7) deals with functions of fixed arity. Here, our ability to constrain exactly the types of the free variables comes into play. Rule [ABS-M] guarantees that the closure of every memoized function only captures variables whose type is memoizable. The types of the arguments of such a function are unconstrained. Similarly, [ABS-S] introduces completely static functions which may only refer to completely static values, while [ABS] introduces standard functions which may process arbitrary values. Rule [ABS-D] is the standard rule for dynamic abstraction. Each of these rules has a companion application rule which types applications of memoized, static, and dynamic functions, respectively.
The same reasoning applies to variadic functions (Fig. 8). Here, we must additionally insist that the argument variables be of type ``argument list.'' Furthermore, we have the [VAPP-D2] rule which deals with the case where the function is dynamic, but the length of the argument list is known (see 3.2).
The final set of rules deals with eval and call/cc. The rule [EVAL] deals with the static eval: The text of the expression must be a static base value and the result must be completely static (not necessarily constrained to base values). In this case, the specializer executes eval. Rule [EVAL-LIFT] deals with static expression texts in dynamic context (quite similar to the standard rule [LIFT]), the corresponding eval inserts the code result of the expression into the residual program. Finally, rule [EVAL-D] deals with dynamic expression texts in dynamic contexts. Executing eval generates a call to eval in the residual program.
The construct eval is superficially similar to lift as it also coerces a specialization-time value to code. However, lift produces a piece of code which produces the specialization-time value when executed; it generates the quoted value. In contrast, eval simply inserts its argument in the residual program without quoting it. Composing eval with lift has the same effect, but with eval it is possible to omit eval from the residual program altogether.
In order to safely
process call/cc statically, the argument must be a completely static
function of type
as demanded by rule
[CWCC]. This way, it cannot handle code and it cannot be memoized.
Otherwise it must be suspended to the residual program as dictated by rule [CWCC-D].
For completeness, we also exhibit the typing rules for the static operations on argument lists in Fig. 10 and the rule for typing two-level programs in Fig. 11. We have omitted the dynamic variants of the argument list operations as they are identical to the [OP-D] rule in Fig. 6. Definitions and programs are typed using different judgements , which relates a definition to the remaining program, and , which states that all definitions in are consistently typed with respect to all their uses.
Finally, we define a completion of a (standard) program to be a well-typed two-level program such that is obtained by erasing all overlinings and underlinings, as well as omitting the (lift ...) construct.
In the above description we distinguish four different states that a function may assume: static, completely static, memoized, and dynamic. Every non-memoized function can be represented by a standard abstraction, which may result in faster specialization.