François Pessaux
email: francois.pessaux@inria.fr

Xavier Leroy
email: xavier.leroy@inria.fr.

Type-based analysis of uncaught exceptions

This paper presents a program analysis to estimate uncaught exceptions in ML programs. This analysis relies on unification-based type inference in a non-standard type system, using rows to approximate both the flow of escaping exceptions (a la effect systems) and the flow of result values (a la control-flow analyses). The resulting analysis is efficient and precise; in particular, arguments carried by exceptions are accurately handled.

Introduction

Many modern programming languages such as Ada, Modula-3, ML and Java provide built-in support for exceptions: raising an exception at some program point transfers control to the nearest handler for that exception found in the dynamic call stack.

Exceptions provide safe and flexible error handling in applications: if an exception is not explicitly handled in a function by the programmer, it is automatically propagated upwards in the call graph until a function that "knows" how to deal with the exception is found. If no handler is provided for the exception, program execution is immediately aborted, thus pinpointing the unexpected condition during testing. This stands in sharp contrast with the traditional C-style reporting of error conditions as "impossible" return values (such as null pointers or the integer -1): in this approach, the programmer must write significant amount of code to propagate error conditions upwards; moreover, it is very easy to ignore an error condition altogether, often causing the program to crash much later, or even complete but produce incorrect results.

The downside of using exceptions for error reporting and as a general non-local control structure is that it is very easy to forget to catch an exception at the right place, i.e. to handle an error condition. ML compilers generate no errors or warnings in this case, and the programming mistake will only show up during testing. Exhaustive testing of applications is difficult, and even more so in the case of error conditions that are infrequent or hard to reproduce. Our experience with large ML applications is that uncaught exceptions are the most frequent mode of failure.

To address this issue, languages such as Modula-3 and Java require the programmer to declare, for each function or method, the set of exceptions that may escape out of it. Those declarations are then checked statically during type-checking by a simple intraprocedural analysis. This forces programmers to be conscious of the flow of exceptions through their programs.

Declaring escaping exceptions in functions and method signatures works well in first-order, monomorphic programs, but is not adequate for the kind of higher-order, polymorphic programming that ML promotes. Consider the map iterator on lists. In Modula-3 or Java, the programmer must declare a set E of exceptions that the function argument to map may raise; map, then, may raise the same exceptions E. But E is fixed arbitrarily, thus preventing map from being applied to functions that raise exceptions not in E. The genericity of map can be restored by taking for E the set of all possible exceptions, but then the precision of the exception analysis is dramatically decreased: all invocations of map are then considered as potentially raising any exception. (Similar problems arise in highly object-oriented Java programs using e.g. container classes and iterators intensively.) To deal properly with higher-order functions, a very rich language for exception declarations is required, including at least exception polymorphism (variables ranging over sets of exceptions) and arbitrary unions of exception sets. (See section 2 for a more detailed discussion.) We believe that such a complex language for declaring escaping exceptions is beyond what programmers are willing to put up with.

The alternative that we follow in this paper is to infer escaping exceptions from unannotated ML source code. In other terms, we view the problem of detecting potentially uncaught exceptions as a static debugging problem, where static analyses are applied to the programs not to make them faster via better code generation, but to make them safer by pinpointing possible run-time failures. This approach has several advantages with respect to the Modula-3/Java approach: it blends better with ML's type inference; it does not change the language and supports the static debugging of "legacy" applications; it allows the use of complex approximations of exception sets, as those need not be written by the programmer (within reason -the results of the analysis must still be understandable to the programmer). Finally, the exception inference needs not be fully compatible with the ML module system: a whole program analysis can be considered (again within reason -analysis time should remain practical).

Several exception analyses for ML have been proposed [START_REF] Guzmán | A type system for exceptions[END_REF][START_REF] Yi | An abstract interpretation for estimating uncaught exceptions in Standard ML programs[END_REF][START_REF] Yi | Towards a cost-effective estimation of uncaught exceptions in SML programs[END_REF][START_REF] Fähndrich | Program analysis using mixed term and set constraints[END_REF][START_REF] Fähndrich | Tracking down exceptions in Standard ML programs[END_REF], some based on effect systems, some on control-flow analyses, some on combinations of both (see section 6 for a detailed discussion). The analysis presented in this paper attempts to combine the efficiency of effect systems with the precision of flow analyses. It is based on unification and non-standard type inference algorithms that have excellent running time and we hope should scale well to large applications. At the same time, our analysis is still fairly precise; in particular, it approximates not only the names of the escaping exceptions, but also the arguments they carrya feature that is essential to analyze precisely many existing ML programs. This constitutes the main technical contribution of this paper: integrate in the same unification-based framework both approximation of exception effects in the style of effect systems [START_REF] Talpin | The type and effect discipline[END_REF], and approximation of sets of values computed at each program point in the style of flow analyses and soft typing [START_REF] Shivers | Control-Flow Analysis of Higher-Order Languages[END_REF][START_REF] Wright | A practical soft type system for Scheme[END_REF]. Finally, our analysis has been implemented to cover the whole Objective Caml language -not only core ML, but also datatypes, objects, and the module system. We present some preliminary experimental results obtained with our implementation.

The remainder of this paper is organized as follows. Section 2 lists the main requirements for an ML exception analysis. Section 3 presents the non-standard type system we use for exception analysis. Extension to the full Objective Caml language is discussed in section 4; experimental results obtained with our implementation, in section 5; and related work, in section 6. Concluding remarks can be found in section 7.

Design requirements

In this section, we list the main requirements for an effective exception analysis for ML, and show that they go much beyond what can be expressed by exception declarations in Modula-3 or Java. Existing exception analyses have addressed some of these requirements, but none addresses all.

Handling higher-order functions precisely

The exception behavior of higher-order functions depends on the exceptions that can be raised by their functional arguments. A form of polymorphism over escaping exceptions is thus needed to analyze higher-order functions precisely. Consider the map iterator over lists mentioned in introduction. An application map f l may raise whatever exception the f argument may raise. Writing τ ϕ → τ for the annotated type of functions from type τ to type τ whose set of potentially escaping exception is ϕ, the behavior of map is captured by the following annotated type scheme:

map : ∀α, β, ϕ. (α ϕ → β) ∅ → (α list ϕ → β list)
where α, β range over types and ϕ ranges over sets of exceptions. In general, the escaping exceptions for a higher-order function are combinations ϕ1 ∪. . .∪ϕn ∪{C1; . . . ; Cn} where the ϕi are variables representing the escaping exceptions for functional arguments and the Cj are exception constants. For instance, we have the following annotated type for function composition λf.λg.λx.f (g(x)):

∀α, β, γ, ϕ, ψ. (α ϕ → β) ∅ → (γ ψ → α) ∅ → γ ϕ∪ψ -→ β
Given the frequent use of higher-order functions in ML programs, an exception analysis for ML must handle them with precision similar to what the annotated types above suggest.

Similar issues arise when functions are stored into data structures such as lists or hash tables (as in callback tables for instance). The exception analysis should keep track of the union of the exceptions that can be raised by functions contained in the structure. It is not acceptable to say that any exception can be raised by applying a function retrieved from the structure.

Handling exceptions as first-class values

In ML and Java, exceptions are first-class values: exception values can be built in advance and passed through functions before being raised. Consider for instance the following contrived example: let test = λexn. try raise(exn) with E → 0

The exception behavior of this function is that test exn raises the exception contained in the argument exn, except when exn is actually the exception E, in which case no exception escapes out of test. We seek exception analyses precise enough to capture this behavior.

It is true that the first-class character of exception values is rarely, if ever, used in actual ML programs. However, there is one important idiom where an exception value appears: finalization. Consider:

let f = λx. try g(x)
with E → 0 | exn → finalization code; raise(exn)

Assuming g can raise exceptions E and E', the exception analyzer should recognize that the exn exception variable can only take the value E', thus the raise(exn) that reraises the exception after finalization can only raise E', and so does the function f itself.

Keeping track of exception arguments

ML exceptions can optionally carry arguments, just like all other data type constructors. This argument can be tested in the with part of an exception handler, using patternmatching on the exception value, so that only certain exceptions with certain arguments are caught. Consider the following example:

exception Failure of string let f = λx. if ... then ... else raise(Failure "f") let g = λx. try f(x) with Failure "f" → 0

An exception analysis that only keeps track of the exception head constructors (i.e. Failure above) but not of their arguments (i.e. the string "f" above) fails to analyze this example with sufficient precision: the analysis records that function f may raise the Failure exception, hence it considers that the application f(x) in g may raise Failure with any argument. Since the exception handler traps only Failure "f", the analyzer concludes that g may raise Failure, while in reality no exception can escape g. This lack of precision can be brushed aside as "unimportant" and "bad programming style anyway". Indeed, the programmer should have declared a specific constant exception Failure_f to report the error in f, rather than rely on the general-purpose Failure exception. However, code fragments similar to the example above appear in legacy Caml applications that we would like to analyze. More importantly, there are also legitimate uses of exceptions with parameters. For instance, the Caml interface to Unix system calls uses the following scheme to report Unix error conditions: This allows user code to trap all Unix errors at once (try ... with Unix_error(_) -> ...), and also to trap particular errors (try ... with Unix_error(ENOENT) -> ...). Replacing Unix_error by 67 distinct exceptions, one for each error code, would make the former very painful. It is desirable that the exception analysis be able to show that certain Unix_error exceptions with arguments representing common errors (e.g. Unix_error(ENOENT), "no such file") are handled in the program and thus do not escape, while we can accept that other Unix_error exceptions representing rare errors are not handled in the program and may escape.

