Assessing the Overhead of ML Exceptions by Selective CPS Transformation

Jung-taek Kim, Kwangkeun Yi

Programming Languages Lab. ^{∗} Department of Computer Science

KAIST ^{†} Olivier Danvy

BRICS ^{‡}

Department of Computer Science University of Aarhus ^{§}

Abstract

ML’s exception handling makes it possible to describe exceptional execution flows conveniently, but it also forms a performance bottleneck. Our goal is to reduce this overhead by source-level transformation.

To this end, we transform source programs into continuation-passing style (CPS), replacing handle and raise expressions by continuation-catching and throwing expressions, respectively. CPS-transforming every expression, however, introduces a new cost. We therefore use an exception analysis to transform expressions selectively: if an expression is statically determined to involve exceptions then it is CPStransformed; otherwise, it is left in direct style.

In this article, we formalize this selective CPS transformation, prove its correctness, and present early experimental data indicating its effect on ML programs.

1 Introduction

Programming with exceptions is an expensive affair in ML, since it involves installing and uninstalling exceptions handlers at run time. This dynamic nesting of handlers can be a performance bottleneck if it is frequent, e.g., when the handler exists in the body of a recursive function.

1.1 An example

For example, let us consider the problem of substituting a closed expression for a variable in another expression. The expression is either a variable, a lambda abstraction, or an application (see Figure 1). In a naïve implementation of

     structure Exp
     = struct
         datatype exp = VAR of string
                      | LAM of string * exp
                      | APP of exp * exp
       end

Figure 1: A sample definition of expressions

substitution, the source expression is entirely copied. In an economical implementation, the subexpressions unaffected by the substitution (i.e., those where the variable to substitute does not occur free) are shared between the source expression and the resulting expression. This economical implementation is an instance of what Gérard Huet, in the mid-80’s, called “sharing transducers.”

We measured the performances of two sharing transducers: one using exceptions (Figure 2) and the other using continuations (Figure 3). Figure 4 displays two extreme cases: (a) one where the source expression yields much exception raising and handling; and (b) one where the source expression yields no exception raising and handling at all. In Case (a), the continuation-based version is about twice as fast as the exception-based version.^{1} In Case (b), the continuation-based version runs in about the same time as the exception-based version.

We also implemented a third sharing transducer, using a disjoint sum instead of an exception or two continuations. In performance, it matches the continuation-based one, thus showing that at least for sharing transducers, continuations form a viable alternative solution to disjoint sums.

Figure 4 shows that there is considerable room for improvement, particularly when the input program uses exceptions frequently. Our goal is to achieve this optimization by source-level transformation(s). Since exceptions affect the control flow of programs, we choose to translate the raise and handle constructs into continuation-based idioms.

1.2 This work

We remove raise and handle from ML programs by transforming them into continuation-passing style (CPS). Specifically, we pass two continuations: one for the normal course of execution, and one for exceptional situations.

∗http://pllab.kaist.ac.kr This work is supported in part by Korea Science and Engineering Foundation grant KOSEF 961-0100-001-2 and by Korea Ministry of Information and Communication grant 96151-IT2-12.