The problem with exception arguments is made worse by the availability (in the Caml standard library at least) of predefined functions to raise general-purpose exceptions such as Failure above. Indeed, the example with Failure above is more likely to appear under the following form: exception Failure of string let failwith = λmsg. raise(Failure msg) let f = λx. if ... then ... else failwith("f") let g = λx. try f(x) with Failure "f" → 0 Precise exception analysis in this example requires tracking the string constant "f" not only when it appears as immediate argument to the Failure exception constructor, but also when it is passed to the function failwith. Hence the exception analysis must also include some amount of data flow analysis, not limited to exception values.

Running faster than control-flow analyses

All the requirements we have listed so far point towards control-flow analyses in the style of Shiver's k-CFA [START_REF] Shivers | Control-Flow Analysis of Higher-Order Languages[END_REF] or Heintze's SBA [START_REF] Heintze | Set-based analysis of ML programs[END_REF]. Control-flow analyses provide an approximation of the set of values that can flow to each program point. It is entirely straightforward to extend them to approximate also the set of escaping exceptions at each program point at the same time as they approximate the set of result values. Alternatively, the exception analysis can be run as a second pass of dataflow analysis exploiting the results of control-flow analysis [START_REF] Yi | Towards a cost-effective estimation of uncaught exceptions in SML programs[END_REF], although this results in some loss of precision, as the control flow can be determined more accurately if exception information is available. This exception analysis benefits from the relatively precise approximation of values provided by the control-flow analysis, especially as far as exception arguments are concerned.

Our first implementation of an exception analyzer for Objective Caml was indeed based on control-flow analysis: 0-CFA initially, then Jagannathan and Wright's "polymorphic splitting" [START_REF] Jagannathan | Polymorphic splitting: An effective polyvariant flow analysis[END_REF]. Our practical experience with this approach was mixed: the precision of the exception analysis was satisfactory (at least with polymorphic splitting), but the speed of the analysis left a lot to be desired. In particular, we observed quadratic behavior on several examples, indicating that the analysis would not scale easily to large programs1 . Although sophisticated techniques have been developed to speed up program analyses based of set inclusion constraints such as CFA and SBA [START_REF] Fähndrich | Making set-constraint based program analyses scale[END_REF][START_REF] Flanagan | Componential set-based analysis[END_REF][START_REF] Fähndrich | Partial online cycle elimination in inclusion constraint graphs[END_REF][START_REF] Pottier | A framework for type inference with subtyping[END_REF], it is still an open problem whether those analyses can scale to 100,000-line programs.

For these reasons, we decided to abandon analyses based on CFA or more generally set inclusion constraints, and settled for less precise but faster analyses based on equality constraints and unification.

A type system for exception analysis

In the style of effect systems [START_REF] Lucassen | Polymorphic effect systems[END_REF][START_REF] Talpin | The type and effect discipline[END_REF], our exception analysis is presented as a type inference algorithm for a nonstandard type system. The type system uses unified mechanisms based on row variables both to keep track of the effects (sets of escaping exceptions) of expressions and to refine the usual ML types by more precise information about the possible values of expressions. In this section, we present first the typing rules for our type system (that is, the specifications for the exception analysis), then type inference issues (the actual analysis).

The source language

The source language we consider in this paper is a simple subset of ML with integers and exceptions as the only data types, the ability to raise and handle exceptions, and simplified pattern-matching.

Terms:

a

::= x identifier | i integer constant | λx. a application | a1(a2) abstraction | let x = a1 in a2 the let binding | match a1 with p → a2 | x → a3 pattern-matching | C | D(a)
exception constr. | try a1 with x → a2 exception handler Patterns:

p ::= x variable pattern | i | C constant patterns | D(p) constructed pattern
The match a1 with p → a2 | x → a3 performs patternmatching on the value of a1; if it matches the pattern p, the branch a2 is evaluated; otherwise, a3 is evaluated. Multicase pattern matchings can be expressed by cascading match expressions. The try a1 with x → a2 construct evaluates a1; if an exception is raised, its value is bound to x and a2 is evaluated. There is no syntactic form for raising an exception; instead, we assume predefined a raise function in the environment. The try construct catches all exceptions; catching only a given exception C is performed by:

try a1 with x → match x with C → a2 | y → raise(y)
The dynamic semantics for this language is given by the reduction rules in figure 1, in the style of [START_REF] Wright | A syntactic approach to type soundness[END_REF]. Values, evaluation contexts, and evaluation results are defined as:

Values: v ::= i | C | D(v) | λx.a | raise Evaluation contexts: Γ ::= [ ] | Γ(a) | v(Γ) | D(Γ) | let x = Γ in a | match Γ with p → a2 | x → a3 | try Γ with x → a (λx.a)(v) ⇒ a{x ← v} let x = v in a ⇒ a{x ← v} match v with p → a2 | x → a3 ⇒ σ(a2) if σ = M (v, p) is defined match v with p → a2 | x → a3 ⇒ a3{x ← v} if M (v, p) is undefined try v with x → a2 ⇒ v (raise v)(a) ⇒ raise v (λx.a)(raise v) ⇒ raise v D(raise v) ⇒ raise v let x = raise v in a ⇒ raise v match raise v with p → a2 | x → a3 ⇒ raise v try raise v with x → a2 ⇒ a2{x ← v} Γ[a] ⇒ Γ[a ] if a ⇒ a
The pattern-matching function M (v, p):

M (v, x) = {x ← v} M (i, i) = id M (C, C) = id M (D(v), D(p)) = M (v, p)

The type algebra

The type system uses the following type algebra: Type expressions:

τ ::= α type variable | int[ϕ] integer type | exn[ϕ] exception type | τ1 ϕ → τ2
function type Type schemes:

σ ::= ∀αi, ρj, δ k .τ Rows:

ϕ ::= ρ row variable | all possible elements | ε; ϕ the element ε plus whatever is in ϕ Row elements:

ε ::= i : π integer constant | C : π constant exception | D(τ )
parameterized exception Presence annotations:

π ::= Pre element is present | δ presence variable
As in effect systems, our function types τ1 ϕ → τ2 are annotated by the latent effect ϕ of the function, that is, the set of exceptions that may be raised during application of the function. In addition, the base types exn[ϕ] and int[ϕ] are also annotated by sets of exceptions and integers respectively. Those sets refine the ML types exn and int by restricting the values that an expression of type exn[ϕ] or int[ϕ] can have.

Sets of exceptions or integers are represented by rows similar to those used for typing extensible records [START_REF] Wand | Complete type inference for simple objects[END_REF][START_REF] Rémy | Records and variants as a natural extension of ML[END_REF][START_REF] Rémy | Type inference for records in a natural extension of ML[END_REF]. A row is either , meaning that all values of the type are possible (we do not have any more precise information), or a sequence of row elements ε1 . . . εn terminated by a row variable ρ. We impose the following equational theory on rows to express that the order of elements in a row does not matter (equation 1), and that is absorbing (equation 2):

ε1; ε2; ϕ = ε2; ε1; ϕ (1) i : Pre; = (2)
The absorption equation 2 applies only to integer row elements because we intend to be used only in rows annotating the int type. (The kinding rules below enforce this invariant.) A symbol is required for base types such as int, which have an infinite (or at least very large) signature. It is not required for datatypes such as exn, which have a finite signature: a row enumerating all possible constructors can be used instead (this is discussed in section 4.1.4 below). Moreover, combining and rows containing parameterized constructors raises technical problems 2 ; we prefer to avoid the difficulty by restricting to rows containing only integer elements.

Rows and row variables support both polymorphism over sets and a form of set union in a unification framework. For instance, the two rows ε1; ρ1 and ε2; ρ2, which informally represent the sets {ε1} and {ε2} respectively, unify into the row ε1; ε2; ρ representing the set {ε1; ε2} via the substitution {ρ1 ← (ε2; ρ); ρ2 ← (ε1; ρ)}.

A row element ε is either an integer constant i, a constant exception constructor C, or a parameterized exception constructor D(τ ) carrying the annotated type τ of its argument. To maintain crucial kinding invariants (see below), 2 The obvious absorption equation D(τ ); = is unsound, as it allows deductions such as D(α); = = D(β); , which lead to inconsistent typings. If ML had subtyping and a supertype of all types, a correct equation would be D( ); = . This equation allows to absorb any D(τ ) (because D(τ ); <: D( ); = ), but only allows expansion of into D( ); , meaning correctly that no information is available on the argument of D.

ρ 2 → int[ρ3] ρ 4 → int[ ]
(no effects, no information known on the return value).

The type scheme ∀ρ. int[1 : Pre; 2 : Pre; ρ] stands for the set {1; 2} and is the type of integer expressions that can only evaluate to 1 or to 2. A universally quantified row variable ρ that occurs only positively in a type should be read as denoting the empty set of elements, for the same reasons that ∀α.α denotes an empty set of values.

The type scheme ∀ρ, δ. int[1 : δ; 2 : Pre; ρ] stands for the set {2}. Although 1 is mentioned in the row, it should not be considered present in the set, since its presence annotation δ is universally quantified and occurs only positively.

The type scheme ∀ρ, ρ . exn[D(int[3 : Pre; 4 : Pre; ρ]); ρ ] stands for the set of exceptions {D(3); D(4)}.

The raise predefined function has the following type scheme: ∀α, ρ. exn[ρ] ρ → α. It expresses that an application of raise never returns and raises exactly the exceptions that it receives as argument.

Kinding of rows: To simplify the formulation of the typing rules and to ensure the existence of principal unifiers and principal typings, we require the following four structural invariants on rows:

1. A given integer constant or exception constructor should occur at most once in a row (for instance, (D(τ ); D(τ ); ϕ) is not well-formed).

2. A row variable ρ is preceded by the same set of integer constants and exception constructors in all row expressions where it occurs (for instance, we cannot have both (1 : Pre; ρ) and (2 : Pre; ρ) in the same derivation).

3. A row ϕ annotating an integer type int[ϕ] can only contain integer elements i. Invariants (1) and ( 2) are well known from earlier work on record types [START_REF] Rémy | Type inference for records in a natural extension of ML[END_REF]. Invariants (3) and ( 4) are more unusual. They ensure a clear separation between annotations of int types (composed of integer elements and possibly ) and annotations of the exn types (composed of constructors and no ). Since absorbs only integer elements (equation 2), we do not want it to occur in rows containing exception constructors C, D.

Following [START_REF] Rémy | Type inference for records in a natural extension of ML[END_REF][START_REF] Ohori | A polymorphic record calculus and its compilation[END_REF], we use kinds to enforce the invariants above. Our kinds κ are composed of a tag (either INT or EXN) and a set of constants and constructors:

κ ::= INT({i1, . . . , in}) | EXN({C1, . . . , Cp, D1, . . . , Dq})
The constants and constructors appearing in the set part of a kind are those constants and constructors that must not appear in rows of that kind (because they already appear in elements concatenated before those rows). We assume given a global mapping K assigning kinds to row variables, and such that for each κ there are infinitely many variables of that kind (i.e. K -1 (κ) is infinite). The kinding rules are shown in figure 2. They define the two judgements ϕ :: κ (row ϕ has kind κ) and τ wf (type τ is well-formed).

The typing rules

Figure 3 shows the typing rules for our system. They define the judgement E a : τ /ϕ, where E is the typing environment, a the term to type, τ the type of values that a may evaluate to, and ϕ the set of exceptions that may escape during the evaluation of a. All types appearing in the rules are assumed to be well-kinded. We assume that typing starts in the initial environment E0 = {raise : ∀α, ρ. exn[ρ] ρ → α}. The rules for variables and let bindings (rules 1 and 5) are standard, except that we generalize over all three kinds of type variables. For variables as well as other language constructs that never raise exceptions (rules 1, 2, 3, 7), the ϕ component of the result is unconstrained and can be chosen as needed to satisfy equality constraints in the remainder of the typing derivation.

The rules for function abstraction and application (rules 3 and 4) are the usual rules for effect systems. For abstraction, the effect of the function body becomes the latent effect of the function type. For application a1(a2), we require that the same set ϕ of exceptions occurs as effect of a1, latent effect of the function denoted by a1, and effect of a2. This corresponds in our unification setting to taking the union of those three effects.

Typing of expressions:

τ ≤ E(x) E x : τ (1) ϕ :: INT({i}) ϕ :: EXN(∅) E i : int[i : Pre; ϕ ]/ϕ (2)
τ1 wf E ⊕ {x : τ1} a : τ2/ϕ ϕ :: EXN(∅)

E λx. a : (τ1 ϕ → τ2)/ϕ (3) E a1 : (τ ϕ → τ )/ϕ E a2 : τ /ϕ E a1(a2) : τ /ϕ (4) E a1 : τ1/ϕ E ⊕ {x : Gen(τ1, E, ϕ)} a2 : τ /ϕ E let x = a1 in a2 : τ /ϕ (5) E a1 : τ1/ϕ p : τ1 ⇒ E τ1 -p Y τ2 E ⊕ E a2 : τ /ϕ E ⊕ {x : τ2} a3 : τ /ϕ E match a1 with p → a2 | x → a3 : τ /ϕ (6)
E a1 : τ /ϕ E ⊕ {x : exn[ϕ ]} a2 : τ /ϕ E try a1 with x → a2 : τ /ϕ (9)
Typing of patterns:

x : τ ⇒ {x : τ } (10) i : int[i : Pre; ϕ] ⇒ {} (11) C : exn[C : Pre; ϕ] ⇒ {} (12) τ ≤ TypeArg(D) p : τ ⇒ E D(p) : exn[D(τ ); ϕ] ⇒ E (13)
Pattern subtraction:

τ wf τ -x Y τ (14) int[i : Pre; ϕ] -i Y int[i : π; ϕ] (15) exn[C : Pre; ϕ] -C Y exn[C : π; ϕ] (16) τ -p Y τ exn[D(τ ); ϕ] -D(p) Y exn[D(τ ); ϕ] (17)
Instantiation and generalization:

τ ≤ ∀αiρjδ k . τ iff there exists τi, ϕj, π k such that τ = τ {αi ← τi, ρj ← ϕj, δ k ← π k } and τi wf and ϕj :: K(ρj).

Gen(τ, E, ϕ) is ∀αiρjδ k . τ where {αi, ρj, δ k , } = F V (τ ) \ (F V (E) ∪ F V (ϕ)).
Figure 3: The typing rules

For integer constants and exception constructors (rules 2, 7 and 8), we record the actual value of the expression in the approximation part of the type int or exn. For instance, the type of i must be of the form int[i : Pre; ϕ], forcing i : Pre to appear in the type of the expression. In rules 8 and 13, we write TypeArg(D) for the type scheme of the argument of constructor D, e.g. TypeArg(D) = ∀ρ. int[ρ] for an integervalued exception D.

For an exception handler try a1 with x → a2 (rule 9), the effect ϕ1 of a1 is injected in the type exn[ϕ1] assumed for x in a2.

The most interesting rule is rule 6 for the match construct. This rule is crucial to the precision of our exception analysis. When typing match a1 with p → a2 | x → a3, we want to reflect the fact that the second alternative (x → a3) is selected only when the first alternative (p → a2) does not match the value of a1. In other terms, the type of values that can "flow" to x in the second alternative is not the type of the matched value a1, but the type of a1 from which we have excluded all values matching the pattern p in the first alternative.

To achieve this, rules 14-17 define the pattern subtraction predicate τ -p Y τ , meaning that τ is a correct type for the values of type τ that do not match pattern p. For a variable pattern p = x (rule 14), all values match the pattern, so it is correct to assume any τ for the type of the non-matched values. For an integer pattern p = i (rule 15), we force τ to unify with int[i : Pre; ϕ], thus exposing in ϕ the set of all possible values of type τ that are different from i. Then, we take τ = int[i : π; ϕ] for a suitable π. In particular, if that π is unconstrained in the remainder of the derivation, we can take π to be a fresh presence variable δ, thus reflecting that i is not among the possible values of type τ . The rules for exception patterns (rules 16 and 17) are similar. If the exception has an argument, instead of changing a presence annotation, we recursively subtract in the type of the argument of the exception.

It is easy to see that the typing rules preserve the kinding invariants: if E is well-kinded and E a : τ /ϕ, then τ wf and ϕ :: EXN(∅).

Examples of typings

We now show some typings derivable in our system. These are principal typings identical to those found by our exception analyzer. Consider first a simple handler for one Thus we conclude as before that no exception escapes this expression.

For a representative example of higher-order functions, consider function composition:

let compose = λf. λg. λx. f(g(x)) in compose (λy. 0) (λz. raise(C)) 1
The type scheme for compose is ∀α, β, γ, ρ, ρ1, ρ2. (α Finally, here is an (anecdotal) example that is ill-typed in ML, but well-typed in our type system due to the refined typing of pattern-matching:

ρ → β) ρ 1 → (γ ρ → α)
match 1 with x -> x | e -> raise e
Since the first case of the matching is a catch-all, rule 6 lets us assign the type exn[ρ ] for a fresh ρ to the variable e bound by the second case, even though the matched value is an integer. Hence the expression is well-typed, and moreover we obtain that it has type int[1 : Pre; ρ] and raises no exceptions (its effect is ρ for any ρ ).

Type soundness and correctness of the exception analysis

We now establish the correctness of our exception analysis: all uncaught exceptions are predicted by our effect system. This property is closely connected to the type soundness of our system.

Theorem 1 (Subject reduction) Reduction preserves typing: if E0 a : τ /ϕ and a ⇒ a , then E0 a : τ /ϕ

The proof of subject reduction is mostly standard and follows [START_REF] Wright | A syntactic approach to type soundness[END_REF] closely. Detailed proofs of the statements in this paper can be found in the technical report [START_REF] Leroy | Type-based analysis of uncaught exceptions[END_REF]. A key lemma is the following property of pattern subtraction: v : τ /ϕ for some D, v , τ , ϕ . In either case, the uncaught exception v is correctly predicted in the effect ϕ.

Type soundness for our non-standard type system follows from the subject reduction property and the following lemma showing that well-typed expressions either reduce to a value or to an uncaught exception, or loop, but never get "stuck".

Lemma 4 (Progress) If E0

a : τ /ϕ, then either a is a value v, or a is an uncaught exception raise v, or there exists a such that a ⇒ a .

Principal types and inference of types and exceptions