† Department of Computer Science (http://cs.kaist.ac.kr), Korea Advanced Institute of Science & Technology, Taejon 305-701, Korea.

E-mail: {judaigi,kwang}@cs.kaist.ac.kr ‡ Basic Research in Computer Science (http://www.brics.dk), Centre of the Danish National Research Foundation.

§ Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark.

E-mail: danvy@brics.dk

1The peaks in the graph reflect the situations where the programs hit the memory thresholds that make the garbage collector increase its heap size (which causes some overhead).

structure Subst_exn
= struct
local open Exp
      exception same
in fun subst (x, e, b)
       = let fun walk (VAR x')
                 = if x' = x then e else raise same
               | walk (LAM (x', b'))
                 = if x' = x then raise same else LAM (x', walk b')
               | walk (APP (e0, e1))
                 = let val e0' = walk e0
                   in APP (e0', walk e1
                                handle same => e1)
                   end
                   handle same => APP (e0, walk e1)
         in walk b
            handle same => b
         end
end
end

Figure 2: Economical substitution using exceptions

structure Subst_cps =
struct
local open Exp
in fun subst (x, e, b)
 = let fun walk (VAR x') k h
           = if x' = x then k e else h ()
         | walk (LAM (x', b')) k h
           = if x' = x then h () else walk b' (fn b'' => k (LAM (x', b''))) h
         | walk (APP (e0, e1)) k h
           = walk e0
                  (fn e0' => walk e1 (fn e1' => k (APP (e0', e1'))) (fn () => k (APP (e0', e1))))
                  (fn () => walk e1 (fn e1' => k (APP (e0, e1'))) h)
   in walk b (fn b' => b') (fn () => b)
   end
end
end

Figure 3: Economical substitution using continuations

X coordinate: the input expression size. Y coordinate: execution time in ms, using SML/NJ 110 on a Sun UltraSPARC 2 (user time + system time + gc time).

(a) Exceptions are frequently raised.  (b) No exceptions are raised.

Figure 4: Performance difference: exception-based (Figure 2) versus continuation-based (Figure 3) versions

Passing two continuations to process exceptions is not a new idea: for example, Appel mentions it in his book on compiling with continuations [App92]. However, and even though his ML compiler uses a CPS transformation, it does not remove raise and handle: these two constructs remain as primitive operators (sethdlr and gethdlr). We conjecture that it was not cost-effective to pass two continuations to every function as specified, e.g., by Biagioni et al. [BCL^{+}98, Figure 2].

The new idea here is a cost-effective CPS transformation using two continuations: we exploit the static information from Yi and Ryu’s exception analysis [YR97] to reduce the continuation-passing traffic to where it is actually needed. To this end, we present a selective CPS transformation that only introduces continuations where they are needed, based on the static information gathered by the exception analysis. Our selective CPS transformation thus generalizes both the CPS transformation with two continuations (for expressions using exceptions) and the identity transformation (for exception-free expressions).

We prove that this selective CPS transformation is correct, and present some early experimental data that show its effectiveness for exception-intensive programs.

1.3 Related work

We know of three earlier works using the idea of exploiting static information to perform a selective CPS transformation. This has been done for strictness analysis [DH93a], for totality analysis [DH93b], and for binding-time analysis [DD95]. None of these selective CPS transformations, however, has been integrated in an actual compiler. Only the latter transformation has been integrated in a partial evaluator [Dus97]. In their work on “selective thunkification,” Steckler and Wand use a similar idea to reduce the number of thunks when converting a call-by-name program into a call-by-value program, after strictness analysis [HD97, SW94].

1.4 Overview

The rest of this article is organized as follows. Section 2 defines the syntax and semantics of our source language, a subset of the ML’s core. Section 3 presents a naïve CPS transformation that blindly passes continuations to every expression. Section 4 defines the annotation process of selecting candidate expressions for our selective transformation. Section 5 formalizes our selective transformation and proves its correctness. Section 6 shows our preliminary experimental data and discusses some more selective transformations which we will consider if the ongoing experiments with the selective transformation turn out to be not economical enough.

2 Source Language

2.1 Abstract syntax

We consider ML’s core language, which is call-by-value and higher-order. Its abstract syntax reads as follows. (κ denotes a constructor.)

e ::= 1  unit
| x  variable
| λx. e  function
| fix f λx. e  recursive function
| e_{1} e_{2}  application
| con κ e  exception construction
| decon e  deconstruction
| case e_{1} κ e_{2} e_{3}  switch
| handle e_{1} κ λx. e_{2} handle expression
| raise e  raise exception

An exception value κ·v is constructed by “con κ e” where evaluating e yields v. Symmetrically, an exception value κ · v denoted by e is deconstructed into v by evaluating “decon e.” Evaluating the case expression “case e_{1} κ e_{2} e_{3}” yields the value of e_{2} if the value of e_{1} is κ·v; otherwise, it yields the value of e_{3}. When evaluating the raise expression “raise e” e is first evaluated, yielding an exception value κ·v. The exception associated to κ is then raised. The handle expression “handle e_{1} κ λx.e_{2}” evaluates e_{1} first. If e_{1} yields an exception value κ·v, this exception value is passed to λx.e_{2}. Otherwise, the value of the handle expression is the value yielded by e_{1}.

For brevity, we omit datatype values, strings, and memory operations (assignment, reference, and dereference) here. In reality, we work on the complete core language of Standard ML.

2.2 Operational semantics

We define the semantics of expressions with a structural operational semantics [Plo81] using Felleisen’s evaluation contexts [Fel87]. In doing so, we need to extend the expressions to contain a set of values v and raised exceptions p that represent terminated computations:

v ::= 1  unit
| λx. e  function
| fix f λx. e recursive function
| κ·v  exception value with argument v
p ::= \underline{κ·v}  raised exception

The evaluation context C is defined by

C ::= [ ]  hole

                                                                            | con κ C
                                                                            | decon C

| C e
| v C
| case C κ e_{1} e_{2}
| handle C κ λx. e

                                                                            | raise C

This context defines a left-to-right, call-by-value reduction. As usual, we write C[e] if the hole in context C is filled with e. We use this context to define the reduction rule for arbitrary expressions:

{e → e′ \atop C[e] → C[e′]}

The single reduction step e → e′ for a redex e is defined in Figure 5. As usual, the notation [v/x]e denotes the new expression that results from substituting v for every free occurrence of x in e.

Normal reduction steps:

con κ v → κ·v

                   decon κ·v → v

(λx. e) v → [v/x]e
(fix f λx. e) v → [v/x][fix f λx. e/f]e
case κ·v κ e_{1} e_{2} → e_{1}
case κ·v κ′ e_{1} e_{2} → e_{2} (κ′ ≠ κ)
handle v κ λx. e → v

Exceptional reduction steps:

raise κ·v → \underline{κ·v}
raise\underline{κ·v} → \underline{κ·v}
handle\underline{κ·v} κ λx. e → (λx. e) κ·v
handle\underline{κ·v} κ′ λx. e → \underline{κ·v} (κ′ ≠ κ)
con κ \underline{κ·v} → \underline{κ·v}
decon\underline{κ·v} → \underline{κ·v}
case\underline{κ·v} κ′ e_{1} e_{2} → \underline{κ·v}
\underline{κ·v} e → \underline{κ·v}
(λx. e) \underline{κ·v} → \underline{κ·v}
(fix f λx. e) \underline{κ·v} → \underline{κ·v}

Figure 5: Reduction steps

T (1) = λ⟨K, H⟩. K(1)
T (x) = λ⟨K, H⟩. K(x)
T (con κ e) = λ⟨K, H⟩. T (e) ⟨λv. K (con κ v), H⟩
T (decon e) = λ⟨K, H⟩. T (e) ⟨λv. K (decon v), H⟩
T (λx. e) = λ⟨K, H⟩. K(λx. T (e))
T (fix f λx. e) = λ⟨K, H⟩. K(fix f λx. T (e))
T (e_{1} e_{2}) = λ⟨K, H⟩. T (e_{1}) ⟨λf. T (e_{2}) ⟨λv. f v ⟨K, H⟩, H⟩, H⟩
T (case e_{1} κ e_{2} e_{3}) = λ⟨K, H⟩. T (e_{1}) ⟨λv. case v κ (T (e_{2})⟨K, H⟩) (T (e_{3})⟨K, H⟩), H⟩
T (handle e_{1} κ λx. e_{2}) = λ⟨K, H⟩. T (e_{1}) ⟨K, λv. case v κ ((λx. T (e_{2})) v ⟨K, H⟩) (H v)⟩
T (raise e) = λ⟨K, H⟩. T (e) ⟨H, H⟩

Figure 6: Naïve CPS transformation T

Definition 1 The semantics of a closed expression e is defined to be the sequence of reduction steps

e → e_{1} → e_{2} → · · · .

If the sequence terminates with a value v (with an uncaught exception \underline{κ·v}, respectively) after zero or more reductions, we write

e →^{∗} v (e →^{∗} \underline{κ·v}, respectively)

3 Naïve CPS Transformation

We can remove the raise and handle expressions by passing two continuations to each expression. Consider, for example, the following handle expression

handle e_{1} κ λx. e_{2}.

The handler λx. e_{2} is installed prior to evaluating e_{1}. Therefore, if an exception \underline{κ·v} is raised during this evaluation, then it is caught by the handler and λx. e_{2} is applied to κ·v, yielding the value of the handle expression.

The CPS transformation encodes both how to handle a raised exception and how to proceed thereafter, with a handler continuation. This handler continuation is passed to the sub-expressions of e_{1}. Accordingly, a raise expression is CPS-transformed with the current handler continuation in place of the current continuation. Note that, because a handler continuation needs to encode how to continue after the handling, we also have to make the normal continuation ready to be captured by a handler continuation. Thus we keep passing two continuations (normal and handler continuations) to every expression.

Figure 6 shows the definition of this CPS-transformation function T. The T function transforms expressions of type τ to expressions of type (τ → Ans) × (Exn → Ans) → Ans.

Theorem 1 (Correctness of T) For any program ℘

\begin{aligned}℘ →^{∗} v & ⟹ & T (℘) ⟨K, H⟩ →^{∗} K(Ψ(v)) \\ ℘ →^{∗} \underline{κ·v} & ⟹ & T (℘) ⟨K, H⟩ →^{∗} H(Ψ(κ·v)) \end{aligned}

where the auxiliary function Ψ coerces direct-style values to CPS values:

Ψ(1) = 1
Ψ(λx. e) = λx. T (e)
Ψ(fix f λx. e) = fix f λx. T (e)
Ψ(κ·v) = κ·Ψ(v)

Proof. Analogous to the proof of Plotkin’s simulation theorem [Plo75]. In the proof we need to extend T to be defined for values and raised exceptions:

\begin{aligned}T (v) & = & λ⟨K, H⟩. K(Ψ(v)) \\ T (\underline{κ·v}) & = & λ⟨K, H⟩. H(Ψ(κ·v)) \end{aligned}

□

Transforming every expression into this CPS-form, as done by T, however, offsets the benefit of removing raisehandle expressions. Indeed, every expression becomes a higher-order function application that receives two functions (continuations).

At this stage, two orthogonal optimizations can take place:

• We can perform administrative reductions, e.g., during the CPS transformation [DF92].

• We can selectively apply the CPS transformation by exploiting the results of Yi and Ryu’s exception analysis [YR97]. The point is that an exception analysis tells us a conservative approximation of which expressions may raise an uncaught exception when they are evaluated and of which functions may raise an uncaught exception when they are applied. Therefore, such an analysis also tells us a safe approximation of which expressions do not raise any uncaught exceptions when they are evaluated and of which functions do not raise any uncaught exceptions when they are applied. These latter expressions and functions need not be CPS-transformed.

4 Annotation

We pass two continuations to an expression e to cater for the case where uncaught exceptions raised while evaluating e (in the future) are caught by a surrounding handler (that was installed in the past). The raise expression will call a handler continuation that was passed to it from the outer context. If we know that evaluating an expression will not yield an uncaught exception, there is no need to pass it any continuations since we know statically that these continuations would be of no use. Three cases occur:

• If evaluating e cannot yield any uncaught exceptions (i.e., it can only yield normal values), then e needs no continuations.

• If evaluating e may yield an uncaught exception which is not handled in the complete program, then e needs no continuations either: we can just call an abort function instead of raising this uncaught exception.

• If evaluating e may yield an uncaught exception which is handled in the complete program, then e needs two continuations.

The expressions of the third kind are candidates to our selective CPS transformation. The other ones can be kept in direct style.

Our selective CPS transformation therefore needs two pieces of information per source expression: whether the expression is protected by a handler and which exceptions, if any, may be raised when the expression is evaluated. The first condition ⌈e⌉^{κ} is checked by scanning the subexpressions in the scope of a handler (i.e., sub-expressions of e in “handle e κ λx. e′”), referencing a safe closure analysis [YR97].^{2} The second condition ⌊e⌋_{κ} checks whether evaluating e raises an exception κ. It is based on Yi and Ryu’s exception analysis [YR97].

If both the conditions ⌈e⌉^{κ} and ⌊e⌋_{κ}, for the same exception κ, hold for an expression e, the exceptional expression e becomes the candidate ĕ of our CPS transformation. Otherwise, the expression e is marked ė as normal.

Figure 7 displays the rules

R(Exn analysis_{℘}, Closure analysis_{℘}) κ ∈ Exn analysis_{℘}(e)

⌊e⌋_{κ}

{handle e_{1} κ λx. e_{2} \atop ⌈e_{1}⌉^{κ}}

{⌈con κ′ e⌉^{κ} \atop ⌈e⌉^{κ}}  {⌈decon e⌉^{κ} \atop ⌈e⌉^{κ}}  {⌈raise e⌉^{κ} \atop ⌈e⌉^{κ}}

⌈e_{1} e_{2}⌉^{κ} λx. e ∈ Closure analysis_{℘}(e_{1}) ⌈e_{1}⌉^{κ} ⌈e_{2}⌉^{κ} ⌈e⌉^{κ}

{⌈case e_{1} κ e_{2} e_{3}⌉^{κ} \atop ⌈e_{1}⌉^{κ} ⌈e_{2}⌉^{κ} ⌈e_{3}⌉^{κ}}

⌈e⌉^{κ} ⌊e⌋_{κ} ; ĕ

⌊e⌋_{κ} is read as “evaluating e may raise a κ-exception.” ⌈e⌉^{κ} is read as “a κ-handler protects e.” Once the analysis is completed, any expression e that is not marked as exceptional ĕ is marked as normal ė.

Figure 7: Rules R(Exn analysis_{℘}, Closure analysis_{℘}) for deciding whether an expression e in a program ℘ is exceptional (ĕ) or normal (ė).

for determining which expressions are exceptional in program ℘. The first analysis, Exn analysis_{℘}, maps each expression of the program ℘ to the set of exceptions that may be uncaught in the expression. The second analysis, Closure analysis_{℘}, maps each function expression to the set of lambda-abstractions that can flow into it. These two auxiliary analyses are assumed correct. In our implementation we use the ones developed by Yi and Ryu [YR97].

Definition 2 The annotated version Annotate(℘) of a program ℘ is the one resulting from marking each sub-expression e either as exceptional (ĕ) or as normal (ė), based on the rules R(Exn analysis_{℘}, Closure analysis_{℘}) in Figure 7.

Theorem 2 (Safety of Annotation) If an expression e of a program is marked normal ė, then evaluating it yields either a normal value or an uncaught exception that aborts the program.

Proof. Assume for contradiction that an expression e evaluates into an uncaught exception that will be handled inside the program. Then it must be marked exceptional ĕ because ⌊e⌋_{κ} and ⌈e⌉^{κ} hold and are based on annotation rules that use Exn analysis_{℘} and Closure analysis_{℘}, both of which are safe. □ Figure 8 shows the syntax of well-formed sets of normal expressions ė and exceptional expressions ĕ, respectively. Let us list some noteworthy cases:

• An application expression ė_{1} ė_{2} with all normal subexpressions can be exceptional if a function that flows into ė_{1} has an exceptional body.

2For languages with exceptions that can carry functions, existing works [Shi91, HM97, JW96, Ses89] cannot be used because exception analysis and closure analysis are interdependent in ML. We therefore had to devise our own closure analysis.

Annotated expressions: e ::= ė | ĕ

Normal expressions: ė ::= 1 | x
| λx. ė | λx. ĕ
| fix f λx. e
| ė_{1} ė_{2}

| con κ ė | decon ė

| case ė_{1} κ ė_{2} ė_{3}
| handle e_{1} κ λx. ė_{2}
| handle ė_{1} κ λx. ĕ_{2}

| raise ė

Exceptional expressions: ĕ ::= e_{1} e_{2}

                                                          | con κ ĕ
                                                          | decon ĕ

| case ĕ_{1} κ e_{2} e_{3}
| case e_{1} κ ĕ_{2} e_{3}
| case e_{1} κ e_{2} ĕ_{3}
| handle ĕ_{1} κ λx. e_{2}

                                                          | raise e

Figure 8: Two classes of expressions: normal or exceptional

Define ⊥_{K} = λx.x and ⊥_{H} = λx.raise x. Transformation Ṫ (ė) for normal expressions ė:

Ṫ (1) = 1
Ṫ (x) = x
Ṫ (λx. ė) = λx. (λ⟨K, H⟩. K(Ṫ (ė)))
Ṫ (λx. ĕ) = λx. T̆(ĕ)
Ṫ (fix f λx. ė) = fix f λx. λ⟨K, H⟩. K(Ṫ (ė))
Ṫ (fix f λx. ĕ) = fix f λx. T̆(ĕ)
Ṫ (ė_{1} ė_{2}) = Ṫ (ė_{1}) Ṫ (ė_{2}) ⟨⊥_{K}, ⊥_{H}⟩
Ṫ (con κ ė) = con κ Ṫ (ė)

    Ṫ (decon ė) = decon Ṫ (ė)

Ṫ (case ė_{1} κ ė_{2} ė_{3}) = case Ṫ (ė_{1}) κ Ṫ (ė_{2}) Ṫ (ė_{3})
Ṫ (handle ė_{1} κ λx. ė_{2}) = Ṫ (ė_{1})
Ṫ (handle ė_{1} κ λx. ĕ_{2}) = Ṫ (ė_{1})
Ṫ (handle ĕ_{1} κ λx. ė_{2}) = T̆(ĕ_{1}) ⟨⊥_{K}, λv. case v κ ((λx. Ṫ (ė_{2})) v) (⊥_{H} v)⟩
Ṫ (raise ė) = ⊥_{H}(Ṫ (ė))

Transformation T̆(ĕ) for exceptional expressions ĕ:

T̆(ė_{1} ė_{2}) = λ⟨K, H⟩. Ṫ (ė_{1}) Ṫ (ė_{2}) ⟨K, H⟩
T̆(ĕ_{1} ė_{2}) = λ⟨K, H⟩. T̆(ĕ_{1}) ⟨λf. (f Ṫ (ė_{2}) ⟨K, H⟩), H⟩
T̆(ė_{1} ĕ_{2}) = λ⟨K, H⟩. (λf. T̆(ĕ_{2}) ⟨λv. (f v ⟨K, H⟩), H⟩) Ṫ (ė_{1})
T̆(ĕ_{1} ĕ_{2}) = λ⟨K, H⟩. T̆(ĕ_{1}) ⟨λf. T̆(ĕ_{2}) ⟨λv. (f v ⟨K, H⟩), H⟩, H⟩
T̆(con κ ĕ) = λ⟨K, H⟩. T̆(ĕ)⟨λv. K(κ·v), H⟩
T̆(decon ĕ) = λ⟨K, H⟩. T̆(ĕ)⟨λκ·v. K(v), H⟩
T̆(case ĕ_{1} κ ė_{2} ė_{3}) = λ⟨K, H⟩. T̆(ĕ_{1}) ⟨λv. case v κ K(Ṫ (ė_{2})) K(Ṫ (ė_{3})), H⟩
T̆(case ė_{1} κ ĕ_{2} ė_{3}) = λ⟨K, H⟩. case Ṫ (ė_{1}) κ (T̆(ĕ_{2})⟨K, H⟩) K(Ṫ (ė_{3}))
T̆(case ė_{1} κ ė_{2} ĕ_{3}) = λ⟨K, H⟩. case Ṫ (ė_{1}) κ K(Ṫ (ė_{2})) (T̆(ĕ_{3}) ⟨K, H⟩)
T̆(case ĕ_{1} κ ĕ_{2} ė_{3}) = λ⟨K, H⟩. T̆(ĕ_{1}) ⟨λv. case v κ (T̆(ĕ_{2}) ⟨K, H⟩) K(Ṫ (ė_{3})), H⟩
T̆(case ĕ_{1} κ ė_{2} ĕ_{3}) = λ⟨K, H⟩. T̆(ĕ_{1}) ⟨λv. case v κ K(Ṫ (ė_{2})) (T̆(ĕ_{3}) ⟨K, H⟩), H⟩
T̆(case ė_{1} κ ĕ_{2} ĕ_{3}) = λ⟨K, H⟩. case Ṫ (ė_{1}) κ (T̆(ĕ_{2}) ⟨K, H⟩) (T̆(ĕ_{3}) ⟨K, H⟩)
T̆(case ĕ_{1} κ ĕ_{2} ĕ_{3}) = λ⟨K, H⟩. T̆(ĕ_{1}) ⟨λv. case v κ (T̆(ĕ_{2})⟨K, H⟩) (T̆(ĕ_{3})⟨K, H⟩), H⟩
T̆(handle ĕ_{1} κ λx. ė_{2}) = λ⟨K, H⟩. T̆(ĕ_{1}) ⟨K, λv. case v κ K((λx. Ṫ (ė_{2})) v) (H v)⟩
T̆(handle ĕ_{1} κ λx. ĕ_{2}) = λ⟨K, H⟩. T̆(ĕ_{1}) ⟨K, λv. case v κ ((λx. T̆(ĕ_{2})) v ⟨K, H⟩) (H v)⟩
T̆(raise ė) = λ⟨K, H⟩. H(Ṫ (ė))
T̆(raise ĕ) = λ⟨K, H⟩. T̆(ĕ) ⟨H, H⟩

Figure 9: Selective CPS transformation • raiseė can be normal^{3} if no handler exists that catches

the exception ė.

• handle ĕ_{1} κ λx. ė_{2} can be normal or exceptional depending on whether an uncaught exception from ĕ_{1} is handled by λx. ė_{2} or not.

• The toplevel expression of the program is always marked normal because it evaluates either into a normal value or into an uncaught exception.

5 Selective CPS Transformation

Our selective CPS transformation is defined by two transformation functions Ṫ and T̆, which transform normal and exceptional expressions, respectively. We transform a program ℘ by applying Ṫ to its annotated version Annotate(℘):

Ṫ (Annotate(℘)).

Each sub-expression of ℘ is transformed by either Ṫ or T̆, depending on its annotation. Figure 9 displays the definitions.

T̆ transforms exceptional expressions of type τ into expressions of type (τ → α) × (Exn → α) → α. The type α is determined by the context where the transformation T̆ occurs. If T̆(ĕ_{1}) occurs where ĕ_{1} is a sub-expression of a normal expression ė, then the result type α of the continuations becomes the type of ė. If ĕ_{1} is a sub-expression of an exceptional expression ĕ, then the α is determined by the context where T̆(ĕ) occurs, and so on.

Ṫ transforms normal expressions of type τ into expressions of the same type, except for one case: Ṫ always transform lambda-abstractions (λx. e and fix f λx. e) to receive continuations. This coercion is necessary when an exceptional application can execute a normal body, which is possible as follows. For an application ė_{1} ė_{2}, let us assume that two lambda-abstraction λx.ĕ and λy.ė can flow into ė_{1}. Because of the exceptional body ĕ the application expression can be marked exceptional, hence is transformed by T̆ to

λ⟨K, H⟩. Ṫ (ė_{1}) Ṫ (ė_{2}) ⟨K, H⟩.

Then it is necessary to coerce the other function λy. ė to expect continuations:

λy. λ⟨K, H⟩. K(Ṫ (ė)).

Because of this coercion, if an application e_{1} e_{2} is transformed we must always pass two continuations. In case of the normal transformation Ṫ (e_{1} e_{2}) we pass a dummy pair ⟨⊥_{K}, ⊥_{H}⟩. In case of the exceptional transformation T̆(e_{1} e_{2}) we pass the continuation pair ⟨K, H⟩ received from the context.

Note that even though the transformed program can still have raise expressions because of (λx. raise x), which is our ⊥_{H} function, such raise expressions are evaluated if and only if the input program raises exceptions that abort the program execution.

Let us consider several examples. Their basic theme is that an exceptional expression ĕ is transformed with T̆ to receive a pair of continuations, whereas a normal expression ė is transformed with Ṫ to yield its value in the usual direct style.

• Case of normal handle-expression whose first sub-expr-ession is exceptional:

Ṫ (handle ĕ_{1} κ λx. ė_{2}) =

T̆(ĕ_{1}) ⟨⊥_{K}, λv. case v κ ((λx. Ṫ (ė_{2})) v) (⊥_{H} v)⟩

The exceptional sub-expression ĕ_{1} is transformed with T̆ to receive two continuations. The normal continuation is the identity function ⊥_{K}, because the normal value of ĕ_{1} is the value of the handle expression. The handler continuation is a case expression that, if the exception v is unmatched, aborts the program by raising the exception (⊥_{H} v), and otherwise, handles it normally ((λx. Ṫ (ė_{2})) v). The abortion case takes place when ĕ_{1} raises an exception the program cannot handle.

• Similar case, but when the handle-expression is exceptional:

T̆(handle ĕ_{1} κ λx. ė_{2}) = λ⟨K, H⟩. T̆(ĕ_{1}) ⟨K, λv. case v κ K((λx. Ṫ (ė_{2})) v) (H v)⟩

The difference from the previous case is that the transformed expression expects continuations ⟨K, H⟩ from the context and uses them in defining continuations to pass to subexpression T̆(ĕ_{1}). Continuations to pass to T̆(ĕ_{1}) are defined using the continuations ⟨K, H⟩ passed from the context.

• Case of exceptional application-expression whose second expression is normal.

T̆(ĕ_{1} ė_{2}) = λ⟨K, H⟩. T̆(ĕ_{1}) ⟨λf. (f Ṫ (ė_{2}) ⟨K, H⟩), H⟩

The exceptional sub-expression ĕ_{1} is transformed with T̆ to receive two continuations. We pass two continuations to it: the normal continuation part λf. (f ...) is to apply the resulting function f to argument Ṫ (ė_{2}) with the current continuations ⟨K, H⟩, and the handler continuation part is the H from the context.

Theorem 3 (Correctness of Ṫ and T̆) For any program ℘,

℘ →^{∗} v  ⟹ Ṫ (Annotate(℘)) →^{∗} Ψ̇(v)
℘ →^{∗} \underline{κ·v} ⟹ Ṫ (Annotate(℘)) →^{∗} \underline{Ψ̇(κ·v)}

where the auxiliary function Ψ̇ coerces direct-style values to selective-CPS values:

Ψ̇(1) = 1
Ψ̇(κ·v) = κ·Ψ̇(v)
Ψ̇(λx. ė) = λx. λ⟨K, H⟩. K(Ṫ (e))
Ψ̇(λx. ĕ) = λx. T̆(e)
Ψ̇(fix f λx. ė) = fix f λx. λ⟨K, H⟩. K(Ṫ (e))
Ψ̇(fix f λx. ĕ) = fix f λx. λ⟨K, H⟩. K(T̆(e))

The proof uses the following three lemmas, which are analogous to those used in Plotkin’s simulation theorem [Plo75].

3The word “normal” is slightly misleading here because such an expression aborts the whole execution of the program—in fact, we replace it by an abort operation. But since this operation does not need to be passed any continuation, we can mark the expression as normal.

Lemma 1

\{ \begin{matrix}[Ψ̇(v)/x]Ṫ (ė) & = & Ṫ ([v/x]ė) \\ [Ψ̇(v)/x]T̆(ĕ) & = & T̆([v/x]ĕ) \end{matrix}

Proof. By induction on size of e. □

Now the following two lemmas prove two vital properties about the infix operator “:”, which is defined analogously to Plotkin’s one. (See Figure 12, in appendix, for the definition.) Particular to our case is the definition of e: Return, which denotes that the term e needs no continuations to finish.

For the proofs, we need to extend the Ṫ and T̆ functions, which were defined only for a program, to be defined also for all terms in the reduction sequence of the program:

\begin{aligned}Ṫ (κ·v) & = & Ψ̇(κ·v) \\ Ṫ (\underline{κ·v}) & = & \underline{Ψ̇(κ·v)} \\ T̆(v) & = & λ⟨K, H⟩. K(Ψ̇(v)) \\ T̆(\underline{κ·v}) & = & λ⟨K, H⟩. H(Ψ̇(κ·v)) \end{aligned}

Although our annotation is defined only for programs not for the terms that occur during reductions, we find it convenient in the proofs that the terms also have annotations inherited from their original expressions:

ė_{1}, e_{1} → e_{2} ; ė_{2}  ĕ_{1}, e_{1} → e_{2} ; ĕ_{2}

Lemma 2

\{ \begin{matrix}Ṫ (ė) & →^{+} & ė : Return \\ T̆(ĕ) ⟨K, H⟩ & →^{+} & ĕ: ⟨K, H⟩ \end{matrix}

Proof. By induction on size of e. □

Lemma 3

\{ \begin{matrix}ė → ė′ & ⟹ & e : Return →^{+} e′ : Return \\ ĕ → ĕ′ & ⟹ & e : ⟨K, H⟩ →^{+} e′ : ⟨K, H⟩ \end{matrix}

Proof.

• ė = handle\underline{κ̆·v_{1}} κ ė_{2} → [κ̆·v_{1}/x] ė_{2}

handle\underline{κ̆·v_{1}} κ ė_{2} : Return

= case Ψ̇(κ̆·v_{1}) κ (⊥_{K} (λx. Ṫ (ė_{2}) Ψ̇(κ̆·v_{1}))) (⊥_{H} Ψ̇(κ̆·v_{1})) (by def. of :)

→^{+} ⊥_{K} (λx. Ṫ (ė_{2}) Ψ̇(κ̆·v_{1}))

→^{+} [Ψ̇(κ̆·v_{1})/x] Ṫ (ė_{2})(by reduction rule) = Ṫ ([κ̆·v_{1}/x] ė_{2})(by Lemma1) = [κ̆·v_{1}/x] ė_{2} : Return(by Lemma2)

• ĕ = raise ė_{1} → raise\underline{v̇_{1}}

raise ė_{1} : ⟨K, H⟩ = H (ė_{1} : Return)(by def. of :) →^{+} H (\underline{v̇_{1}} : Return)(by I.H.) = H \underline{Ψ̇(v̇_{1})}(by def. of :)

→^{+} \underline{Ψ̇(v̇_{1})}(by reduction rule)

= raise\underline{v̇_{1}} : ⟨K, H⟩(by def. of :)

• ė = handle ė_{1} κ λx. ė_{2} → handle\underline{κ̇·v_{1}} κ λx. ė_{2} Impossible by annotation rule.

Other cases are similarly treated. □ It is now straightforward to prove Theorem 3: Proof. If ℘ →^{∗} v, then

Ṫ ( ˙℘) →^{+} ℘ : Return (by Lemma 2)
→^{∗} v  (by Lemma 3)
→ Ψ̇(v)  (by definition)

Similarly when ℘ →^{∗} \underline{κ·v}. □

6 Preliminary Experiments and Discussion

6.1 Sharing transducers

We tested our transformation for the subst function of Figure 2, i.e., a sharing transducer implementing substitution with exceptions. Figure 10 displays the transformed program, which results from our one-pass selective CPS transformer (à la Danvy and Filinski [DF92]).

Figure 11 shows (in solid line) that the transformed program can run with almost twice the speed of the original exception-based substitution program. As Graph (b) shows, if the program does not raise exceptions (hence handlers are not used) then the transformed program and the exceptionbased code run with about the same speed. Overall, the performance of the transformed program is actually nearing the performance of the CPS version (in dotted line) as specified in Figure 3, and which we consider as ideal.

6.2 Non exception-intensive programs

Our transformation’s assumptions that all exceptions are explicitly raised inside the program does not hold in reality because some exceptions (e.g., Overflow) can be raised from pre-defined functions (e.g., +). While the program can handle such primitive exceptions, the transformed version misses them because our transformer doesn’t see any raise expression which is transformed to activate the handler continuation. Thus our transformation must transform only such programs where uncaught exceptions from primitive functions are uncaught also inside the program. Meanwhile, if the input program has neither raise nor handle constructs, our transformation yields the same program.

6.3 More selective CPS transformations

We can tune our CPS transformation further. Currently, we transform every function (and application, respectively) to receive (to pass, respectively) two continuations. This blind transformation provides a simple solution to the “untypeful” flow situation where both normal and exceptional functions may flow into exceptional applications. Because of this situation, we need to coerce such normal functions to receive continuations. Since the coerced functions are also called at normal applications, we also coerce the normal applications to pass dummy continuations.

By classifying functions and applications more finely, we can reduce the traffic of such dummy continuations. Two cases occur for functions:

• Pure normal functions: normal functions which are always called in normal applications.

• Impure normal functions: normal functions which are called in exceptional applications.

exception same
fun subst_trans {1=x,2=e,3=body}
= let fun walk (VAR x') (k_var1,h_var2)
= (case x'=x
   of true => k_var1 e
    | false => h_var2 same)
| walk (LAM {1=x',2=body'}) (k_var1,h_var2)
= (case x'=x
   of true => h_var2 same
    | false => walk body' ((fn a_var5 => k_var1 (LAM {2=a_var5,1=x'})),
                           (fn b_var6 => h_var2 b_var6)))
| walk (APP {1=e0,2=e1}) (k_var1,h_var2)
= walk e0
       ((fn a_var14 => walk e1
                            ((fn a_var17 => k_var1 (APP {2=a_var17,1=a_var14})),
                             (fn b_var18 => ((fn same => k_var1 (APP {2=e1,1=a_var14})
                                               | a_var16 => raise a_var16)
                                             b_var18)))),
        (fn b_var15 => ((fn same => walk e1
                                         ((fn a_var10 => k_var1 (APP {2=a_var10,1=e0})),
                                          (fn b_var11 => h_var2 b_var11))
                          | a_var7 => h_var2 a_var7)
                        b_var15)))
in walk body ((fn a_var20 => a_var20),
      (fn b_var21 => ((fn same => body
                        | a_var19 => raise a_var19)
                      b_var21)))
end

Figure 10: The exception-based substitution of Figure 2 after selective CPS transformation

X coordinate: the input expression size. Y coordinate: execution time in ms, using SML/NJ 110 on a Sun UltraSPARC 2 (user time + system time + gc time).

(a) Exceptions are frequently raised.  (b) No exceptions are raised.

Figure 11: Experimental results for Figure 2 (−·−), Figure 3 (···), and Figure 10 (−)

Dually, two cases also occur for applications:

• Pure normal applications: all functions to call are pure normal functions.

• Impure normal applications: some functions to call are coerced normal functions.

Only impure normal functions must be coerced to receive continuations and only impure normal applications must be coerced to send dummy continuations.

The above finer classification is possible by adding the following two annotation rules to Figure 7: let \overline{ė} denote that ė is an impure normal expression.

λx.ė ∈ Closure analysis_{℘}(e_{1}) ĕ = e_{1} e_{2}
\overline{λx.ė}
\overline{λx.ė} ∈ Closure analysis_{℘}(e_{1}) ė = ė_{1} ė_{2}
\overline{ė_{1} ė_{2}}

A new transformation function can easily be defined to exploit this finer annotation.

Depending on the source programs, however, this finer transformation can offset the benefit of removing raise and handle expressions. In some cases, it may actually be preferable to keep some of them. Indeed, if a handler is installed long before a matching raise expression occurs, the CPStransformed intermediate expressions have the burden of carrying the two continuations for a long time. For such cases, we would better leave the handle and raise expressions intact. To this end, we are currently designing a static analysis that estimates the interval between a handler installation and its exception raise.

All such tunings of our selective CPS transformation are to be applied based on our experiments with realistic application programs (e.g., Isabelle, HOL, Knuth-bendix, etc.). Currently, our transformation is not compatible with separate compilation.

7 Conclusion

Processing ML exceptions forms an overhead. In SML/NJ, the overhead amounts to installing and uninstalling exception handlers in a global resource. In this work, we are exploring an alternative implementation based on a selective source-level CPS transformation. Instead of relying on one global stack of exception handlers, we pass to each function both its conventional continuation and a handler continuation accounting for exceptions. Furthermore, we reduce this continuation traffic using the static information provided by Yi and Ryu’s exception analysis [YR97]. We have implemented this selective CPS transformation for Standard ML’s core language and have integrated it as a separate phase in the SML/NJ compiler. (Hence our transformed programs are CPS-transformed yet again when they are compiled.) Our selective CPS transformation has been observed to improve the run times of exception-intensive programs by a factor of 2. As for programs where no exceptions are raised, it leaves them in direct style and their performance is thus the same as with SML/NJ. The more usual programs where exceptions are occasionally raised are the most challenging ones, since carrying continuations de facto forms a new overhead which is sometimes bigger than SML/NJ’s. We are currently investigating this last issue.

Acknowledgment

In a personal communication to the second author, Andrew Appel suggested that the results of the exception analysis could be exploited in reducing the overhead of raise/handle expressions. The present work originates from this suggestion. Thanks are also due to the anonymous referees for perceptive comments.

References

[App92] Andrew W. Appel. Compiling with Continuations. Cambridge University Press, New York, 1992.

[BCL^{+}98] Edoardo Biagioni, Ken Cline, Peter Lee, Chris Okasaki, and Chris Stone. Safe-for-space threads in Standard ML. Higher-Order and Symbolic Computation (née Lisp and Symbolic Computation), 11(2), 1998.

[DD95] Olivier Danvy and Dirk Dussart. CPS transformation after binding-time analysis. Unpublished note, Department of Computer Science, University of Aarhus, April 1995.

[DF92] Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, December 1992.

[DH93a] Olivier Danvy and John Hatcliff. CPS transformation after strictness analysis. ACM Letters on Programming Languages and Systems, 1(3):195– 212, 1993.

[DH93b] Olivier Danvy and John Hatcliff. On the transformation between direct and continuation semantics. In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Proceedings of the 9th Conference on Mathematical Foundations of Programming Semantics, number 802 in Lecture Notes in Computer Science, pages 627–648, New Orleans, Louisiana, April 1993. Springer-Verlag.

[Dus97] Dirk Dussart. Topics in program specialization and analysis for statically typed functional languages. PhD thesis, Katholieke Universiteit Leuven, Leuven, Belgium, May 1997.

[Fel87] Matthias Felleisen. The Calculi of λ-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Department of Computer Science, Indiana University, Bloomington, Indiana, August 1987.

[HD97] John Hatcliff and Olivier Danvy. Thunks and the λ-calculus. Journal of Functional Programming, 7(2):303–319, 1997.

[HM97] Nevin Heintze and David McAllester. Lineartime subtransitive control flow analysis. In Ron K. Cytron, editor, Proceedings of the ACM SIGPLAN’97 Conference on Programming Languages Design and Implementation, SIGPLAN

v : Return  = Ψ̇(v)
v : ⟨K, H⟩  = K ( Ψ̇(v) )
\underline{v} : Return  = \underline{Ψ̇(v)}
\underline{v} : ⟨K, H⟩  = H ( Ψ̇(v) )
ė_{1} ė_{2} : Return  = (e_{1} : Return) Ṫ (e_{2}) ⟨⊥_{K}, ⊥_{H}⟩
ė_{1} ė_{2} : ⟨K, H⟩  = (e_{1} : Return) Ṫ (e_{2}) ⟨K, H⟩
ĕ_{1} ė_{2} : ⟨K, H⟩  = e_{1} : ⟨λf. f Ṫ (e_{2}) ⟨K, H⟩, H⟩
ė_{1} ĕ_{2} : ⟨K, H⟩  =

(λf. T̆(e_{2}) ⟨λv. f v ⟨K, H⟩, H⟩)(e_{1} : Return)

ĕ_{1} ĕ_{2} : ⟨K, H⟩  =

e_{1} : ⟨λf. T̆(e_{2}) ⟨λv. f v ⟨K, H⟩, H⟩, H⟩

v_{1} ė_{2} : Return  = Ψ̇(v_{1}) (e_{2} : Return) ⟨⊥_{K}, ⊥_{H}⟩
v_{1} ė_{2} : ⟨K, H⟩  = Ψ̇(v_{1}) (e_{2} : Return) ⟨K, H⟩
v_{1} ĕ_{2} : ⟨K, H⟩  = e_{2} : ⟨λv. Ψ̇(v_{1}) v ⟨K, H⟩, H⟩
\underline{v_{1}} ė_{2} : Return  = \underline{Ψ̇(v_{1})}
\underline{v_{1}} ė_{2} : ⟨K, H⟩  = H ( Ψ̇(v_{1}) )
\underline{v_{1}} ĕ_{2} : ⟨K, H⟩  = H ( Ψ̇(v_{1}) )
v_{1} v_{2} : Return  = Ψ̇(v_{1})Ψ̇(v_{2}) ⟨⊥_{K}, ⊥_{H}⟩
v_{1} v_{2} : ⟨K, H⟩  = Ψ̇(v_{1})Ψ̇(v_{2}) ⟨K, H⟩
v_{1} \underline{v_{2}} : Return  = \underline{Ψ̇(v_{2})}
v_{1} \underline{v_{2}} : ⟨K, H⟩  = H ( Ψ̇(v_{2}) )

con κ ė : Return = con κ (e : Return)

con κ ĕ: ⟨K, H⟩ = e : ⟨λv. K ( κ·v ), H⟩

con κ v : Return = con κ Ψ̇(v)

con κ v : ⟨K, H⟩ = K ( Ψ̇(κ·v) )

con κ \underline{v} : Return = \underline{Ψ̇(v)}

con κ \underline{v} : ⟨K, H⟩ = H ( Ψ̇(v) )

decon ė : Return = decon (e : Return)

decon ĕ: ⟨K, H⟩ = e : ⟨λκ·v. K ( Ψ̇(v) ), H⟩

decon κ·v : Return = Ψ̇(v)

decon κ·v : ⟨K, H⟩ = K ( Ψ̇(v) )

decon\underline{v} : Return = \underline{Ψ̇(v)}

decon\underline{v} : ⟨K, H⟩ = H ( Ψ̇(v) )

raise ė : Return = ⊥_{H} (e : Return)

raise ė : ⟨K, H⟩ = H ( e : Return )
raise ĕ: ⟨K, H⟩ = e : ⟨H, H⟩

raise v : Return = ⊥_{H} Ψ̇(v)

raise v : ⟨K, H⟩ = H ( Ψ̇(v) )

raise\underline{v} : Return = \underline{Ψ̇(v)}

raise\underline{v̆} : ⟨K, H⟩ = H ( Ψ̇(v) )
raise\underline{v̇} : ⟨K, H⟩ = \underline{Ψ̇(v)}

                                                    handle ė_{1} κ λx. ė_{2} : Return = e_{1} : Return
                                                    handle ĕ_{1} κ λx. ė_{2} : Return =

e_{1} : ⟨⊥_{K}, λv. case v κ (⊥_{K} (λx. Ṫ (e_{2}) v)) (⊥_{H} v)⟩
handle ĕ_{1} κ λx. ė_{2} : ⟨K, H⟩ =
e_{1} : ⟨K, λv. case v κ (K (λx. Ṫ (e_{2}) v)) (H v)⟩
handle ĕ_{1} κ λx. ĕ_{2} : ⟨K, H⟩ =
e_{1} : ⟨K, λv. case v κ (λx. T̆(e_{2}) v ⟨K, H⟩) (H v)⟩
handle v_{1} κ λx. ė_{2} : Return = Ψ̇(v_{1})
handle v_{1} κ λx. ė_{2} : ⟨K, H⟩ = K ( Ψ̇(v_{1}) )
handle\underline{κ·v_{1}} κ λx. ė_{2} : Return = [Ψ̇(v_{1})/x]e_{2} : Return
handle\underline{κ′·v_{1}} κ λx. ė_{2} : Return = ⊥_{H}(Ψ̇(v_{1}))
handle\underline{κ·v_{1}} κ λx. ė_{2} : ⟨K, H⟩ = K([Ψ̇(v_{1})/x]e_{2} : Return)
handle\underline{κ′·v_{1}} κ λx. ė_{2} : ⟨K, H⟩ = H(Ψ̇(v_{1}))
handle\underline{κ·v_{1}} κ λx. ĕ_{2} : ⟨K, H⟩ = K([Ψ̇(v_{1})/x]T̆(e_{2}) ⟨K, H⟩)
handle\underline{κ′·v_{1}} κ λx. ĕ_{2} : Return = H(Ψ̇(v_{1}))

                                                    case ė_{1} κ ė_{2} ė_{3} : Return  =

case (ė_{1} : Return) κ Ṫ (ė_{2}) Ṫ (ė_{3})
case ė_{1} κ ė_{2} ĕ_{3} : ⟨K, H⟩  =
case (ė_{1} : Return) κ Ṫ (ė_{2}) T̆(ė_{3}) ⟨K, H⟩
case ė_{1} κ ĕ_{2} ė_{3} : ⟨K, H⟩  =
case (ė_{1} : Return) κ T̆(ė_{2}) ⟨K, H⟩ Ṫ (ė_{3})
case ĕ_{1} κ ė_{2} ė_{3} : ⟨K, H⟩  =
ĕ_{1} : ⟨λv. case v κ Ṫ (ė_{2}) Ṫ (ė_{3}), H⟩
case ė_{1} κ ĕ_{2} ĕ_{3} : ⟨K, H⟩  =
case (ė_{1} : Return) κ T̆(ė_{2}) ⟨K, H⟩ T̆(ė_{3}) ⟨K, H⟩
case ĕ_{1} κ ė_{2} ĕ_{3} : ⟨K, H⟩  =
ĕ_{1} : ⟨λv. case v κ Ṫ (ė_{2}) T̆(ė_{3}) ⟨K, H⟩, H⟩
case ĕ_{1} κ ĕ_{2} ė_{3} : ⟨K, H⟩  =
ĕ_{1} : ⟨λv. case v κ T̆(ė_{2}) ⟨K, H⟩ Ṫ (ė_{3}), H⟩
case ĕ_{1} κ ĕ_{2} ĕ_{3} : ⟨K, H⟩  =
ĕ_{1} : ⟨λv. case v κ T̆(ė_{2}) ⟨K, H⟩ T̆(ė_{3}) ⟨K, H⟩, H⟩

                                                    case κ·v_{1} κ ė_{2} ė_{3} : Return = ė_{2} : Return

case κ·v_{1} κ ė_{2} ė_{3} : ⟨K, H⟩ = ė_{2} : ⟨K, H⟩
case κ·v_{1} κ ĕ_{2} ė_{3} : ⟨K, H⟩ = ė_{2} : ⟨K, H⟩
case κ·v_{1} κ ė_{2} ĕ_{3} : ⟨K, H⟩ = K(ė_{2} : Return)
case κ·v_{1} κ ĕ_{2} ĕ_{3} : ⟨K, H⟩ = ė_{2} : ⟨K, H⟩

                                                    case κ′·v_{1} κ ė_{2} ė_{3} : Return = ė_{3} : Return

case κ′·v_{1} κ ė_{2} ė_{3} : ⟨K, H⟩ = ė_{3} : ⟨K, H⟩
case κ′·v_{1} κ ĕ_{2} ė_{3} : ⟨K, H⟩ = K(ė_{3} : Return)
case κ′·v_{1} κ ė_{2} ĕ_{3} : ⟨K, H⟩ = ĕ_{3} : ⟨K, H⟩
case κ′·v_{1} κ ĕ_{2} ĕ_{3} : ⟨K, H⟩ = ĕ_{3} : ⟨K, H⟩
case\underline{κ′·v_{1}} κ ė_{2} ė_{3} : Return = \underline{κ′·v_{1}}
case\underline{κ′·v_{1}} κ e_{2} e_{3} : ⟨K, H⟩ = K(\underline{κ′·v_{1}})

Figure 12: Definition of the infix operator ‘:’ Notices, Vol. 32, No 5, pages 261–272, Las Vegas, Nevada, June 1997. ACM Press.

[JW96] Suresh Jagannathan and Andrew Wright. Flowdirected inlining. In Proceedings of the ACM SIGPLAN’96 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 31, No 5, pages 192–205. ACM Press, May 1996.

[Plo75] Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

[Plo81] Gordon D. Plotkin. A structural approach to operational semantics. Technical Report FN-19, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, September 1981.

[Ses89] Peter Sestoft. Replacing function parameters by global variables. In Joseph E. Stoy, editor, Proceedings of the Fourth International Conference on Functional Programming and Computer Architecture, pages 39–53, London, England, September 1989. ACM Press.

[Shi91] Olin Shivers. Control-Flow Analysis of Higher-Order Languages or Taming Lambda. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, May 1991. Technical Report CMU-CS-91-145.

[SW94] Paul Steckler and Mitchell Wand. Selective thunkification. In Baudouin Le Charlier, editor, Static Analysis, number 864 in Lecture Notes in Computer Science, pages 162–178, Namur, Belgium, September 1994. Springer-Verlag.

[YR97] Kwangkeun Yi and Sukyoung Ryu. Towards a cost-effective estimation of uncaught exceptions in SML programs. In Pascal Van Hentenryck, editor, Static Analysis, number 1302 in Lecture Notes in Computer Science, pages 98–113, Paris, France, September 1997. Springer-Verlag.