Just like the ML type system, our type system admits principal types, which can be computed by a simple extension of Milner's algorithm W , thus implementing the exception analysis.

Theorem 5 (Principal unifiers) The set of well-kinded types modulo equations ( 1) and ( 2) admits principal unifiers. More precisely, there exists an algorithm mgu that, for all system Q of well-kinded equations between types, either returns a substitution µ that is a principal solution of Q, or fails, meaning that Q has no solution. Moreover, the substitution µ preserves kinds in the following sense: for all α, µ(α) wf and for all ρ, µ(ρ) :: K(ρ).

In the theorem above, systems of well-kinded equations are sets Q = {τi = τ i ; ϕj = ϕ j ; π l = π l } of equations between types, rows, row elements, and presence annotations such that for all i, τi wf and τ i wf, and for all j, there exists a kind κj such that ϕj :: κj and ϕ j :: κj.

The existence of principal unifiers follows from the fact that our equational theory is syntactic and regular [START_REF] Rémy | Syntactic theories and the algebra of record terms[END_REF]. The algorithm mgu is given in appendix A.

Theorem 6 (Principal types) There exists a type inference algorithm W satisfying the following conditions:

• (Correctness) If E is well-kinded and (τ, ϕ, θ) = W (E, a) is defined, then θ(E) a : τ /ϕ.

• (Completeness) If E is well-kinded and there exists a kind-preserving substitution θ and types τ , ϕ such that θ (E) a : τ /ϕ , then (τ, ϕ, θ) = W (E, a) is defined and there exists a substitution ψ such that τ = ψ(τ ) and ϕ = ψ(ϕ) and θ (v) = ψ(θ(v)) for all type, row or presence variable v not used as a fresh variable by algorithm W .

The algorithm W is shown in appendix B.

Extension to the full Objective Caml language

In this section, we discuss the main issues in extending the analysis presented in section 3 to deal with the whole Objective Caml language [START_REF] Leroy | The Objective Caml system. Software and documentation available on the Web[END_REF].

Datatypes

User-defined datatypes (sum types) can be approximated in several different ways, depending on the desired trade-off between precision and speed of the analysis. We have considered the four approaches listed below (from most precise to least precise).

Full approximation of datatypes

The first approach applies to datatypes the same treatments as for exceptions: we annotate the type by a row ϕ approximating the possible values of that type, as constant constructors with presence annotations, and unary constructors with types of arguments. Consider the source-level datatype definition

type α t = C1 | . . . | Cn | D1 of µ1 | . . . | Dm of µm
where the µi are unannotated ML types. The propagation of approximations is captured by the following type schemes assigned to the constructors Ci and Di:

Ci : ∀ α, ρ . α t[Ci : Pre; ρ ] Di : ∀ α, ρ, ρ , ρ . τi ρ → α t[Di(τi); ρ ]
where τi is the annotated type obtained from µi by adding distinct fresh row variables taken from ρ on every type constructor that carries a row annotation. For instance, given the declaration

type intlist = Nil |

"Looped" approximations for recursive datatypes

The approximation scheme described above has the undesirable side-effect of recording in the type approximation the whole structure of a data structure given in extension. If the data types involved are recursive, we may end up with very large type approximations. Continuing the intlist example above, consider the expression n = Cons(i1, Cons(i2, . . . , Cons(in, Nil) . . .)). With the type of Cons given above, this expression is given an annotated type that is of depth n and records not only the fact that the list contains the integers i1 . . . in (an information that might be useful to analyze exceptions), but also the fact that the list has length n and that its first element is i1, the second i2, etc. The latter piece of information is, on practical examples, useless for analyzing exceptions. Moreover, such large approximations slow down the analysis. A solution to this problem comes from the following remark: as soon as one of those big data structures given in extension is passed to a sufficiently complex function, its big, unfolded annotated type is going to be unified with a recursive type, forcing all the information in the big type to be folded back into a smaller recursive type. For instance, if we pass the list n to the tail function shown above, the type of the list will be unified into τn = µα. intlist[Cons(int[i1 : Pre; . . . ; in : Pre; ρ1] × α);

Nil : Pre; ρ2]
The idea, then, is to force this folding into a recursive type when the data structure is created, by giving recursive, prefolded types to the data type constructors. This is easily achieved by unifying, in the type of the constructors, all occurrences of the recursively-defined type in argument position with the occurrence of the recursively-defined type in result position. For instance, in the case of the Cons constructor of type intlist, we start with the type

int[ρ1] × intlist[ρ2] ρ 3 → intlist[Cons(int[ρ1] × intlist[ρ2]); ρ4]
as in the previous section, then unify the two underlined intlist types, then generalize the free variables, obtaining Cons : ∀ρ1, ρ3, ρ4. int[ρ1] × τ This technique of "looping" the types of constructors also works for parameterized datatypes, as long as they are regular (the data type constructor is used with the same parameters in the argument types of the constructors). For non-regular datatypes such as type 'a nreg = Leaf of 'a | Node of 'a list nreg the unification of the occurrences of t in the type of Node would render that constructor essentially useless. Fortunately, such non-regular data types are extremely rare in actual programs, so we can use full approximations for them without impacting performance.

Adding row parameters to datatypes

An alternative to annotating datatype constructors with rows is to add row parameters to the type constructor reflecting the row annotations on exn, int and function types contained within the datatype. This technique is used by Fähndrich et al [START_REF] Fähndrich | Tracking down exceptions in Standard ML programs[END_REF]. For instance, the ML datatype definition

type t = A of int | B of exn | C of t | D of t is turned into type (ρ1, ρ2) t = A of int[ρ1] | B of exn[ρ2] | C of (ρ1, ρ2) t | D of (ρ1, ρ2) t
Two parameters ρ1 and ρ2 were added in order to reflect in the type t the possible values of types int and exn contained in that type. The type t itself is not annotated by a row recording which constructors A, B, C and D are present in values of that type. The net effect is to forget the structure of terms of type t, while correctly remembering the integers and exception values contained in the structure.

In practice, this solution appears to be slightly less precise and slightly more efficient than full approximations of non-recursive datatypes and looped approximations of recursive datatypes: type expressions are smaller, but in the case of t above, looped approximations can express the fact that a value of type t lack one of the constructors C or D, while this is not captured in the solution based on extra row parameters.

On datatypes that are not annotated by a row, we can no longer perform type subtraction during pattern-matching, since we have no approximation on the structure of values of that type. Hence, we simply consider that subtraction is the identity relation on those datatypes.

Datatypes without any approximations

For maximal speed and minimal precision, we can put no annotations at all on a datatype (neither a row approximation nor extra row parameters). This way, we forget not only the structure of values of that type, but also the exceptions, functions and base values contained in that type. Of course, this forces us to make very pessimistic assumptions on values extracted from a datatype without approximation. For instance, if we extract an integer by pattern-matching on such a datatype, we must give it type int[ ] since it can really be any integer. This is reflected in the types of constructors by putting annotations on all annotated types in the constructor argument. In the intlist example above, if we choose not to annotate intlist at all, we must give its constructors the following types:

Nil : intlist Cons : ∀ρ1. int[ ] × intlist ρ 1 → intlist
This approach assumes that we have annotations for all types, while the type system from section 3 only has for type int. However, we can allow to annotate other base types such as float and string. For exceptions and other datatypes, since there are finitely many constructors, we can use a (potentially recursive) row enumerating all constructors of the datatype instead of a built-in constant . In the case of lists, for instance, we can use the following "top row" Tlist(α, ρ):

Tlist(α, ρ) = µρ . Nil : Pre; Cons(α × α list[ρ ]); ρ
The annotated type τ list[Tlist(τ, ρ)] correctly represents any list of elements of type τ .

The "no approximation" approach described in this paragraph may look excessively coarse, but is actually quite effective for datatypes that introduce no base types, exception types, nor function types. Prominent examples are the builtin ML types α list and α array, where the α parameter already records all the information we need about list and array elements. For instance, a list of functions from integers to booleans has type (int[ϕ1]

ϕ 2 → bool[ϕ3]
) list, where ϕ2 denotes the union of the effects of all functions present in the list. A function extracted from that list and applied has effect ϕ2, and not any exception as one might naively expect.

Choosing a datatype approximation

The choice between the four datatype analysis strategies described above can be done on a per-datatype basis, depending on the shape of the datatype definition. We have considered several simple heuristics to perform this choice. Our first prototype used full approximations for non-parameterized datatypes, and no approximations for parameterized datatypes. Our current prototype uses full approximations for non-recursive or non-regular datatypes, looped approximations for recursive datatypes, and no approximations for built-in types without interesting structure (arrays and floating-point numbers, for instance). Another factor that we plan to integrate in the heuristic is whether the datatype introduces any exception type, function type, or base type likely to be an exception argument (string and int, essentially); if not, we could favor the "no approximation" approach.

Tuples and records

Tuple types are not approximated specially: each component of the tuple type carries its own annotation. For instance, int[1 : Pre; 2 : Pre; ρ] × int[3 : Pre; 4 : Pre; ρ ] stands for the set of four pairs {1; 2} × {3; 4}. Pattern subtraction on tuple types is not pointwise subtraction, which would lead to incorrect results.

Consider the type int[1 : Pre; ρ] × int[2 : Pre; 3 : Pre; ρ ]. Subtracting pointwise the pattern (1, 2) from this type would lead to type int[1 : δ; ρ] × int[2 : δ ; 3 : Pre; ρ ], which is incorrect since the value (1, 3) is no longer in the set. Therefore, the current implementation perform no subtraction on tuples: we take (τ1 × τ2) -(p1, p2) Y τ1 × τ2. For a more refined behavior, we could perform subtraction on one of the components if all other components are matched against catch-all patterns. For instance, we could take

(τ1 × τ2) -(p1, x2) Y τ 1 × τ2 if τ1 -p1 Y τ 1 .
Unlike in SML, records in Caml are declared and matched by name. We analyze them like datatypes, by annotating the name of the record type by a row of a particular form. The row contains exactly one element recording the annotated type of every field. Pattern subtraction for record types behaves as in the case of tuples.

To summarize, the extended type algebra for datatypes, tuples and records is as follows: This results in a precise approximation of mutable data. For instance, an array of functions has type (τ1 ϕ → τ2) array, where ϕ is the union of the latent effects of all functions stored in the array. In contrast, control-flow analyses would lose track of which functions are stored in the array, and thus also of the exceptions they may raise, unless supplemented by a region (aliasing) analysis.

Objects and classes

Because our system already uses recursive types, OCamlstyle objects do not add significant complexity to our framework. We just need to extend the type algebra with object types, that is, polymorphic records of methods [START_REF] Rémy | Objective ML: A simple object-oriented extension of ML[END_REF]. The type of each method is annotated by its latent effect. No extension to rows and row elements are needed. Since there are no object patterns in pattern-matching, pattern subtraction needs not be modified.

The OCaml class language interferes very little with the exception analysis. No significant modifications to the class type-checker are needed.

Modules and functors

Structures are assigned annotated signatures containing annotated types for the value components. Type abbreviations are currently handled by systematic expansion of their definitions 3 .

For matching a structure S against a signature Σ, there are two possible semantics. The opaque semantics says that the only things known about the restriction (S : Σ) is what Σ publicizes. In our case, since user-provided signatures Σ contain no annotations, this amounts to forgetting the result of the analysis of S and assume annotation on all value components of the restricted structure. The transparent semantics simply check that S matches Σ, but the restriction (S : Σ) retains all information known about S. We implemented the transparent semantics, as the opaque semantics results in too much information loss. (The opaque semantics also precludes choosing datatype annotations based on the definition of the datatype.) Similar problems arise with functors. All is known about the parameter of a functor is its syntactic signature. Hence, a naive analysis would assume annotation on all components of the functor argument. For better precision, one could use techniques based on conjunctive types such as [START_REF] Shao | Smartest recompilation[END_REF]. Other issues with functors are still unclear, such as the generativity of exception declaration in functor bodies, and the impact of the "exception polymorphism" offered by functors (a functor can take one or several exceptions as arguments, and have a different exception behavior depending on whether those arguments are instantiated later with identical or different exceptions).

For simplicity, we chose not to analyze functors when they are defined, but instead expand the functor body at each application and re-analyze the β-reduced body. Although this transformation increases the size of the analyzed source, the Caml programs we are interested in do not use functors intensively and this simple approach to analyzing functors works well in practice.

Separate analysis

Transparent signature matching precludes "true" separate analysis (where any module can be analyzed separately knowing only the syntactic signatures of the modules it imports). We can still do "bottom-up" separate analysis, however: a module can be analyzed separately provided the implementations of its imports have been analyzed already, and their annotated signatures inferred.

Since annotated signature for a module may contain free row variables (e.g. if the module defines mutable structures), separately analyzing several clients of that module may result in independent instantiations of those free variables. Those instantiations are recorded in the result of the analysis of each module, and reconciled in a final "linking" pass before displaying the results of the analysis.

Polymorphic recursion

Polymorphic recursion as introduced by Mycroft [17] is not needed to type-check the source OCaml language, but is desirable to enhance the precision of our exception analyzer. With ML-style monomorphic recursion, we obtain false positives on functions that recursively call themselves inside a try. . . with. Consider:

let rec f = λx. try f(x) with C → () | y → raise y
The latent effect inferred for f is C; ρ because the effect of f(x) is unified with the type of the pattern C at a time where the type of f is not yet generalized. With polymorphic recursion, we can assign f the type scheme ∀α, ρ. α ρ → unit both outside and inside the recursion; it is a fresh instance of that type scheme that gets unified with the type of C, thus not polluting the type scheme of f.

Although type inference with polymorphic recursion is undecidable [START_REF] Kfoury | Type reconstruction in the presence of polymorphic recursion[END_REF], there exists incomplete inference algorithms that work very well in practice. We experimented with Henglein's algorithm [START_REF] Henglein | Type inference with polymorphic recursion[END_REF] and with a home-grown algorithm based on restricted fixpoint iteration and obtained good results.

Experimental results

In this section, we present some experimental results obtained with our implementation. Currently, our analyzer implements all extensions described in section 4 except objects 4 . The analyzer is compiled with the OCaml 2.00 native-code compiler and runs on a Pentium II 333 Mhz workstation under Linux. Analysis speed: Figure 4 gives timings for the analysis of various small to medium-sized OCaml programs. We give timings both without and with polymorphic recursion. For comparison, we also give the time OCaml takes to parse and type-check those programs. (The timings given include parsing and pre-processing as well as analysis time.)

The overall performances are quite good, in the order of 1000-2000 lines of source per second. Programs that contain large data structures given in extension (Nucleic, Docteur) take longer to analyze due to the large size of the rows annotating the types of those data structures. On average, the exception analysis takes twice as much time as OCaml type inference; the ratio ranges between 1 (on simple programs) and 8 (on Docteur, because of the large constant data structures). Polymorphic recursion slows down the analysis somewhat on the largest benchmarks, but the slowdown remains acceptable compared with the increase in precision.

Precision of the analysis:

We have manually inspected the output of the analyzer on our benchmark programs. Programs 1, 3, 4, 5 and 7 have a relatively simple exception behavior, and our analysis reports exact results for those programs: there are no false positives except run-time errors such as "division by zero" or "array index out of bounds", which require extra analyses (or even general program proof) to show that they cannot occur.

For Knuth-Bendix, which has a quite complicated exception structure, 8 exceptions (Failure with 8 different string arguments) appearing in the source are correctly reported as non-escaping; 7 exceptions (one Invalid_argument and 6 Failure) are reported as potentially escaping, and can actually occur in some circumstances. Without polymorphic recursion, the analysis reports two false positives (one Not_found and one Failure), which correspond to recursive functions containing try . . . with around recursive calls. Adding polymorphic recursion as discussed in section 4.7 removes one of those false positives. The other one is still there, because our incomplete inference algorithm for polymorphic recursion fails to give a type polymorphic enough to one of the functions. A more precise algorithm such as Henglein's [START_REF] Henglein | Type inference with polymorphic recursion[END_REF] would probably eliminate the other false positive as well.

The larger examples 8 and 9 exhibit another source of false positives: mutable data structures (references and arrays) containing functions. As mentioned in section 4.3, the row variables appearing in approximations of mutable data structures are not generalized, hence "collect" all exceptions at their use sites. For instance: Several exception analyses for ML are described in the literature. Guzmán and Suárez [START_REF] Guzmán | A type system for exceptions[END_REF] develop a simple type and effect system to keep track of escaping exceptions. Their system does not handle exceptions as first-class values, nor exceptions carrying arguments. The first exception analysis proposed by Yi [START_REF] Yi | An abstract interpretation for estimating uncaught exceptions in Standard ML programs[END_REF] is based on general abstract interpretation techniques, and runs too slowly to be usable in practice. Later, Yi and Ryu [START_REF] Yi | Towards a cost-effective estimation of uncaught exceptions in SML programs[END_REF] developed a more efficient analysis roughly equivalent to a conventional control-flow analysis to approximate the call graph and the values of exceptions, followed by a data-flow analysis to estimate uncaught exceptions.

Fähndrich and Aiken [START_REF] Fähndrich | Program analysis using mixed term and set constraints[END_REF][START_REF] Fähndrich | Tracking down exceptions in Standard ML programs[END_REF] have applied their BANE toolkit for constraint-based program analyses to the problem of analyzing uncaught exceptions in SML. Their system uses a combination of inclusion constraints (as in controlflow analyses) to approximate the control flow, and equality constraints (unification) between annotated types to keep track of exception values.

To compare performances between [START_REF] Yi | Towards a cost-effective estimation of uncaught exceptions in SML programs[END_REF], [START_REF] Fähndrich | Program analysis using mixed term and set constraints[END_REF] and our analyzer, we used two of our benchmarks for which we have a faithful SML translation: Knuth-Bendix and Nucleic. The times reported below are of the form t1/t2, where t1 is the time spent in exception analysis only, and t2 is the total program analysis time, including parsing and type-checking in addition to exception analysis. From these figures, our exception analysis seems notably faster. However, there are many external factors that influence the total running times of the analyses (such as the Yi-Ryu and BANE analyses being compiled by SML/NJ while ours is compiled by Objective Caml), so the figures above are not conclusive.

The main difference between the analyses of [START_REF] Yi | Towards a cost-effective estimation of uncaught exceptions in SML programs[END_REF][START_REF] Fähndrich | Program analysis using mixed term and set constraints[END_REF] and ours is the approximation of arguments carried by exceptions: they approximate only exception and function values carried by exceptions, but our analysis is the only one that also approximates exception arguments that are strings, integers, or datatypes. As explained in section 2.3, approximating all arguments of exceptions is crucial to obtain precise analysis of many real applications.

In theory, our unification-based analysis should be less precise than analyses based on inclusion constraints such as [START_REF] Yi | Towards a cost-effective estimation of uncaught exceptions in SML programs[END_REF][START_REF] Fähndrich | Program analysis using mixed term and set constraints[END_REF]: the bidirectional propagation of information performed by unification causes exception effects to "leak" in types where those exceptions cannot actually occur. It is easy to construct artificial examples of such leaks, e.g. by replacing let-bound identifiers by λ-bound identifiers. However, those examples do not seem to occur in actual programs. The only leaks we observed in actual programs were related either to deficiencies of our incomplete algorithm for typing polymorphic recursion, or to functions contained inside mutable data structures. On those two cases, [START_REF] Fähndrich | Program analysis using mixed term and set constraints[END_REF] obtains more precise results than our analysis.

Other related work

Our use of rows with row variables and presence annotations to approximate values of base types and sum types is essentially identical to Rémy's typing of extensible variants [START_REF] Rémy | Records and variants as a natural extension of ML[END_REF]. Another application of Rémy's encoding is the soft typing system for Scheme of [START_REF] Wright | A practical soft type system for Scheme[END_REF].

There is a natural connection between exception analysis and type inference for extensible variants: using the well-known functional encoding of exceptions (where each subexpression is transformed to return a value of a variant type, either an exception tag or NormalResult(v) where v is the value of the subexpression), estimating uncaught exceptions is equivalent to inferring precise variant types. Pottier [START_REF] Pottier | Type inference in the presence of subtyping: from theory to practice[END_REF] outlines an exception analysis thus derived from a type inferencer for ML with subtyping.

Refinement types [START_REF] Freeman | Refinement types for ML[END_REF] also introduce annotations on types to characterize subsets of ML's data types. Our approach is less ambitious than refinement types, in that it does not try to capture "deep" structural invariants of recursive data structures; on the other hand, type inference is much easier.

The principles of effect systems were studied extensively in the early '90s [START_REF] Lucassen | Polymorphic effect systems[END_REF][START_REF] Talpin | The type and effect discipline[END_REF], but few practical applications have been developed since. An impressive application is the region analysis of Tofte et al. [START_REF] Tofte | Region-based memory management[END_REF][START_REF] Tofte | A region inference algorithm[END_REF]. Like ours, its precision is improved by typing recursion polymorphically.

Several program analyses based on unification and running in quasi-linear time have been proposed as faster alternatives to more conventional dataflow analyses. Two wellknown examples are Henglein's tagging analysis [START_REF] Henglein | Global tagging optimization by type inference[END_REF] and Steensgaard's aliasing analysis [START_REF] Steensgaard | Points-to analysis in almost linear time[END_REF]. Baker [START_REF] Baker | Unify and conquer (garbage, updating, aliasing[END_REF] suggests other examples of unification-based analyses.

Conclusions and future work

It is often said that unification-based program analyses are faster, but less precise than more general constraint-based analyses such as CFA or SBA. For exception analysis, our experience indicates that a combination of unification, letpolymorphism, and polymorphic recursion is in practice almost as precise as analyses based on inclusion constraints. (The only case where our analysis is noticeably less precise than inclusion constraints is when references to functions are used intensively.) The running times of our algorithm seem excellent (although its theoretical complexity is at least as high as that of ML type inference). In turn, this good efficiency of our analysis allows us to keep more information on exception arguments than the other exception analyses, increasing greatly the precision of the analysis on certain ML programs. Thus, we see an interesting case of "less is more", where an a priori imprecise technology (unification) allows to improve eventually the precision of the analysis. Some engineering issues remain to be solved before our analysis can be applied to large ML applications. The main practical issue is displaying the results of the analysis in a readable way. The volume of information contained in annotated type expressions can be overwhelming. The programmer should be able to select different levels of display abstracting some of that information.

  type unix_error = EACCES | ENOENT | ENOSPC | ... (* enumerated type with 67 constructors representing Unix error codes *) exception Unix_error of unix_error

Figure 1 :

 1 Figure 1: Reduction rules

Figure

  Figure 2: Kinding rules

4 .

 4 A row ϕ annotating an exception type exn[ϕ] or a function type τ1 ϕ → τ2 can only contain constant or parameterized constructors C, D and must not end with .

ϕ

  :: EXN({C}) ϕ :: EXN(∅) E C : exn[C : Pre; ϕ ]/ϕ (7) τ ≤ TypeArg(D) E a : τ /ϕ ϕ :: EXN({D}) ϕ :: EXN(∅) E D(a) : exn[D(τ ); ϕ ]/ϕ (8)

  exception C: try raise(C) with x → match x with C → 1 | y → raise yThe effect of raise(C) is C : Pre; ρ. Hence, the type of x is exn[C : Pre; ρ]. Subtracting the pattern C from this type, we obtain the type exn[C : δ; ρ] for y. Hence the effect of the whole match expression, and also of the whole try expression, is C : δ; ρ. The type is int[1 : Pre; ρ ]. Since δ, ρ and ρ are generalizable and occur only positively, we have established that no exception escapes the expression, and that it can only evaluate to the integer 1.We now extend the previous example along the lines of the failwith example of section 2.3: let failwith = λn. raise(D(n)) in try failwith(42) with x → match x with D(42) → 0 | y → raise y We obtain the following intermediate typings: failwith : ∀α, ρ1, ρ2. int[ρ1] D(int[ρ 1 ]);ρ 2 -------→ α x : exn[D(int[42 : Pre; ρ3]); ρ4] y : exn[D(int[42 : δ; ρ3]); ρ4]

  The three occurrences of ρ express the union of the effects of f and g. The application of compose above has effect C : Pre; ρ3. Concerning exceptions as first-class values, the first example from section 2.2 becomes: let test = λexn. try raise(exn) with x → match x with C → 1 | y → raise(y) in test(C) The type scheme for test is ∀ρ, ρ , δ. exn[C : Pre; ρ] C : δ; ρ --→ int[1 : Pre; ρ ], expressing that the function raises whatever exception it receives as argument, except C. The application test(C) has thus type int[1 : Pre; ρ1] and effect C : δ2; ρ2. Hence no exception escapes. The application test C' where C' is another exception distinct from C would have effect C : δ3; C : Pre; ρ3, thus showing that C' may escape.

Lemma 2 (

 2 Correctness of subtraction) If E0 v : τ /ϕ and M (v, p) is undefined (v does not match pattern p) and τ -p Y τ , then E0 v : τ /ϕ. The correctness of our exception analysis (all uncaught exceptions are detected) is a simple corollary of subject reduction: Theorem 3 (Correctness of exception analysis) Let a be a complete program. Assume E0 a : τ /ϕ and a * ⇒ raise v. Then, either v = C and ϕ = C : Pre; ϕ for some C and ϕ , or v = D(v ) and ϕ = D(τ ); ϕ and E0

ρ 3 →

 3 τ where τ is µα.intlist[Cons(int[ρ1] × α); ρ4]. With this type for Cons, the list n is given the reasonably compact type τn shown above.

  let r = ref(λx. ...) in let f = λy. if cond then !r y else raise C in !r 0 r has type int ρ → int where ρ is not generalized. When typing f, the effect of raise C is unified with that of !r y, hence ρ becomes C : Pre; ρ and the application !r 0 appears to raise C. 6 Related work 6.1 Exception analyses for ML

  2: Kinding rules the constant row elements (i and C) also carry a presence annotation, written π. A presence annotation can be either Pre, meaning that the element is present in the set denoted by the row expression; or a presence variable δ meaning that the element is actually not present in the set denoted by the row expression, but may be considered as present in order to satisfy unification constraints.

Examples: The type int[ ] denotes all integer values. The type of integer addition is ∀ρ1, ρ2, ρ3, ρ4. int[ρ1]

  During inference, tl and l receive types intlist[ρ1] and intlist[Cons(int[ρ2] × intlist[ρ1]); ρ3] respectively. If only finite type expressions are allowed, those two types have no unifier and the program is rejected by the analysis. This is not acceptable, so we extend our type system with recursive (infinite, regular) type expressions. On the example above, we obtain µα. intlist[Cons(int[ρ2] × α); ρ3].

		The extension of our type system with recursive type
		expressions involves replacing term unification by graph
		unification in the type inference algorithm, but this causes
		no technical difficulties.
	Cons : ∀ρ1, ρ2, ρ3, ρ4. int[ρ1] × intlist[ρ2]	ρ 3 →
	intlist[Cons(int[ρ1] × intlist[ρ2]); ρ4]
	Recursive datatypes such as intlist above naturally lead
	to recursive type expressions. Consider:

Cons of int * intlist we assign Nil and Cons the type schemes Nil : ∀ρ. intlist[Nil : Pre; ρ] let tail = λx. match x with Cons(hd,tl) → tl | l → l

  . . . × τn tuple type Row elements: ε ::= . . . | {lbl 1 : τ1; . . . ; lbl n : τn}

	Type expressions:
	τ ::= . . .
	| τ t[ϕ]	approximated type constructor
	| τ t	non-approximated type constructor
	| τ1 × 4.3 Mutable data structures
	Mutable data structures (references, arrays, records with
	mutable fields) are trivially handled: it suffices to introduce
	the standard value restriction on let-generalization [34].

The complexity of 0-CFA alone is O(n 3 ), where n is the size of the whole program. We did not observe cubic behavior on our tests, however. Quadratic behavior arises in the following not uncommon case: assume that a group of functions of size k = O(n) recurses over a list of m = O(n) elements given in extension in the program source. At least m iteration of the analysis is required before fixpoint is reached on the parameters and results of the functions. Since each iteration takes time proportional to k, the time of the analysis is O(

n 2 ).

This might cause performance problems in conjunction with OCaml objects, which relies intensively on type abbreviations to make type expressions more manageable[START_REF] Rémy | Objective ML: A simple object-oriented extension of ML[END_REF]. If this turns out to be a problem, we could also handle abbreviations by adding extra row parameters to the type constructors, as described in[START_REF] Fähndrich | Tracking down exceptions in Standard ML programs[END_REF] and in

section 4.1.3.

The analysis of objects and classes was prototyped separately and remains to be merged in our main implementation.

Acknowledgements

The inference algorithm for polymorphic recursion used in our implementation was designed in collaboration with Pierre Weis. We thank François Pottier and Didier Rémy for interesting discussions.

A The unification algorithm

In this appendix, we give the unification algorithm for our type algebra modulo the two equations ( 1) and [START_REF] Fähndrich | Making set-constraint based program analyses scale[END_REF]. We define the head constructor H(ε) of a row element ε as follows:

The algorithm handles the left commutativity axiom (equation (1)) like in [START_REF] Rémy | Type inference for records in a natural extension of ML[END_REF].

mgu(∅) = id Unification between types:

and ρ is not free in the l.h.s. and has kind t(S ∪ {H(ε1), H(ε2)}) where t(S) is the kind of ε1; ϕ1 and ε2; ϕ2 Unification between row elements:

If none of the cases above is applicable, mgu(Q) is undefined.

B The type inference algorithm

The result of the algorithm W (E, a) is the triple (τ, ϕ, θ) defined by induction on a as follows:

If a is x (with x ∈ Dom(E)): let ρ be a fresh variable of kind EXN(∅) take τ = Inst(E(x)) and ϕ = ρ and θ = id .

If a is i: let ρ be a fresh variable of kind INT({i}) let ρ be a fresh variable of kind EXN(∅) take τ = int[i : Pre; ρ] and ϕ = ρ and θ = id .

If a is λx. a1: let α be a fresh variable let (τ1, ϕ1, θ1) = W (E ⊕ {x : α}, a1) let ρ be a fresh variable of kind EXN(∅) take τ = θ1(α) ϕ → τ1 and ϕ = ρ and θ = θ1.

If a is C: let ρ be a fresh variable of kind EXN({C}) let ρ be a fresh variable of kind EXN(∅) take τ = exn[C : Pre; ρ] and ϕ = ρ and θ = id .

let ρ be a fresh variable of kind EXN({D}) let ρ be a fresh variable of kind EXN(∅) take τ = exn[D(µ(τ1)); ρ] and ϕ = ρ and θ = µ • θ1.

The auxiliary function Inst(σ) (trivial instance):

where α i , ρ j , δ k are fresh variables such that ρ j and ρj have the same kind for all j.


An overview of Types in Compilation

Types in programming languages

Most programming languages are equipped with a type system that detects type errors in the program, such as using a variable or result of a given type in a context that expects data of a different, incompatible type. Such type checking can take place either statically (at compile-time) or dynamically (at run-time). Type checking has proved to be very effective in catching a wide class of programming errors, from the trivial (misspelled identifiers) to the fairly deep (violations of data structure invariants). It makes program considerably safer, ensuring integrity of data structures and type-correct interconnection of program components.

Safety is not the only motivation for equipping programming languages with type systems, however. Another motivation, which came first historically, is to facilitate the efficient compilation of programs. Static typing restricts the set of programs to be compiled, possibly eliminating programs containing constructs that are difficult to compile efficiently or even to compile correctly at all. Also, static typing guarantees certain properties and invariants on the data manipulated by the program; the compiler can take advantage of these semantic guarantees to generate better code. The "Types in Compilation" workshops are dedicated to the study of these interactions between type systems and the compilation process.

Exploiting type information for code generation and optimization

An early example of a type system directed towards efficient compilation is that of Fortran. The Fortran type system introduces a strict separation between integers numbers and floating-point numbers at compile-time. The main motivation for this separation, according to Fortran's designers, was to avoid the difficulties of handling mixed arithmetic at run-time [2, chapter 6]. Thanks to the type system, the compiler "knows" when to generate integer arithmetic operations, floating-point arithmetic operations, and conversions between integers and floats.

Since then, this separation has permeated hardware design: most processor architectures provide separate register sets and arithmetic units for integers and for floats. In turn, this architectural bias makes it nearly impossible to generate efficient numerical code for a language whose type system does not statically distinguish floating-point numbers from integers.

Another area where compilers rely heavily on static typing is the handling of variable-sized data. Different data types have different natural memory sizes: for instance, double-precision floats usually occupy more space than integers; the size and memory layout of aggregate data structures such as records and arrays vary with the sizes and number of their elements. Precise knowledge of size information is required to generate correct code that allocates and operates over data structures. This knowledge is usually derived from the static typing information: the type of a data determines its memory size and layout. Languages without static typing cannot be compiled as efficiently: all data representations must fit a default size, if necessary by boxing (heap-allocating and handling through a pointer) data larger than the default size -an expensive operation. Staticallytyped languages whose type system is too flexible to allow this determination of size information in all cases (e.g. because of polymorphism, type abstraction, or subtyping) make it more difficult, but not impossible, to exploit unboxed data representations: see [START_REF] Simon | Unboxed values as first-class citizens in a non-strict functional language[END_REF][START_REF] Leroy | Unboxed objects and polymorphic typing[END_REF][START_REF] Shao | A type-based compiler for Standard ML[END_REF][START_REF] Harper | Compiling polymorphism using intensional type analysis[END_REF][START_REF] Tarditi | TIL: a type-directed optimizing compiler for ML[END_REF][START_REF] Leroy | The effectiveness of type-based unboxing[END_REF][START_REF] Shao | Flexible representation analysis[END_REF][START_REF] Ohori | An unboxed operational semantics for ML polymorphism[END_REF] for various approaches.

Guarantees provided by the type system can also enable powerful program optimizations. For instance, in a strongly-typed language (whose type system does not allow "casts" between incompatible types), two pointers that have incompatible types cannot alias, i.e. cannot point to the same memory block. This guarantees that load and store operations through those two pointers cannot interfere, thus allowing more aggressive code motion and instruction scheduling [START_REF] Diwan | Type-based alias analysis[END_REF]. One can also envision different heap allocation strategies for objects of different types, as exemplified by the paper by Genius et al. in this proceeding.

Another area where type information is useful is the optimization of method dispatch in object-oriented languages. General method dispatch is an expensive operation, involving a run-time lookup of the code associated to the method in the object's method suite, followed by a costly indirect jump to that code. In a class-based language, if the actual class to which the object belongs is known at compile-time, a more efficient direct invocation of the method code can be generated instead. If the code of the method is small enough, it can even be expanded in-line at the point of call. Simple examination of the static type of the object and of the class hierarchy of the program uncovers many opportunities for this optimization. For instance, if the static type of the object is a class C that has no subclasses, the compiler knows that the actual class of the object is C and can generate direct invocations for all methods of the object [START_REF] Dean | Optimization of object-oriented programs using static class hierarchy analysis[END_REF][START_REF] Fernández | Simple and effective link-time optimization of Modula-3 programs[END_REF][START_REF] Bacon | Fast static analysis of C++ virtual function calls[END_REF].

Program analyses and optimizations based on non-standard type systems

There are many points of convergence between, on the one hand, algorithms for type checking and type inference, and on the other hand, static analyses of programs intended to support code optimization. This should not come as a surprise: both static analyses and type inference algorithms attempt to reconstruct semantic information that is implicit in the program source, and propagate that information through the program, recording it at each program point. A more formal evidence is that both static analyses and type inference problems can be recast in the common framework of abstract interpretation [START_REF] Cousot | Types as abstract interpretations[END_REF]. What is more remarkable is that essentially identical algorithms are used for type inference and for certain program analyses.

For instance, unification between first-order terms, as used for type inference in the Hindley-Milner type system of ML and Haskell, is also at the basis of several fast program analyses such as Steensgaard's aliasing analysis [START_REF] Steensgaard | Points-to analysis in almost linear time[END_REF], and Henglein's tagging analysis [START_REF] Henglein | Global tagging optimization by type inference[END_REF]. Baker [START_REF] Henry | Unify and conquer (garbage, updating, aliasing[END_REF] reflects informally on this connection between Hindley-Milner type inference and several program analyses.

Another technique that has attracted considerable interest recently both from a type inference standpoint and a program analysis standpoint consists in setting up systems of set inclusion constraints (set inequations) and solving them iteratively. This technique has been used to perform type inference for type systems with subtyping [START_REF] Mitchell | Coercion and type inference[END_REF][START_REF] Aiken | Type inclusion constraints and type inference[END_REF][START_REF] Eifrig | Type inference for recursively constrained types and its application to OOP[END_REF]. The same technique is also at the basis of several flow analyses for functional and object-oriented languages [START_REF] Shivers | Control-flow analysis in Scheme[END_REF][START_REF] Shivers | Control-Flow Analysis of Higher-Order Languages[END_REF][START_REF] Heintze | Set-based analysis of ML programs[END_REF][START_REF] Agesen | Type inference of Self: analysis of objects with dynamic and multiple inheritance[END_REF][START_REF] Plevyak | Precise concrete type inference for objectoriented languages[END_REF][START_REF] Jagannathan | Polymorphic splitting: An effective polyvariant flow analysis[END_REF][START_REF] Defouw | Fast interprocedural class analysis[END_REF]. These analyses approximate the flow of control and data in the presence of first-class functions and objects, and are very effective to optimize function applications and method invocations, and also to eliminate dynamic type tests in dynamically-typed languages. Palsberg and O'Keefe [START_REF] Palsberg | A type system equivalent to flow analysis[END_REF] draw a formal connection between those two areas, by proving the equivalence between a flow analysis (0-CFA) and a type inference algorithm (for the Amadio-Cardelli type system with subtyping and recursive types). The paper by Aiken et al. in these proceedings surveys the use of set inclusion constraints and equality (unification) constraints for program analyses.

Several non-standard type systems have been developed to capture more precisely the behavior of programs and support program transformations. The effect systems introduced by Lucassen and Gifford [START_REF] Lucassen | Polymorphic effect systems[END_REF][START_REF] Jouvelot | Algebraic reconstruction of types and effects[END_REF] enrich function types with effects approximating the dynamic behavior of the functions, such as inputoutput or operations on the store. This information is useful for code motion and automatic parallelization. Jouvelot, Talpin and Tofte [START_REF] Talpin | The type and effect discipline[END_REF][START_REF] Tofte | Region-based memory management[END_REF] use region annotations on the types of data structures and functions to determine aliasing and lifetime information on data structures. The ML compiler developed by Tofte et al. [START_REF] Birkedal | From region inference to von Neumann machines via region representation inference[END_REF] relies on these lifetime information for managing memory as a stack of regions with compiler-controlled explicit deallocation of regions instead of a conventional garbage collector. Tolmach's paper in these proceedings presents a reformulation of simple effect systems as monadic type systems. Shao and Trifonov's paper develop a type system to keep track of the use of first-class continuations in a program, thus allowing interoperability between languages that support callcc and languages that do not.

Finally, non-standard type systems can also be used to record and exploit the results of earlier program analyses. For instance, Dimock et al. [START_REF] Dimock | Strongly typed flow-directed representation transformations[END_REF] and Banerjee [START_REF] Banerjee | A modular, polyvariant, and type-based closure analysis[END_REF] develop rich type systems that capture and exploit the flow information produced by flow analyses. Another example is Thiemann's paper in these proceedings, which develops a type system that captures resource constraints that appear in compilers during register allocation.

Types at run-time

Many programming languages require compiled programs to manipulate some amount of type information at run-time. Interesting compilation issues arise when trying to make these run-time manipulations of types as efficient as possible. A prime example is the compilation of run-time type tests in dynamicallytyped languages such as Scheme and Lisp: many clever tagging schemes have been developed to support fast run-time type tests. Another example is objectoriented languages such as Java, Modula-3, or C++ with run-time type inspection, where programs can dynamically test the actual class of an object. Again, clever encodings of the type hierarchy have been developed to perform those tests efficiently.

Even if the source language is fully statically typed, compilers and run-time systems may need to propagate type information to run-time in order to support certain operations. A typical example is the handling of non-parametric polymorphic operations such as polymorphic equality in ML and type classes in Haskell [START_REF] Wadler | How to make ad-hoc polymorphism less adhoc[END_REF]. Another example is the handling of polymorphic records presented in [START_REF] Ohori | A polymorphic record calculus[END_REF]. There are several ways to precompile the required type information into an efficient form: one is to attach simple tags to data structures; another is to pass extra arguments (type representations or dictionaries of functions) to polymorphic functions. Elsman's paper in these proceedings compares the performances of these two approaches in the case of ML's polymorphic equality.

Passing run-time representations of type expressions as extra arguments to polymorphic function allows many type-directed compilation techniques to be applied to languages with polymorphic typing. The TIL compiler [START_REF] Tarditi | TIL: a type-directed optimizing compiler for ML[END_REF] and the Flint compiler [START_REF] Shao | Flexible representation analysis[END_REF] rely on run-time passing of type expressions (taken from extensions of the F ω type system) to handle unboxed data structures in polymorphic functions and modules with abstract types. Constructing and passing these type expressions at run-time entail some execution overhead. The paper by Shao and Saha in these proceedings shows how to minimize this overhead by lifting those type-related computations out of loops and functions so that they all take place once at the beginning of program execution.

Non-conservative garbage collectors also require some amount of type information at run-time in order to distinguish pointers from non-pointers in memory roots and heap blocks. The traditional approach is to use tags on run-time values. Alternatively, Appel [START_REF] Appel | Run-time tags aren't necessary[END_REF] suggested to attach source types to blocks of function code, and reconstruct type information for all reachable objects at run-time, using a variant of ML type reconstruction. The paper by Hosoya and Yonezawa in these proceedings is the first complete formalization of this approach.

Communicating static type information to the run-time system can be challenging, as it requires close cooperation from the compiler back-end. For instance, a type-directed garbage collector needs type information to be associated with registers and stack locations at garbage collection points; cooperation from the register allocator is needed to map the types of program variables onto the registers and stack slots. The paper by Bernard et al. in these proceedings discuss their experience with coercing a generic back-end into propagating type information.

Another operation that relies heavily on run-time type information is marshaling and un-marshaling between arbitrary data structures and streams of bytes -a crucial mechanism for persistence and distributed programming. In these proceedings, Duggan develops rich type systems to support marshaling in the presence of user-defined marshaling operations for some data types.

Typed intermediate languages

In traditional compiler technology, types are checked on the source language, but the intermediate representations used in the compilation process are essentially untyped. The intermediate representations may sometimes carry type annotations introduced by the front-end, but no provision is made for type-checking again these intermediate representations. Recently, several compilers have been developed that take the opposite approach: their intermediate representations are equipped with typing rules and type-checking algorithms, and their various passes are presented as type-preserving transformations that, given a well-typed input, must produce a well-typed term of the target intermediate language.

The need for typed intermediate representations is obvious in compilers that require precise type information to be available till run-time, such as TIL and Flint [START_REF] Tarditi | TIL: a type-directed optimizing compiler for ML[END_REF][START_REF] Shao | Flexible representation analysis[END_REF], or at least till late in the compilation process. Without requiring that each compiler pass be type-preserving and its output typable, it is nearly impossible to ensure the propagation of correct type information throughout the whole compiler.

Even in compilers that do not rely as crucially on types, typed intermediate languages can be extremely useful to facilitate the debugging of the compiler itself. During compiler development and testing, the type-checkers for the intermediate representations can be run on the outcome of every program transformation performed by the compiler. This catches a large majority of programming errors in the implementation of the transformations. In contrast with traditional compiler testing, which shows that the generated code is incorrect but does not indicate which pass is erroneous, type-checking the intermediate representations pinpoints precisely the culprit pass. The Glasgow Haskell compiler was one of the first to exploit systematically this technique [START_REF] Simon | Compiling Haskell by program transformation: a report from the trenches[END_REF].

So far, typed intermediate representations as described above have been applied almost exclusively to compiling functional languages. The paper by Wright et al. in these proceedings develops a typed intermediate language for compiling Java, and discusses the difficult issue of making explicit the "self" parameter to methods in a type-preserving way.

Typed intermediate languages usually do not go all the way down to code generation. For instance, Glasgow Haskell preserves types through its high-level program transformation, but the actual code generation is mostly untyped. The TIL compiler goes several steps further, in particular by performing the conversion of functions into closures in a type-preserving manner [START_REF] Minamide | Typed closure conversion[END_REF]. The paper by Morrisett et al. in these proceedings shows how to go all the way to assembly code: it proposes a type system for assembly code that can type-check reasonably optimized assembly code, including most uses of a stack.

Other applications of types

While the discussion above has concentrated on core compiler technology for functional and object-oriented languages, types have also found many exciting and sometimes unexpected applications in other areas of programming language implementation. For instance, type-directed partial evaluation is an interesting alternative to traditional partial evaluation based on source-level reductions. The paper by Balat and Danvy in these proceedings presents a type-directed partial evaluator that also uses run-time code generation. The paper by Fujinami presents a partial evaluator and run-time code generator for C++.

Languages for distributed programming based on process calculi are another area where the exploitation of type information is crucial to obtain good performances. Kobayashi's abstract in these proceedings surveys this topic.

Types have interesting applications in the area of language-based security for mobile code. Java applets have popularized the idea that foreign compiled code can be locally verified for type-correctness before execution. This local type-checking of compiled code then enables language-based security techniques that rely on typing invariants, such as the Java "sandbox". Advances in typed intermediate languages have an important impact in this area. For instance, while Java code verification is performed on unoptimized bytecode for an abstract machine, the paper by Morrisett et al. in these proceedings show that similar verifications can be carried on optimized machine code. Lee and Necula's work on proof-carrying code [START_REF] Necula | Proof-carrying code[END_REF] show how to generalize this approach to the verification of arbitrary specifications.

In conclusion, there has been considerable cross-fertilization between type systems and compilers, and we hope to see more exciting new applications of types in the area of programming language implementations in the near future.