Zaynah Dargaye
email: lea-zaynah.dargaye@cea.fr

Xavier Leroy
email: xavier.leroy@inria.fr

A verified framework for higher-order uncurrying optimizations

Keywords: Functional programming languages, Compiler optimization, Compiler verification, Semantic preservation, Mechanized verification

Function uncurrying is an important optimization for the efficient execution of functional programming languages. This optimization replaces curried functions by uncurried, multiple-argument functions, while preserving the ability to evaluate partial applications. First-order uncurrying (where curried functions are optimized only in the static scopes of their definitions) is well understood and implemented by many compilers, but its extension to higher-order functions (where uncurrying can also be performed on parameters and results of higher-order functions) is challenging. This article develops a generic framework that expresses higher-order uncurrying optimizations as type-directed insertion of coercions, and prove its correctness. The proof uses step-indexed logical relations and was entirely mechanized using the Coq proof assistant.

Introduction

Currying in functional languages

Most programming languages support n-ary functions, that is, functions that take zero, one or several arguments. Following the models of λ -calculus and set theory, some functional languages provide only unary functions, that is, functions of exactly one argument. This is the case in programming languages such as Standard ML, Caml, and Haskell, and also in specification languages of proof assistants such as HOL and Coq. In these languages, multiple-argument functions are encoded in terms of single-argument functions. One such encoding puts multiple arguments in a tuple or record, which is passed to the function as a single argument, and from which the function recovers the arguments by pattern-matching. For example, the two-argument function taking x and y and returning x + y is encoded as λ p. let (x, y) = p in x + y. Another encoding, called currying 1 , uses functions that return functions to achieve the effect of passing several arguments. Continuing the example above, the two-argument addition function is encoded as f = λ x. λ y. x + y; applying it to the arguments 1 and 2 is performed by two successive applications ( f 1) 2, also written f 1 2.

The choice between the two encodings is largely a matter of programming style. For example, the Standard ML community favors the use of tuples, while currying is the preferred approach among Caml and Haskell programmers. One technical advantage in favor of currying, however, is the ease with which it expresses partial applications of n-ary functions to m < n initial arguments. For example, if f = λ x. λ y. x + y, the partial application f 1 computes λ y. 1 + y, that is, a one-argument function representing the specialization of f to x = 1.

The run-time cost of currying

Both encodings of n-ary functions entail significant run-time costs if implemented naively. We concentrate on the currying encoding in the following. Consider a simple call-by-value, "eval-apply" strategy (in the terminology of [START_REF] Marlow | Making a fast curry: push/enter vs. eval/apply for higher-order languages[END_REF]) as embodied in the SECD [START_REF] Landin | The mechanical evaluation of expressions[END_REF] and CEK [START_REF] Felleisen | Control operators, the SECD machine and the λ -calculus[END_REF] abstract machines, for example. In this setting, a total application f 1 2 of a 2-argument curried function f proceeds as follows. First, f is evaluated to a function value λ x.λ y.M. Second, the first argument 1 is evaluated. Third, the function is entered, binding 1 to x, and returns the function closure representing λ y.M{x ← 1}. Fourth, the second argument 2 is evaluated. Fifth, the intermediate function λ y.M{x ← 1} is entered with y bound to 2, and the function body M is evaluated at last. Generalizing over the number of arguments, we see that a total application of a n-ary curried function entails the creation of n -1 short-lived intermediate closures, as well as 2n control-flow jumps between the caller and the callee. In contrast, an execution model that natively supports n-ary functions would perform only 2 such jumps and avoid the creation of intermediate closures entirely, saving significant runtime costs. Some of these inefficiencies can be avoided by using a "push-enter" execution model (following again the terminology of [START_REF] Marlow | Making a fast curry: push/enter vs. eval/apply for higher-order languages[END_REF]) instead of an "eval-apply" model. Examples of "push-enter" models include Krivine's machine [START_REF] Krivine | A call-by-name lambda-calculus machine[END_REF], the STG abstract machine [START_REF] Jones | Implementing lazy functional languages on stock hardware: the spineless tagless G-machine[END_REF], and the ZINC abstract machine [START_REF] Leroy | The ZINC experiment: an economical implementation of the ML language[END_REF]. In these models, a curried application such as f 1 2 is evaluated by first pushing the arguments on a stack, in right-to-left order (first 2, then 1), keeping track of the number of available arguments, then evaluating f to a function value, then entering its code. A prelude to the function checks that enough arguments were provided. If so, the body of the function is evaluated. If not, a function closure representing the partial application is immediately returned to the caller.

The "push-enter" model avoids most of the costs of currying in the "eval-apply" model, especially the creation of intermediate closures. Compared with a native implementation of n-ary functions, some overhead remains, however. For instance, parameters must be passed in memory: hardware registers cannot be used for parameter passing. Also, maintaining the count of available arguments at run-time and testing it on entrance to every n-ary function is costly in execution time. For these reasons, we now turn to another approach: static (compile-time) uncurrying, and concentrate on it in the remainder of this article.

Static uncurrying

Static uncurrying is a compile-time optimization that translates an ML-or Haskell-like surface language of unary functions to an intermediate language featuring n-ary functions without partial applications (i.e. the number of arguments provided at calls must match exactly the arity of the callee). Such an intermediate language can, then, be compiled to efficient machine code, with registers being used for parameter passing and no run-time arity checks on entrance to functions.

We now describe the simple static uncurrying strategy that is implemented in the OCaml native-code compiler and recent versions of the Glasgow Haskell compiler, among others. It detects curried function abstractions that are bound by a let (or similar local, top-level or module-level binding construct) and turns them into n-ary functions of the target language2 : let f = λ x.λ y. x + y ⇒ let f = λ (x,y). x + y

Within the lexical scope of their bindings, total, curried applications of these functions are turned into single, n-ary applications:

in f 1 2 ⇒ in f(1, 2)
Partial applications of these functions, as well as any use of these functions as first-class values, are handled by re-constructing a curried version of the n-ary function. Changing only the "in" part of the example above, we have the following translations: 3in List.map2 f l1 l2 ⇒ in List.map2 (curry 2 (f), l1, l2) in List.map (f 3) l3

⇒ in List.map (curry 2 (f)(3), l3)
The curry 2 combinator is defined as λ ( f ). λ (x). λ (y). f (x, y) in the intermediate language.

It takes a function f of arity 2 and returns the equivalent curried function. One such curry n combinator is defined for each arity n of interest.

There exist several variants of this uncurrying strategy. (The one outlined above is approximately the one used in OCaml.) For instance, the curry combinators can be expanded in-line and reduced, at some cost in code size: the partial application f 3 would then be translated as let x = 3 in λ y. f(x, y). Also, the Glasgow Haskell compiler exploits combinators papp n,m = λ ( f , x 1 , . . . , x m ). λ (x m+1 ) . . . λ (x n ). f (x 1 , . . . , x n ) to speed up the partial application of a n-ary function f to m < n initial arguments.

The performance characteristics of this approach can be summarized as follows. Within the lexical scope of a named definition of a curried function, total applications of the function name are compiled optimally to a n-ary application. All other uses of curried functions (partial applications, passing a curried function as parameter to a higher-order function, storing curried functions in data structures, etc) suffer from the same run-time costs exhibited by the naive "eval-apply" model. However, the first case (total applications of known functions) is very common: Marlow and Peyton Jones [START_REF] Marlow | Making a fast curry: push/enter vs. eval/apply for higher-order languages[END_REF] report that it amounts for 80% of function calls on a Haskell benchmark suite; the second author observed similar numbers on an OCaml benchmark suite. This uncurrying strategy therefore performs well in practice. Compared with a "push-enter" execution model, it also simplifies the run-time system [START_REF] Marlow | Making a fast curry: push/enter vs. eval/apply for higher-order languages[END_REF] and is more compatible with the use of standard, currying-unaware compiler back-ends.

The correctness of static uncurrying (that the generated intermediate code does not get stuck on an arity mismatch at application-time and computes the same results as the original code) is intuitively clear, but not obvious to prove in full details. As part of her work on the formal verification of a compiler front-end for the MiniML functional language, the first author developed a mechanically-checked proof of correctness for the uncurrying optimization outlined above [START_REF] Dargaye | Décurryfication certifiée[END_REF]. The present article extends this work to more aggressive static uncurrying schemes that work across higher-order functions.

Higher-order static uncurrying

The static uncurrying strategy outlined in section 1.3 is first-order in nature: as soon as a curried function is passed as argument to a higher-order function or used as a first-class value, no uncurrying takes place. This is clearly suboptimal: opportunities for uncurrying across higher-order functions are not uncommon, as the following example demonstrates. Consider the map2 iterator from OCaml's List module, which applies a two-argument function pairwise to the elements of two lists.

let rec map2 = λ f.λ l1.λ l2. match (l1, l2) with | ([], []) -> [] | (h1::t1, h2::t2) -> f h1 h2 :: map2 f t1 t2 | (_, _) -> fail in map2 (λ x.λ y. x + y) l1 l2
First-order uncurrying produces the following intermediate code, where map2 is uncurried but its f parameter remains curried:

let rec map2 = λ (f, l1, l2). match (l1, l2) with | ([], []) -> [] | (h1::t1, h2::t2) -> f(h1)(h2) :: map2(f, t1, t2) | (_, _) -> fail in map2((λ x.λ y. x + y), l1, l2)
A higher-order uncurrying optimization could uncurry the parameter f as well, turning it into a 2-argument function and improving the efficiency of the code:

let rec map2 = λ (f, l1, l2). match (l1, l2) with | ([], []) -> [] | (h1::t1, h2::t2) -> f(h1, h2) :: map2(f, t1, t2) | (_, _) -> fail in map2((λ (x, y). x + y), l1, l2)
What happens if, somewhere else in the program, we need to apply map2 to a function f that has not been uncurried? Just like the curry n combinators were used previously to resolve mismatches between an uncurried function definition and a curried use site, we can use the uncurry n combinators

uncurry n = λ ( f ).λ (x 1 , . . . , x n ). f (x 1 ) • • • (x n )
to resolve mismatches between a curried function definition and an uncurried use site. For example, applying map2 above to a curried function f can be done as map2(uncurry 2 (f), l1, l2).

The curry and uncurry combinators can be combined together to resolve more complicated mismatches. For example, the term λ (x).uncurry 2 (curry 3 ( f )(x)) transforms a 3argument uncurried function f into a semi-curried function that takes one argument, then returns an uncurried function of 2 arguments.

Higher-order uncurrying is a natural extension of the familiar, first-order uncurrying optimizations, but it has not received much attention. The only prior work on higher-order uncurrying that we are aware of is that of Hannan and Hicks [START_REF] Hannan | Higher-order uncurrying[END_REF], who developed a type system to validate a posteriori the correctness of an uncurrying transformation. We are not aware of any compiler for a functional language that implements higher-order uncurrying. One possible reason is that choosing between different possible higher-order uncurryings (for example, to decide whether to uncurry the f parameter to the map2 function above) is difficult and no good heuristics are known. We will not settle this issue in this paper, but rather concentrate on characterizing and proving correct a whole family of possible higherorder uncurrying optimizations.

This work

In this article, we develop a general framework for higher-order uncurrying optimizations and prove their correctness through a generic semantic preservation argument. Section 2 develops a nondeterministic specification of what constitutes a valid uncurrying of a source program written in a simple, untyped functional language with unary functions. The specification is presented as a non-standard type system instrumented with the generation of uncurried terms. Coercions are introduced in a type-directed manner to solve arity mismatches, generalizing the curry and uncurry combinators used in earlier examples. To prove that these uncurryings are correct (i.e. preserve the semantics of the source program), we use step-indexed logical relations, a powerful semantic tool introduced by Appel and McAllester [START_REF] Appel | An indexed model of recursive types for foundational proof-carrying code[END_REF] and reviewed in section 3. The proof of semantic preservation is presented in section 4. Two applications of our framework are worked out in section 5: one is a very simple correctness proof for the first-order uncurrying optimization outlined in section 1.3; the other is a validating translation that exploits the results of an external uncurrying strategy, after checking them for correctness, to generate the corresponding uncurried code. Issues with non-terminating programs are discussed in section 6. Section 7 discusses related work, followed by concluding remarks and perspectives for future work in section 8.

Our work improves on that of Hannan and Hicks [START_REF] Hannan | Higher-order uncurrying[END_REF] in two ways. First, we show how to automate the insertion of coercions to resolve 'impedance' mismatches between parts of program that make different uncurrying decisions. This was mentioned but left as future work by Hannan and Hicks. Second, our framework is independent of the type system (if any) of the source language, while that of Hannan and Hicks relies on a specific type system (Hindley-Milner polymorphism). Extending their framework to the richer type systems of languages like Haskell or OCaml, or to the even richer type theories found in proof assistants like HOL or Coq4 is challenging. In contrast, our framework also uses types to capture compile-time arity information, but uses them in the style of soft typing [START_REF] Wright | A practical soft type system for Scheme[END_REF]: a universal "top" type of fully curried functions can always be used as an escape hatch when contradictory compile-time arity information arises. Our work is therefore applicable to any functional language, statically typed or not.

The formalization and proofs presented in this paper have been mechanically checked using the Coq proof assistant [START_REF]Coq development team: The Coq proof assistant[END_REF][START_REF] Bertot | Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions[END_REF]. The complete Coq development is available on the Web at http://gallium.inria.fr/~xleroy/uncurry/. Taking advantage of this, we only sketch the proofs in this paper, referring the reader to the Coq development for full details.

2 Specification of the uncurrying transformation

The source language

The source language for the uncurrying transformation is a standard λ -calculus with con- stants, enriched with a let binding and a letrec binding for defining recursive functions. While both bindings could be encoded in the λ -calculus fragment of the source language, having them as primitive constructs facilitates uncurrying. We omit other features of functional languages (arithmetic, data types, conditionals, pattern-matching, . . . ) since these features are orthogonal to the uncurrying optimization. Alpha-conversion of bound variables is a delicate issue in most mechanized formalizations of program analyses and transformations [START_REF] Aydemir | Mechanized metatheory for the masses: The POPLmark challenge[END_REF]. To avoid this issue, we represent variables by de Bruijn indices: x n is the variable bound by the (n + 1) th enclosing binding construct. Consequently, λ .a binds x 0 to the function parameter in the body a, and let a in a binds the value of a to x 0 during the evaluation of a . Consider letrec λ .a in a . In a, the function parameter is x 0 and the recursive function λ .a itself is x 1 . In a , x 0 refers to the recursive function λ .a.

In examples and informal discussions, we will use variable names f , y, z, . . . for legibility. In standard named notation, our functions are of the shape λ y.a and our local bindings are of the shape let y = a in a and letrec f = λ y.a in a .

The target language

The target language for the uncurrying transformation is similar to the source language, except that it features n-ary function abstractions and applications. To guide the uncurrying transformation, we classify terms of the target language according to their representation types τ. These types capture information on the arity of functions.

Representation types:

τ ::= constants or fully-curried functions | (τ 1 , . . . , τ n ) → τ n-ary functions Compilation environments:

Γ ::= τ 0 . . . τ n maps de Bruijn indices to representation types

The representation type (τ 1 , . . . , τ n ) → τ characterizes a function of arity n that expects n arguments conforming to types τ 1 , . . . , τ n and returns a result conforming to τ. For unary functions (n = 1), we write τ 1 → τ 2 instead of (τ 1 ) → τ 2 .

The representation type corresponds both to non-function values such as constants and to fully-curried functions: functions of arity 1 that expect a fully-curried argument and produce a fully-curried result. In other words, a function of type → can be viewed as having type . (See rule SBASE in section 2.3.) Conversely, it is possible to apply a term b of type to one argument of type , obtaining a result of type . At run-time, such an application can succeed if b is a (fully-curried) function, or fail if b evaluates to a constant. The subset of target terms that have representation type is therefore isomorphic to the source language. It is clear that our type algebra is too weak to guarantee type soundness, but this is not its purpose.

The uncurrying transformation

Many different uncurrying strategies can be considered, and even more so when uncurrying is performed across higher-order functions. Rather than prove the correctness of one particular strategy, we set out to specify (nondeterministically) a large class of uncurrying strategies, which we prove semantically correct in section 4. The specification is presented as a predicate Γ a =⇒ b : τ saying that a target term b is a correct uncurrying of the source term a. In this predicate, τ is the desired representation type for b (as we will see shortly, different representation types lead to different uncurryings), and the compilation environment Γ associates representation types to the free variables of a, which are also the free variables of b.

The predicate Γ a =⇒ b : τ is defined by a set of inference rules reminiscent of a type system. The rules are not syntax-directed, therefore b is not a function of Γ , a, τ but rather of a whole derivation.

Γ (n) = τ (TVAR) Γ x n =⇒ x n : τ Γ c =⇒ c : (TCST) n > 0 τ n . . . τ 1 .Γ a =⇒ b : τ (TABS) Γ λ . . . λ n times .a =⇒ λ n .b : (τ 1 , . . . , τ n ) → τ Γ a =⇒ b : Γ a =⇒ b : (TAPP-) Γ a a =⇒ b(b ) : n > 0 Γ a =⇒ b : (τ 1 , . . . , τ n ) → τ Γ a i =⇒ b i : τ i for i = 1, . . . n (TAPP-N) Γ a a 1 . . . a n =⇒ b(b 1 , . . . , b n ) : τ Γ a =⇒ b : τ τ.Γ a =⇒ b : τ (TLET) Γ let a in a =⇒ let b in b : τ n > 0 τ n . . . τ 1 .((τ 1 , . . . , τ n ) → τ).Γ a =⇒ b : τ ((τ 1 , . . . , τ n ) → τ).Γ a =⇒ b : τ (TLETREC) Γ letrec λ . . . λ n times .a in a =⇒ letrec λ n .b in b : τ Γ a =⇒ b : τ b : τ =⇒ b : τ (TCOERCE) Γ a =⇒ b : τ
The rules for variables and constants (TVAR and TCST) are straightforward. The first interesting rule is TABS. At a function type (τ 1 , . . . , τ n ) → τ, a source-level curried abstraction of at least n parameters λ y 1 , . . . , y n . a uncurries to the n-ary abstraction λ (y 1 , . . . , y n ). b, provided that a uncurries to b at result type τ under the additional assumptions y i : τ i (i = 1, . . . , n). For example, the source term λ x.λ y. y becomes the binary function λ (x, y). y if the desired type is ( , ) → but remains a curried function λ (x). λ (y). y if the desired type is → → . Two rules deal with function applications. Rule TAPP-matches single applications a a at type where the function part a is uncurried to b at type , meaning that it is a fully-curried function. The argument a is uncurried to b at type as well and the generated target term is the unary application b(b ). The other application rule, TAPP-N, deals with source-level curried applications a a 1 . . . a n at type τ. The function part a must uncurry to b at some n-ary function type (τ 1 , . . . , τ n ) → τ. In this case, a n-ary application b(b 1 , . . . , b n ) is generated, where b i is an uncurrying of a i at type τ i . The case of let bindings (rule TLET) is straightforward. For letrec bindings, rule TLETREC combines rules TABS and TLET. The recursive nature of the binding is apparent in the extra hypothesis x n : (τ 1 , . . . , τ n ) → τ introduced in the compilation environment when translating the left subterm of the binding. Rule TCOERCE accounts for most of the flexibility of our specification. It enables us to take an uncurrying b obtained at some type τ and turn it into an uncurrying b at another type τ , provided there exists a coercion from τ to τ that transforms b into b . (Typical examples of coercions are applications of the curry and uncurry combinators mentioned in Introduction.) Such a coercion is written b : τ =⇒ b : τ . A special case of coercion is subtyping, written τ <: τ , where the type changes but the result of the translation does not (b = b). We now define subtyping and coercion via inference rules, starting with the former.

τ <: τ (SREFL) τ 1 <: τ 2 τ 2 <: τ 3 (STRANS) τ 1 <: τ 3 → <: (SBASE) τ i <: τ i for i = 1, . . . , n τ <: τ (SFUN) (τ 1 , . . . , τ n ) → τ <: (τ 1 , . . . , τ n ) → τ
Subtyping is reflexive and transitive. The base case (rule SBASE) corresponds to → being a subtype of . As mentioned in section 2.2, a target term of type → is a fullycurried function and can therefore be injected in the type of constants or fully-curried functions. Subtyping then extends across function types as usual (rule SFUN): covariantly in the result type and contravariantly in the argument types. The following lemma (used in section 5.1) is an example of complex subtyping.

Lemma 1 Define the type τ n of curried functions of n arguments by

τ n = → • • • → n times → We have τ n <: for all n.
Proof The base case n = 0 is trivial by rule SREFL. For the inductive case, note that τ n+1 = → τ n . By induction hypothesis and rules SFUN and SREFL, we have → τ n <: → . By rule SBASE, → <: . We conclude by rule STRANS.

We now turn to the definition of coercions

b : τ =⇒ b : τ . τ <: τ (CSUB) b : τ =⇒ b : τ b : τ =⇒ b : τ b : τ =⇒ b : τ (CTRANS) b : τ =⇒ b : τ n > 0 (CCURRY) b : (τ 1 , . . . , τ n ) → τ =⇒ curry n (b) : τ 1 → . . . → τ n → τ n > 0 (CUNCURRY) b : τ 1 → . . . → τ n → τ =⇒ uncurry n (b) : (τ 1 , . . . , τ n ) → τ x n-i-1 : τ i =⇒ b i : τ i for i = 1, . . . , n x n (b 1 , . . . , b n ) : τ =⇒ b : τ (CFUN) b : (τ 1 , . . . , τ n ) → τ =⇒ (let b in λ n .b ) : (τ 1 , . . . , τ n ) → τ
Coercions are defined by three base cases (rules CSUB, CCURRY and CUNCURRY), which can be combined by transitivity (rule CTRANS) or extended across function types (rule CFUN). One base case is when τ is subtype of τ . Then, the coercion takes place without changing the term (b = b). The other two base cases correspond to applications of the curry n or uncurry n combinators. There is one such combinator for each arity n > 0, defined as:

curry n = λ 1 . λ 1 . . . λ 1 n times . x n (x n-1 , . . . , x 0 ) uncurry n = λ 1 . λ n . x n (x n-1 ) • • • (x 0 ) Source type τ Destination type τ Term b after coercion of b ( , ) → curry 2 (b) τ 1 → τ 2 → τ (τ 1 , τ 2 ) → τ uncurry 2 (b) → (( , ) → ) → let f = b in λ (x). f (curry 2 (x)) (τ 1 , τ 2 , τ 3 ) → τ τ 1 → (τ 2 , τ 3 ) → τ let f = curry 3 (b) in λ (x). uncurry 2 ( f (x)) (τ 1 , τ 2 , τ 3 ) → τ (τ 1 , τ 2 ) → τ 3 → τ uncurry 2 (curry 3 (b))
Table 1 Some examples of coercions or in more readable named notation:

curry n = λ ( f ). λ (y 1 ) . . . λ (y n ). f (y 1 , . . . , y n ) uncurry n = λ ( f ). λ (y 1 , . . . , y n ). f (y 1 ) • • • (y n )
As shown by rules CCURRY and CUNCURRY, these combinators mediate between the uncurried function type (τ 1 , . . . , τ n ) → τ and its curried counterpart τ 1 → . . . → τ n → τ. We could dispense with the curry n and uncurry n combinators and expand them at point of use, as in:

b : (τ 1 , τ 2 ) → τ =⇒ (let f = b in λ (x).λ (y). f (x, y)) : τ 1 → τ 2 → τ
replacing a function call by a cheaper let binding. However, the curry and uncurry combinators can be shared across several coercion sites, therefore reducing the overall code size. Finally, rule CFUN enables us to coerce from a function type (τ 1 , . . . , τ n ) → τ to another function type of the same arity, (τ 1 , . . . , τ n ) → τ . By covariance and contravariance, there must exist coercions from the result type τ to τ , and from each of the argument types τ i to τ i . These coercions are combined in the standard way: Note that the subtyping rule SFUN for function types is partially redundant with the coercion rule CFUN: SFUN could be removed without changing the set of type pairs (τ, τ ) between which coercions exist; however, the terms generated after coercion would be less efficient. For example, coercing b from → → to produces b if SFUN is available, but λ x. b(x) if it is not. More generally, systematic use of the subtyping rules avoids generating coercions that are β η-equivalent to the identity function; this is an easy but very profitable optimization. Table 1 shows some examples of coercions, using named notation.

b 1 : τ 1 . . . b n : τ n → f (b 1 , . . . , b n ) : τ ⇑ ⇑ ⇓ y 1 : τ 1 . . .
The first example combines rule CCURRY and subtyping to go from a 2-argument function to a fully-curried function. The third example illustrates the use of rule CFUN. The last two examples show that combinations of currying and uncurrying can build "semi-uncurried" functions that successively take (in a curried manner) groups of uncurried arguments.

An introduction to step-indexed logical relations

Many program transformations can be proved to preserve the semantics of programs using a purely syntactic correspondence between the terms and values appearing during the execution of the original program and those appearing during the execution of the transformed program, then showing that this correspondence is preserved by the dynamic semantics. In the case of first-order uncurrying, the first author developed a Coq proof of semantic preservation that follows this approach [START_REF] Dargaye | Décurryfication certifiée[END_REF]. However, this technique does not easily extend to the higher-order case.

For some program transformations, it is preferable to adopt a more semantic viewpoint and reason less on the syntactic shape of functions and more on their "input-output" behavior. In other words, the proof of semantic preservation relies on observational equivalence. For example, the two functions λ x. x +x and λ x. x ×2 are equivalent because they map identical integer arguments to identical integer results; therefore, one function can replace the other in any context. In the case of higher-order functional languages, function arguments can themselves be functions. Therefore, we would like to define a notion of equivalence between values such that:

-two constants are related if and only if they are equal; -two functions are related if and only if they map related arguments to related results.

However, this characterization is not a proper definition because it is circular: for instance, the argument to a function can be the function itself, in the case of a self-application.

One way to avoid this circularity and turn the characterization above into a proper definition is to stratify the language using types. This approach is known as logical relations [START_REF] Statman | Logical relations and the typed λ -calculus[END_REF]. Taking the simply-typed λ -calculus as an example, we would state that -two constants are related at a base type ι if and only if they are equal and belong to ι; -two functions are related at type τ 1 → τ 2 if and only if they map arguments related at type τ 1 to results related at type τ 2 .

This is a well-founded notion because the definition of the "is related to" relation at type τ involves only the same relation at strict sub-terms of τ. However, this type-based stratification does not apply to all type systems. For example, recursive types, ML/Haskell-style datatypes or ML-style references reintroduce circularity in the characterization of logical relations. A fortiori, the type-based stratification is useless for untyped or weakly-typed languages, such as the source and target languages of our uncurrying transformation.

To circumvent this difficult, Appel and McAllester [START_REF] Appel | An indexed model of recursive types for foundational proof-carrying code[END_REF] introduced step-indexed logical relations, a variant of Statman's logical relation where the definition is well-founded not by induction on types, but by induction on the number of computational steps performed by the terms under consideration. More precisely, step-indexed logical relations do not directly capture the fact that two terms are observationally equivalent in the absolute, but only the fact that two terms cannot be distinguished in k steps of computation, where k can be chosen arbitrarily large. Taking the call-by-value λ -calculus with constants as an example, two terms M and N are indistinguishable in k steps if and only if:

-for all j ≤ k, if M reduces to a value v in j steps of β -reduction, there exists a value w such that N reduces to w (in any number of steps) and v and w are indistinguishable in k -j steps.

(We focus here on observational equivalence for terminating terms. Non-termination is discussed in section 6.) Likewise, two values v and w are indistinguishable in k steps if and only if:

-v and w are identical constants, or -v = λ x.M, w = λ y.N, and for all j < k and all arguments v , w indistinguishable in j steps, the terms M{x ← v } and N{y ← w } are indistinguishable in j steps.

In the last case above, note that M{x ← v } will run for at most j steps. In particular, if v is a function and M applies it, the function v cannot run for more than j steps. Therefore, it suffices that v and w are indistinguishable for j steps. The definition of "being indistinguishable" above is well-founded by induction on the number k of steps. In particular, in the case of function values, the arguments v , w are compared for j < k steps and the results v , w are compared for j -i steps, where i ≤ j is the length of the reduction sequence M{x ← v } * → v , and therefore j -i < k. Appel and McAllester [START_REF] Appel | An indexed model of recursive types for foundational proof-carrying code[END_REF] and Ahmed [START_REF] Ahmed | Step-indexed syntactic logical relations for recursive and quantified types[END_REF] use the step-indexed approach to define unary and binary logical relations, leading to PER-style models, for rich type system including recursive types and quantifiers. Acar et al. [START_REF] Acar | Imperative self-adjusting computation[END_REF] use step-indexed logical relations in an untyped setting to prove a consistency property of a non-deterministic operational semantics. In the next section, we use step-index logical relations in a weakly-typed setting to show the correctness of the uncurrying transformation defined in section 2.3. Values are defined coinductively (that is, as finite or infinite regular terms satisfying the grammar above), so that we can use cyclic closures to represent the values of recursive functions. For example, evaluating letrec λ .a in . . . in an environment e produces the cyclic closure v = (λ .a)[v.e], an infinite but regular term. When this closure is invoked, variable x 1 is correctly bound to v, that is, the closure of the function itself. This device was introduced by Landin [START_REF] Landin | The mechanical evaluation of expressions[END_REF] and is also used in the Categorical Abstract Machine [START_REF] Cousineau | The categorical abstract machine[END_REF]. It is convenient to unify the treatment of recursive and non-recursive functions.

Reduction semantics with environments and function closures can be defined following the λ σ -calculus [START_REF] Abadi | Explicit substitutions[END_REF]. However, the Coq mechanization is further simplified if we use natural (big-step) semantics instead of reduction (small-step) semantics.

The dynamic semantics for the source language is therefore of the form e a n ⇒ v, meaning "in environment e, term a evaluates in n steps to the value v". This judgment is defined by the inference rules shown in figure 1. The rules are standard except for (1) the use of cyclic closures in the rule for letrec, as explained above, and (2) the addition of the index n, which counts the number of β -reductions (of functions and let/letrec bindings) performed during evaluation. It is easy to check that e a n ⇒ v holds if and only if a reduces

e(n) = v e x n 0 ⇒ v e c 0 ⇒ c e λ .a 0 ⇒ (λ .a)[e] e a 1 i ⇒ (λ .a )[e ] e a 2 j ⇒ v 2 v 2 .e a k ⇒ v n = i + j + k + 1 e a 1 a 2 n ⇒ v e a 1 i ⇒ v 1 v 1 .e a 2 j ⇒ v n = i + j + 1 e let a 1 in a 2 n ⇒ v v 1 = (λ .a 1 )[v 1 .e] v 1 .e a 2 i ⇒ v n = i + 1 e letrec λ .a 1 in a 2 n ⇒ v
Fig. 1 Indexed natural semantics for the source language

f (n) = w f x n ⇒ w f c ⇒ c f λ n .b ⇒ (λ n .b)[ f ] f b ⇒ (λ n .b )[ f ] f b i ⇒ w i for i = 1, . . . , n w n . . . w 1 . f b ⇒ w f b(b 1 , . . . , b n ) ⇒ w f b 1 ⇒ w 1 w 1 . f b 2 ⇒ w f let b 1 in b 2 ⇒ w v 1 = (λ n .b 1 )[v 1 .e] v 1 .e b 2 ⇒ v e letrec λ n .b 1 in b 2 ⇒ v
Fig. 2 Natural semantics for the target language to a value related to v by a sequence of exactly n reductions. As explained in section 3, this count of reductions n is crucial in defining logical relations between the source and target languages. The dynamic semantics for the target language is also given in natural semantics, as a predicate f b ⇒ w ("in environment f , the term b evaluates to the value w"), following the inference rules of figure 2. The semantics is not instrumented to count the number of evaluation steps, since this is not needed to define logical relations. In the rule for function applications, note that the number n of arguments provided must exactly match the arity of the function closure being applied, otherwise execution goes wrong.

Relating values and computations between the source and target languages

Using the step-indexed approach summarized in section 3, we now define the following relations between terms or values of the source and target language that serve as the main invariants in our proof of semantic preservation: -a / e k ≈ w : τ the source term a in environment e is related to the target value w at type τ for up to k computation steps.

We abbreviate "related for up to k computation steps", or equivalently "indistinguishable in k steps", as "k-related". These three relations are specified by the following pseudo-inference rules. As in rule (R2), we consider j-related argument values v and w, with j < k, and computations of the application of (λ .a)[e] to v that run for i ≤ j steps. However, there is no computation to be performed on the target language side. Therefore, we relate the computation a / v.e of the source language with the value (λ n-1 .b)[w. f ] or the target language, using the mixed relatedness relation defined by rule (R5) and explained below. This target value (λ n-1 .b)[w. f ] logically represents the application of (λ n .b)[ f ] to w. Such a partial application is not permitted by the semantics of the target language, but can easily be represented at the level of target values. Rule (R4) defines k-relatedness between two computations: whenever the source computation a / e terminates on a value v in j ≤ k steps, the target computation b / f must terminate on a value w that is (k -j)-related to v. Rule (R5) defines k-relatedness between a computation a / e of the source language and a value w of the target language.

c k ≈ c : (R1) τ = τ 1 → τ 2 or τ = τ 1 = τ 2 = ∀ j, v, w, j < k ∧ v j ≈ w : τ 1 =⇒ a / v.e j ≈ b / w. f : τ 2 (R2) (λ .a)[e] k ≈ (λ 1 .b)[ f ] : τ n ≥ 2 ∀ j, v, w, j < k ∧ v j ≈ w : τ 1 =⇒ a / v.e j ≈ (λ n-1 .b)[w. f ] : (τ 2 , . . . , τ n ) → τ (R3) (λ .a)[e] k ≈ (λ n .b)[ f ] : (τ 1 , . . . , τ n ) → τ ∀ j, v, j ≤ k ∧ (e a j ⇒ v) =⇒ ∃w, ( f b ⇒ w) ∧ v k-j ≈ w : τ (R4) a / e k ≈ b / f : τ ∀ j, v, j ≤ k ∧ (e a j ⇒ v) =⇒ v k-j ≈ w : τ (
As in rule (R4), we consider evaluations of a / e that terminate on a value v in j ≤ k steps. Then, since there are no computations to perform on the target side, we just require that the result value v is related to the given value w in k -j steps. Rules (R1) to (R5) do not constitute a proper inductive definition by an inference system, because the underlying inference operator is not monotone [START_REF] Aczel | An introduction to inductive definitions[END_REF]. Nonetheless, it admits a smallest fixpoint: Proof Treating rules (R4) and (R5) as equivalences between their premises and their conclusions, and expanding these equivalences in rules (R2) and (R3), we see that v k ≈ w : τ is uniquely defined in terms of v j ≈ w : τ for j < k, as mentioned in section 3. Existence and uniqueness then follow by Peano induction over k. In Coq, Peano induction -defining f (n) in terms of { f (p) | p < n} -is not a primitive notion: only structural recursiondefining f (n + 1) in terms of f (n) -is primitive. We therefore use Noetherian induction on the well-founded ordering < over the natural numbers [9, chap. 15]. The proof uses the axioms of function extensionality ( f = g if ∀x, f (x) = g(x)) and proof irrelevance (any two proofs of the same proposition are equal). These two axioms are not provable in Coq but consistent with Coq's predicative logic.

An obvious but important property of k-relatedness is that it is decreasing in k: if two values are indistinguishable in k computation steps, they are a fortiori indistinguishable in k ≤ k steps.

Lemma 3 If v k ≈ w : τ, then v k ≈ w : τ for all k ≤ k.
Proof Straightforward by definition of k-relatedness.

The following lemma gives necessary and sufficient conditions for two trivial computations (of constants, abstractions and variables) to be related. The following two lemmas show that related functions map related arguments to related results, as desired. Lemma 5 corresponds to unary "untyped" applications, where the functions are related at type . Lemma 6 corresponds to n-ary applications, curried on the source side, uncurried on the target side, where the functions are related at a n-ary function type. ⇒ v with p + q + r + 1 = j ≤ k. Exploiting the two hypotheses, it follows that there exist w f and w such that

Lemma 4 1. c / e k ≈ c / f : τ ⇐⇒ c k ≈ c : τ ⇐⇒ c = c ∧ τ =
f b ⇒ w f (λ .a 1 )[e 1 ] k-p ≈ w f : (1) f b ⇒ w v k-q ≈ w :
From ( 1) and (R2) and (R4), it follows that w f is of the form (λ 1 .b 1 )[ f 1 ], and moreover there exists w such that w . Proof As in the previous proof, consider an evaluation e a a 1 . . . a n j ⇒ v in j ≤ k steps. By induction over n and inversion of this evaluation, we obtain values v i , intermediate closures (λ .a i )[e i ] and counts p i , q i such that

f 1 b 1 ⇒ w v k-j
e a i q i ⇒ v i (i = 1, . . . , n) e a p 0 ⇒ (λ .a 1 )[e 1 ] v i-1 .e i-1 a i-1 p i-1 ⇒ (λ .a i )[e i ] (i = 2, . . . , n) v n .e n a n p n ⇒ v j = p 0 + • • • + p n + q 1 + • • • + q n + (n + 1)
Exploiting the first hypothesis, there exists w f such that

f b ⇒ w f (λ .a 1 )[e 1 ] k-p 0 ≈ w f : (τ 1 , . . . , τ n ) → τ (1)
By (R3), it follows that w f is of the form (λ n .b )[ f ]. A second induction over n, exploiting (1)
and the second hypothesis, shows that there exists a list of values w 1 , . . . , w n and a value w such that

f b i ⇒ w i (i = 1, . . . , n) w n . . . w 1 . f b ⇒ w v k-j ≈ w : τ
The expected result follows.

The definition of k-relatedness at uncurried function types (τ 1 , . . . , τ n ) → τ with n > 1 (rule (R3)) is convenient to perform inductions over n, but somewhat mysterious. It is instructive

to spell it out in the case n = 2. What does (λ .a)[e] k ≈ (λ 2 .b)[ f ] : (τ 1 , τ 2 ) → τ entails?
Ignoring step counts for the moment, this relation entails two guarantees. The first guarantee is a weak soundness property: applying (λ .a)[e] to one suitable value v 1 (suitable meaning related to some value w 1 ) cannot produce a constant: the result, if it exists, must be a closure that we can further apply to a second argument. The second guarantee is that if we apply (λ .a)[e] successively to two arguments v 1 and v 2 , which are related to values w 1 and w 2 respectively, and obtain a result v, the application of (λ 2 .b)[ f ] to the two arguments w 1 and w 2 succeeds and returns a result w that is related to v. To formalize this discussion and generalize it from n = 2 to any n > 1, we introduce two predicates M and R:

-M (k, τ 1 . . . τ n , v) captures the fact that the source value v can safely be applied in a curried fashion to n values matching types τ 1 , . . . , τ n : none of the intermediate application will return a value other than a closure. -R(k, τ 1 . . . τ n , v 1 . . . v n , w 1 . . . w n , v, v , p) says that the values v i and w i are pairwise related at types τ i and for decreasing numbers of steps j n < . . . < j 1 < k. The value v is the result of applying v successively to v 1 , . . . , v n . The count p is the number of steps that were not consumed by the evaluation of this curried application and remain available to observe the result value v .

These two predicates are defined by the following inference rules. (ε stands for the empty list.)

M (k, ε, v) ∀i, j, v, v , w, i < k ∧ j ≤ i ∧ v i ≈ w : τ ∧ v.e a j ⇒ v =⇒ M (i -j, - → τ , v ) M (k, τ. - → τ , (λ .a)[e]) R(k, ε, ε, ε, v, v, k) i < k j ≤ i v i ≈ w : τ v.e a j ⇒ v R(i -j, - → τ , - → v , - → w , v , v , p) R(k, τ. - → τ , v. - → v , w. - → w , (λ .a)[e], v , p)
We can then give an alternate characterization of k-relatedness at function types, which will be useful in proving theorem 11 below.

Lemma 7 v k ≈ w : (τ 1 , . . . , τ n ) → τ holds if and only if 1. n > 0; 2. w = (λ n .b)[ f ] for some b and f ; 3. M (k, τ 1 . . . τ n , v); 4. for all - → v , - → w , v and p, R(k, τ 1 . . . τ n , - → v , - → w , v, v , p) =⇒ ∃w , ← - w . f b ⇒ w ∧ v p ≈ w : τ.
(The notation ←w denotes the list of values -→ w in reverse order.)

Proof By induction over n. Refer to the Coq development for a detailed proof.

Correctness of subtyping and coercions

Having defined semantic correspondences between values of the source and target languages, we can now show that subtyping and coercions are sound with respect to these correspondences. For subtyping, we show that any pair of computations related at a type τ are also related at any supertype τ of τ. The proof proceeds by induction on the derivation of τ <: τ and case analysis on the last rule used. The cases of rules SREFL and STRANS are trivial. For rule SBASE, we have τ = → and τ = . The result follows immediately from (R2). Finally, the case of rule SFUN follows from an induction on the number n of function parameters.

We now consider the semantic effect of the curry n and uncurry n combinators. If the computations a in e and b in f are related at a n-ary function type (τ 1 , . . . , τ n ) → τ, it is the case that the computations a in e and curry n (b) in f are related at the corresponding curried function type.

Lemma 9 If a / e k ≈ b / f : (τ 1 , . . . , τ n ) → τ and n > 0, then a / e k ≈ curry n (b) / f : τ 1 → . . . → τ n → τ Proof Consider two closures (λ n .b 1 )[ f 1 ] and (λ n .b 2 )[ f 2 ]
of the target language such that, for all arguments w 1 , . . . , w n and result w,

w n . . . w 1 . f 1 b 1 ⇒ w implies w n . . . w 1 . f 2 b 2 ⇒ w (1)
By induction on n, we first show that

v k ≈ (λ n .b 1 )[ f 1 ] : (τ 1 , . . . , τ n ) → τ implies v k ≈ (λ 1 . . . λ 1 n times .b 2 )[ f 2 ] : τ 1 → . . . τ n → τ (2)
Exploiting the first hypothesis with (R4), we obtain that if a in e evaluates to v in j ≤ k

steps, b in f evaluates to a closure (λ n .b 1 )[ f 1 ] such that v k-j ≈ (λ n .b 1 )[ f 1 ] : (τ 1 , . . . , τ n ) → τ. The application curry n (b), then, evaluates to the closure (λ 1 . . . λ 1 n times .b 2 )[ f 2 ] with b 2 =
x n (x n-1 , . . . , x 0 ) and f 2 = (λ n .b 1 ). f . It is easy to check that the hypothesis (1) above is satisfied. The expected result follows from (2).

Unsurprisingly, the uncurry n combinator enjoys a semantic property that is exactly symmetrical to that of curry n .

Lemma 10 If n > 0 and a / e k ≈ b / f : τ 1 → . . . → τ n → τ, then a / e k ≈ uncurry n (b) / f : (τ 1 , . . . , τ n ) → τ.
Proof The proof is roughly similar to that of lemma 9, and we omit it.

We can now prove the main semantic preservation result for coercions: if a target term b in f is related at type τ to a source term a in e, and the coercion of b from type τ to type τ produces a term b , then a in e and b in f are related at type τ .

Theorem 11 If b : τ =⇒ b : τ , then a / e k ≈ b / f : τ implies a / e k ≈ b / f : τ .
Proof The proof proceeds by induction on the derivation of b : τ =⇒ b : τ and case analysis on the last rule used. The cases of rules CSUB, CCURRY and CUNCURRY correspond to lemmas 8, 9 and 10, respectively. The transitivity case (rule CTRANS) is trivial by induction hypothesis. The difficult case is that of rule CFUN, where the initial type is (τ 1 , . . . , τ n ) → τ and the final type is (τ 1 , . . . , τ n ) → τ . The premises of the rule are:

-x n-i-1 : τ i =⇒ b i : τ i for i = 1, . . . , n -x n (b 1 , . . . , b n ) : τ =⇒ b : τ
and the corresponding induction hypotheses hold. We use the alternate characterization of k-relatedness at function types provided by lemma 7, and show the following properties by induction over n and exploitation of the induction hypotheses for the argument types:

-If M (k, τ 1 . . . τ n , v), then M (k, τ 1 . . . τ n , v). -If R(k, τ 1 . . . τ n , v 1 . . . v n , w 1 . . . w n , v, v , p), there exists values w 1 , . . . , w n such that R(k, τ 1 . . . τ n , v 1 . . . v n , w 1 . . . w n , v, v , p) and w n . . . w 1 . f b i ⇒ w i for i = 1, . . . , n.
The result then follows from these two properties and lemma 7. Proof The proof is similar to that of lemma 13, except that in the base cases we need to assume that v j ≈ w : τ f in order to prove that v.e j ≈ w. f : τ f .Γ . Fortunately, this assumption is needed only for j < k, therefore breaking circularity. The result thus follows by Peano induction over the number of steps k.

Proof (of theorem 12)

The proof of theorem 12 proceeds by induction on the derivation of Γ a =⇒ b : τ and case analysis on the last rule used. Cases TVAR and TCST follow from lemma 4, parts 1 and 3. Case TABS follows from lemmas 13 and 4 (part 2). Lemmas 5 and 6 show cases TAPP-and TAPP-N, respectively. The case of let bindings (TLET) is straightforward. For letrec bindings (TLETREC), we use lemma 14. Finally, the case of rule TCOERCE follows from lemma 11.

As a corollary, we obtain the desired semantic preservation property for whole programs. This section presents two applications of the general framework developed in sections 2 and 4. The first application is a simple proof of correctness for a first-order uncurrying transformation similar to those used in GHC and OCaml. The second application is a generic translator cum validator that exploits the results of any external, untrusted static analysis for higher-order uncurrying after verifying their correctness.

First-order uncurrying

Following [START_REF] Dargaye | Décurryfication certifiée[END_REF], the first-order uncurrying transformation presented here maintains a compile-time environment Θ associating arity information to free variables. The compile-time arity of a variable is either K(n), meaning that the value of this variable is an uncurried function of n arguments, or U, meaning that nothing is known about this value and it is assumed to be fully curried. Owing to the first-order nature of the transformation, arguments and results of functions, even of known arity, are assumed to be fully curried and therefore have arity U.

The first-order uncurrying of a source term a in arity environment Θ , written T (Θ , a), is the target term b defined by the following recursive equations.

T (Θ , x p ) = curry n (x p ) if Θ (p) = K(n) and n > 1; x p otherwise T (Θ , c) = c T (Θ , λ .a) = λ 1 . T (U.Θ , a) T (Θ , x p a 1 . . . a n ) = x p (T (Θ , a 1 ), . . . , T (Θ , a n )) if Θ (p) = K(n) T (Θ , a a ) = T (Θ , a)(T (Θ , a )) otherwise T (Θ , let λ . . . λ n times .a in a ) = let λ n .T (U . . .U n times .Θ , a) in T (K(n).Θ , a ) T (Θ , let a in a ) = let T (Θ , a) in T (U.Θ , a ) otherwise T (Θ , letrec λ . . . λ n times .a in a ) = letrec λ n .T (U . . .U n times .K(n).Θ , a) in T (K(n).Θ , a )
Uncurrying is performed along the lines mentioned in Introduction. Curried functions of n arguments bound by let or letrec are transformed into uncurried functions and associated with arity information K(n) within their scope. Anonymous functions are never uncurried. The curried application of a variable x of arity information K(n) to exactly n arguments is turned into an n-ary application. Any other use of a variable x of arity K(n), n > 1 is translated to curry n (x), therefore recovering a fully-curried function.

Semantic preservation for this uncurrying transformation follows easily from the results of section 4. We first define the obvious translation from arity information and arity environments to representation types and representation environments:

[[U]] = [[K(n)]] = ( , . . . , n times ) → [[Θ ]] = [[ρ 0 ]] . . . [[ρ n ]] if θ = ρ 0 . . . ρ n Theorem 16 If T (Θ , a) = b, then [[Θ ]] a =⇒ b : .
Proof The proof proceeds by structural induction over a and analysis on the corresponding case of the definition of T . We show the non-obvious cases.

Case a = x p . If Θ (p) = U, the result follows from rule TVAR. If Θ (p) = K(1), rule TVAR shows [[Θ ]] x p =⇒ x p : → . Since → <: , an application of rule TCOERCE concludes. If Θ (p) = K(n) with n > 1,
we also apply TCOERCE to go from ( , . . . , ) → to , using rule CCURRY first to go to → • • • → , then rule CSUB and lemma 1 to go to type .

Case a = λ .a . Follows from the induction hypothesis, rule TABS (with n = 1), and TCOERCE with the trivial coercion from → to . Proof Follows from theorem 16 and corollary 15.

Validating translation

Strategies for performing higher-order uncurrying have not been studied yet, and are likely to build on non-trivial static analyses. Instead of proving the correctness of one such strategy, we now develop and prove correct a generic translator that exploits the results of any external strategy. These results are not trusted: instead, the translator explicitly validates them and raises a compile-time error if they are not correct. This approach is inspired by translation validation [START_REF] Pnueli | Translation validation. In: Tools and Algorithms for Construction and Analysis of Systems[END_REF][START_REF] Necula | Translation validation for an optimizing compiler[END_REF] and proof-carrying code [START_REF] Necula | Proof-carrying code[END_REF][START_REF] Appel | Foundational proof-carrying code[END_REF]. As remarked by Tristan and Leroy [START_REF] Tristan | Formal verification of translation validators: A case study on instruction scheduling optimizations[END_REF], a strength of this approach is that it suffices to prove the soundness of the generic validating translation (if it does not fail, the produced code is correct): the external strategy need not be proved correct, and we can experiment with several such strategies without having to re-do any formal proofs.

The results of the external strategy for uncurrying are transmitted to the validating translation as source terms annotated with representation types and explicit coercions. These annotations are underlined in the grammar below.

Annotated source terms:

A

::= x n | c | λ n : τ 1 . . . τ n . A curried function of n arguments | A A | let A in A | letrec λ n .A: (τ 1 . . . τ n ) → τ in A | (A : τ) coercion to representation type τ
The external uncurrying strategy is responsible for annotating function parameters and recursive function declarations with their desired representation types. To further reflect the decisions taken by the strategy, curried abstractions are syntactically delimited in annotated terms.

Example 18 Consider the following unannotated source term (a simplified version of the map2 example from section 1.4):

let app2 = λ f .λ y.λ z. f y z in app2 (λ y.λ z.y + z) 0 1
The uncurrying strategy can choose to uncurry app2, its f parameter, and the λ y.λ z.y + z anonymous function, resulting in the following annotated term:

let app2 = λ 3 ( f : ( , ) → )(y : )(z : ). f y z in app2 (λ 2 (y : )(z : ). y + z) 0 1
If, on the other hand, the strategy chooses to leave the f parameter curried but still uncurry the anonymous function, it must insert an explicit coercion at point of call, obtaining the following annotated term:

let app2 = λ 3 ( f : → )(y : )(z : ). f y z in app2 (λ 2 (y : )(z : ). y + z : → ) 0 1
Annotated source terms support partial applications and over-applications just like source terms: for a curried function λ n : τ 1 . . . τ n . A, there is no requirement that it receives n arguments at once in a single curried application. Indeed, the semantics of annotated source terms is exactly that of source terms after erasing the annotations. Erasure of annotations, written A↓, produces a source term defined as follows:

x n ↓ = x n c↓ = c (λ n : τ 1 . . . τ n . A)↓ = λ . . . λ n times . A↓ (A A )↓ = A↓ A ↓ (let A in A )↓ = let A↓ in A ↓ (letrec λ n .A : (τ 1 . . . τ n ) → τ in A )↓ = letrec λ . . . λ n times . A↓ in A ↓ (A : τ)↓ = A↓ S ( , ) = true (1) S ( → τ, ) = S (τ, ) (2)
S ((τ 1 , . . . , τ n ) → τ, (τ 1 , . . . , τ m ) → τ ) = n = m ∧ S (τ 1 , τ 1 ) ∧ . . . ∧ S (τ n , τ n ) ∧ S (τ, τ ) (3)
S (τ, τ ) = false otherwise ( 4)

C (b, τ, τ ) = b if S (τ, τ ) (5)
C (b, (τ 1 , . . . , τ n ) → τ, ) = C (b, (τ 1 , . . . , τ n ) → τ, → ) (6)
C (b, (τ 1 , . . . , τ n ) → τ, (τ 1 , . . . , τ n ) → τ ) = let b in λ n .b (7) if C (x n-i-1 , τ i , τ i ) = b i for i = 1, . . . , n and C (x n (b 1 , . . . , b n ), τ, τ ) = b C (b, (τ 1 , . . . , τ n ) → τ, τ 1 → τ ) = C (curry n (b), τ 1 → • • • → τ n → τ, τ 1 → τ ) (8)
if n > 1

C (b, τ 1 → τ, (τ 1 , . . . , τ n ) → τ ) = uncurry n (b ) (9)
if

C (b, τ 1 → τ, τ 1 → • • • → τ n → τ ) = b and n > 1 C (b, (τ 1 , . . . , τ n ) → τ, (τ 1 , . . . , τ m ) → τ ) = uncurry m (b ) (10)
if

C (curry n (b), τ 1 → • • • → τ n → τ, τ 1 → • • • → τ m → τ ) = b and n > 1 and m > 1 and n = m C (b, τ, τ ) = / 0 otherwise (11)

Fig. 3 Construction of coercions

The validating translation that we consider in this section takes as input an annotated term A and a representation environment Γ . It is defined in figure 4 as the function V (Γ , A). It checks that the annotations on A are consistent and, if so, returns the representation type τ for A and its translation b (a target term). Option types are used to represent failure: the result of V (Γ , A) is τ, b (read: "some τ and b") in case of success and / 0 (read: "none") in case of failure. Three auxiliary functions, defined in figures 3 and 4, are used: The validating translation V resembles a type-checker for the pseudo type system of section 2.3, augmented with the generation of the translation b. The cases of the definition of V (figure 4) are straightforward. For applications (case 16), it considers maximal curried applications A A 1 • • • A n where A is not an application, recursively validates and translates A, A 1 , . . . , A n to b, b 1 , . . . , b n , then checks (using function A ) that the types of the b i agree with that of b, and groups the b i into a sequence of k-ary applications as dictated by the type of the function b.

-S (τ, τ ) = false | true decides whether τ is a subtype of τ ; -C (b, τ, τ ) = / 0 | b builds the coercion b of b from type τ to type τ ; -A (τ, b, (τ 1 , b 1 ) . . . (τ n , b n )) = / 0 | τ ,
The auxiliary function S (τ, τ ) in figure 3 is a decision procedure for the subtyping relation. Its definition can be understood as a syntax-directed variant of the rules defining the <: predicate, where transitivity is used only where strictly necessary.

The most delicate algorithm is function C (b, τ, τ ), which determines whether there exists a coercion from type τ to type τ , and if so applies it to b (figure 3). The algorithm

V (Γ , x n ) = τ, x n if Γ (n) = τ (12) V (Γ , c) = , c (13)
V (Γ , λ n : τ 1 . . . τ n . A) = (τ 1 , . . . , τ n ) → τ, λ n . b (14) if n > 0 and V (τ n . . . τ 1 .Γ , A) = τ, b (15)
V (Γ , A A 1 • • • A n ) = A (τ, b, (τ 1 , b 1 ) . . . (τ n , b n )) (16)
if A is not an application and

V (Γ , A) = τ, b and V (Γ , A i ) = τ i , b i for i = 1, . . . , n V (Γ , (let A in A )) = τ , (let b in b ) (17) if V (Γ , A) = τ, b and V (τ.Γ , A ) = τ , b V (Γ , (letrec λ n .A : (τ 1 , . . . , τ n ) → τ in A )) = τ , (letrec λ n .b in b ) (18) if V (τ n . . . τ 1 .((τ 1 , . . . , τ n ) → τ).Γ , A) = τ, b and V (((τ 1 , . . . , τ n ) → τ).Γ , A ) = τ , b V (Γ , (A : τ)) = τ, b (19) if V (Γ , A) = τ , b and C (b , τ , τ) = b V (Γ , A) = / 0 otherwise (20) A (τ, b, ε) = τ, b (21)
A ( , b, ( , b 1 ).L) = A ( , b(b 1 ), L) (22) A ((τ 1 , . . . , τ n ) → τ, b, (τ 1 , b 1 ) . . . (τ n , b n ).L) = A (τ, b(b 1 , . . . , b n ), L) (23)
A (τ, b, L) = / 0 otherwise [START_REF] Leroy | The ZINC experiment: an economical implementation of the ML language[END_REF] Fig. 4 The validating translation compares the shapes of τ and τ . In case 6, coercing from a function type to reduces to coercing from this function type to → . Coercion between two function types is handled by cases 7 to 10, depending on the arities of the function types. If the arities match (case 7), the argument and result types are recursively coerced and combined following rule CFUN. Otherwise, the curry and uncurry combinators are applied as appropriate to reduce functions of 2 or more arguments to unary functions, and coercion is recursively attempted between the resulting unary function types.

Example 19 Consider again the annotated terms given in example 18. Executed on the annotated term let app2 = λ 3 ( f : ( , ) → )(y : )(z : ). f y z in app2 (λ 2 (y : )(z : ). y + z) 0 1 and the empty translation environment, the validating translation succeeds and produces the uncurried term let app2 = λ ( f , y, z). f (y, z) in app2 ((λ (y, z). y + z), 0, 1)

With the other annotation considered, let app2 = λ 3 ( f : → )(y : )(z : ). f y z in app2 (λ 2 (y : )(z : ). y + z : → ) 0 1 a curry 2 coercion from × → to → is introduced, and we obtain let app2 = λ ( f , y, z) f (y)(z) in app2 (curry 2 (λ (y, z). y + z), 0, 1)

Finally, if given the following incorrectly-annotated source term let app2 = λ 3 ( f : → )(y : )(z : ). f y z in app2 (λ 2 (y : )(z : ). y + z) 0 1 the translation reports an error because the type of the first effective argument to app2, namely × → , does not match the expected type for its first argument, → . Case [START_REF] Landin | The mechanical evaluation of expressions[END_REF] of figure 4 therefore does not apply.

Concerning termination, V and A are syntax-directed and therefore terminate trivially. In the case of S (τ, τ ), the sum of the sizes of τ and τ (i.e. the number of → constructors in both types) decreases strictly at each recursive call. Termination of C (b, τ, τ ) is more elusive. Define the following positive measure for the ordered pair (τ, τ ):

(τ, τ ) = τ + τ + 3 if τ = ; 0 otherwise.
Here, τ is the following nonstandard size for a type τ, which gives additional weight to function types of arity 2 or more:

= 1 τ 1 → τ = 1 + τ + τ 1 (τ 1 , τ 2 , . . . , τ n ) → τ = 1 + τ + τ 1 + (2 + τ 2 ) + • • • + (2 + τ n )
With these unnatural definitions, we have (τ 1 , τ 2 , . . . ,

τ n ) → τ > τ 1 → • • • → τ n → τ if n ≥ 2.
Moreover, (τ, ) > (τ, → ) . This guarantees that the measure of the two type arguments of C strictly decreases at each recursive call, ensuring termination. We now prove the soundness of the validating translation: if V (Γ , A) succeeds and returns τ, b , then b is a correct translation of the erasure A↓ at type τ according to the specification of section 2.3. It follows that b preserves the semantics of A↓.

Theorem 20 The validating translation is sound:

1. If S (τ, τ ) = true, then τ <: τ holds. 2. If C (b, τ, τ ) = b , then b : τ =⇒ b : τ holds. 3. If V (Γ , A) = τ, b , then Γ A↓ =⇒ b : τ.
Proof The three parts are proved successively by induction on the recursion structure of the corresponding algorithms. For parts 1 and 2, each case of the definition of S and C corresponds to a combination of inference rules defining the subtyping and coercion predicates. For example, in case 2 of S , the induction hypothesis shows that τ <: , from which we can build the following subtyping derivation: Soundness is the essential property of a validating translation such as the V function. However, some evidence that it works well in practice is also needed: for instance, a validating translation that always fails is correct but useless. In the case of V , we provide evidence of usability in the form of a completeness result with respect to the specification from section 2.3: if there exists a valid uncurrying b of the unannotated source term a according to this specification, or more formally if Γ a =⇒ b : τ holds, then there exists an annotation A of a such that V (Γ , A) does not fail; indeed, there exists an uncurrying b such that V (Γ , A) = τ, b . In other words, it is always possible for the external uncurrying strategy to annotate the source term a in a way that will be accepted by the validating translation. Note that, in general, the uncurrying b produced by the validating translation is not identical to the uncurrying b produced by the specification. However, both uncurryings are semantically correct. Proof The proof of part 3 is a simple induction on the derivation of Γ a =⇒ b : τ. To construct the annotated term A, we insert coercions in two places: 1-whenever the original derivation uses rule TCOERCE, and 2-when dealing with a curried application a a 1 • • • a n , in which case we insert a trivial coercion around the annotation of a, so that the recognition of maximal curried applications performed by V stops at a and does not try to decompose it further into applications. The proof of part 1 is an induction on the derivation of τ <: τ . We first need to show that S , viewed as a relation, is reflexive and transitive, which is easy to do by structural induction over types.

<: (SREFL) τ <: (SFUN) → τ <: → → <: (SBASE) (STRANS) → τ <:
Part 2 is the most difficult part of the proof. We first axiomatize the changes in types performed by the various cases of the C function, using the inference rules given in figure 5. These rules define the predicate τ =⇒ τ , read: "τ can be coerced to τ according to the algorithm C ". A simple induction over the derivation of τ =⇒ τ shows that τ =⇒ τ implies ∀b, C (b, τ, τ ) = / 0 as expected. It remains to show that b : τ =⇒ b : τ implies τ =⇒ τ . As in part 1, this is proved by induction over the derivation of b : τ =⇒ b : τ . The only difficult case is rule CTRANS, for which we need to prove some rather delicate transitivity properties: As a final note, the Coq formalization models algorithms S , C and V as computable functions. These functions can be executed directly within Coq (this is how we obtained the examples of coercions shown in table 1), or automatically translated to efficient OCaml code via Coq's extraction facility [START_REF] Letouzey | Extraction in Coq: An overview[END_REF].

(4) S (τ 1 , τ 2 ) = true and τ 2 =⇒ τ 3 imply τ 1 =⇒ τ 3 . (5) τ 1 =⇒ τ 2 and S (τ 2 , τ 3 ) = true imply τ 1 =⇒ τ 3 . (6) τ 1 =⇒ τ 2 and τ 2 =⇒ τ 3 imply τ 1 =⇒ τ 3 . S (τ, τ ) = true (5) τ =⇒ τ (τ 1 , . . . , τ n ) → τ =⇒ → (6) (τ 1 , . . . , τ n ) → τ =⇒ τ i =⇒ τ i for i = 1, . . . , n τ =⇒ τ (7) (τ 1 , . . . , τ n ) → τ =⇒ (τ 1 , . . . , τ n ) → τ n > 1 τ 1 → • • • → τ n → τ =⇒ τ 1 → τ (8) (τ 1 , . . . , τ n ) → τ =⇒ τ 1 → τ n > 1 τ 1 → τ =⇒ τ 1 → • • • → τ n → τ (9) τ 1 → τ =⇒ (τ 1 , . . . , τ n ) → τ n > 1 m > 1 n = m τ 1 → • • • → τ n → τ =⇒ τ 1 → • • • → τ m → τ (10) (τ 1 , . . . , τ n ) → τ =⇒ (τ 1 , . . . , τ m ) → τ

Semantic preservation for non-terminating programs

The semantic preservation result proved in section 4 shows that the uncurrying transformation is correct, but only for terminating programs: if the original program diverges, nothing is known about the behavior of its possible uncurryings; they could diverge as well, as expected, but also terminate, or go wrong. This is not a problem in the application scenario that we initially envisioned, namely uncurrying programs extracted from Coq specifications, since the type system of Coq guarantees that all extracted programs are strongly normalizing. Nonetheless, to perform higher-order uncurrying in a general-purpose compiler for a functional language, it would be desirable to show that uncurrying preserves non-termination as well. This raises two difficulties that we now discuss. Reasoning directly over diverging executions in a step-indexed approach is difficult, because we lack the notion of "number of execution steps" to build inductive definitions and proofs. However, we can characterize divergence negatively: a computation diverges if, for all k, it neither terminates nor goes wrong within k steps. This characterization is amenable to reasoning by induction over the step count k.

Ahmed [START_REF] Ahmed | Step-indexed syntactic logical relations for recursive and quantified types[END_REF] shows how this approach leads to the definition of step-indexed relations that entail observational equivalence. Working in the context of a single, strongly-typed functional language equipped with reduction semantics, she first defines the step-indexed relation a ≤ k a : τ as "a and a have type τ and moreover if a evaluates to a value v in j ≤ k steps, then a evaluates in any number of steps to some value v that is related to v in k -j steps". Then, Ahmed defines the equivalence of two computations a ∼ = a : τ as (∀k, a ≤ k a : τ)∧ (∀k, a ≤ k a : τ). If a ∼ = a : τ, it is obvious that a evaluates to a value if and only if a does. Since the terms a and a are well-typed in a sound type system, divergence is equivalent to not evaluating to a value: by soundness of the type system, a well-typed term cannot go wrong. Therefore, a ∼ = a : τ also implies that a diverges if and only if a diverges.

This line of reasoning does not immediately apply to our weakly-typed setting, since the type soundness theorem does not hold: a term that does not evaluate could go wrong instead of diverging. Ahmed (personal communication, january 2009) suggested to strengthen the step-indexed relation between computations (rule R4) as follows:

∀ j, v, j ≤ k ∧ (e a j ⇒ v) =⇒ ∃w, ( f b ⇒ w) ∧ v k-j ≈ w : τ ∀ j, w, j ≤ k ∧ ( f b j ⇒ w) =⇒ ∃v, (e a ⇒ v) ∧ v k-j ≈ w : τ ∀ j, j ≤ k ∧ ( f b j ⇒ err) =⇒ (e a ⇒ err) (R4 ) a / e k ≈ b / f : τ
In this definition, e a j ⇒ err means that the computation a / e goes wrong in j steps, and e a ⇒ err means that it goes wrong in any number of steps. With this definition, if ∀k, a / e k ≈ b / f : τ, we know that if the computation a / e terminates on a value v, then b / f terminates on a related value, as before. Moreover, since "terminating on a value", "going wrong" and "diverging" are mutually exclusive behaviors, it is easy to show that if a / e diverges, so does b / f . We have not worked out this approach in full details, but believe that it provides an appropriate way to show that program transformations preserve divergence.

Higher-order uncurrying and divergence

The second difficulty encountered when trying to prove that higher-order uncurrying preserves non-terminating behaviors is that the expected result is false: there exists diverging terms a such that some of their legal uncurryings b terminate. Let ω be a diverging term and consider the following source term a:

let f = (λ x. let z = ω in λ y. x + y) in f 1
This term diverges when evaluated, since the partial application f 1 causes ω to be evaluated. First-order uncurrying (rule TABS alone) cannot uncurry the function bound to f , because it is not of the shape λ x.λ y . . .. However, higher-order uncurrying (rule TCOERCE) enables us to produce the following uncurried target term b:

let f = curry 2 (uncurry 2 (λ x. let z = ω in λ y. x + y)) in f 1
Since the composition curry 2 • uncurry 2 is equivalent to two steps of η-expansion, f is bound to a closure of the form (λ x.λ y . . .) [e]. The partial application f 1 therefore does not trigger the evaluation of ω and terminates instead.

An optimization that can turn diverging program into terminating ones is not necessarily bad. However, an optimization that performs uncontrolled η-expansions is generally undesirable: besides non-termination behavior, η-expansion can change time and space complexity, as well as observable effects in functional languages such as ML. To avoid this, we need to restrict uses of the uncurry n combinators in coercions. (The curry n combinators alone cannot create η-expansion problems.) One possibility is to enrich representation types τ with trivial function types (τ 1 , . . . , τ n ) / 0 → τ. These trivial function types are assigned to functions λ x.a that perform no significant computations before returning their results, typically because the body a is a syntactic value such as a λ -abstraction. For instance, λ x.λ y. x + y could be assigned type / 0 → → because no significant computations are performed between the passing of the two arguments. However, this type cannot be assigned to λ x. let z = ω in λ y. x + y, only the less precise type → → . Trivial function types are of course subtypes of general function types:

τ 1 / 0 → τ 2 <: τ 1 → τ 2
We can use trivial function types to control the coercion rules that introduce uncurry and curry combinators:

b : τ 1 / 0 → • • • / 0 → τ n → τ =⇒ uncurry n (b) : (τ 1 , . . . , τ n ) → τ (n > 0) b : (τ 1 , . . . , τ n ) → τ =⇒ curry n (b) : τ 1 / 0 → • • • / 0 → τ n → τ (n > 0)
We conjecture that this refinement suffices to ensure that higher-order uncurrying preserves non-termination, as well as observable effects in the case of ML-like languages.

Related work

In section 1, we already discussed the first-order uncurrying optimization that is commonly implemented in compilers for functional languages, as well as Hannan and Hick's type system for higher-order uncurrying [START_REF] Hannan | Higher-order uncurrying[END_REF]. We now discuss other related work. Automatic insertion of coercions to mediate between different data representations is an old idea that has been applied successfully in many areas of programming language research. Examples include the combinations of dynamic and static typing of Thatte [START_REF] Thatte | Quasi-static typing[END_REF], Henglein [START_REF] Henglein | Dynamic typing: syntax and proof theory[END_REF], Flanagan [START_REF] Flanagan | Hybrid type checking[END_REF] and Siek and Taha [START_REF] Siek | Gradual typing for functional languages[END_REF], as well as the unboxing optimizations of Leroy [START_REF] Leroy | Unboxed objects and polymorphic typing[END_REF] and Henglein and Jørgensen [START_REF] Henglein | Formally optimal boxing[END_REF]. A feature common to all these works and the present paper is the use of higher-order coercions λ f .λ x. c ( f (c(x))) to lift pairs c, c of coercions to function types.

Of these earlier works, Henglein's coercion calculus [START_REF] Henglein | Dynamic typing: syntax and proof theory[END_REF] is particularly interesting to us, since it presents efficient algorithms based on constraint solving to infer the placement of coercions in ways that are optimal under reasonable simplifying assumptions. An effective compilation pass performing higher-order uncurrying could probably be obtained by adapting Henglein's algorithms to our algebra of coercions. However, Henglein's base coercions convert between atomic type expressions, while our base coercions (the curry n and uncurry n combinators) operate over non-atomic function types. It remains to see what impact this difference has on Henglein's results.

Uncurrying of functions, including across higher-order functions, could also be decided based on the results of Shivers' control-flow analysis [START_REF] Shivers | Control-flow analysis in Scheme[END_REF] or its type-based reformulation by Wells et al. [START_REF] Wells | A calculus for polymorphic and polyvariant flow types[END_REF]. Conservatively, one could uncurry a function definition only if all the call sites to which it flows are curried and match the arity of the function; in this case, no coercions need to be inserted. More aggressively, allowing the insertion of coercions to resolve arity mismatches requires heuristics for placing the coercions that, we believe, are best handled by Henglein's constraint-based algorithms.

Conclusions and future work

The framework developed in this article and its generic proof of correctness provides a strong basis to experiment with various higher-order uncurrying strategies without having to prove their correctness every time. Since our framework relies on a "soft" type system, it can be applied to a wide range of source languages, either statically or dynamically typed. Stepindexed logical relations-the key ingredient of our semantic preservation proof-turned out, once more, to be a powerful reasoning technique, providing the general flavor of proofs by denotational semantics while remaining easy to mechanize.

As mentioned in section 1, currying is only one of the two well-known presentations of n-ary functions in the λ -calculus and related programming languages: the other is "tupling", that is, the grouping of n arguments in a single n-tuple argument. Standard ML compilers as well as the OCaml compiler routinely perform first-order elimination of "tupled" functions, turning them into n-ary functions within their syntactic scope. This optimization is known under the name arity raising. Hannan and Hicks [START_REF] Hannan | Higher-order arity raising[END_REF] extend this optimization to the higherorder case. We conjecture that our framework for higher-order uncurrying could easily be extended to deal with tupled functions as well. Representation types τ would be extended with a n-tuple type τ 1 × • • • × τ n , with × • • • × being a subtype of , and tuplify n and untuplify n combinators would be used to mediate between the representation types (τ 1 , . . . , τ n ) → τ and τ 1 × • • • × τ n → τ.

The first-order uncurrying optimizations implemented in the Glasgow Haskell and OCaml native-code compilers exploit low-level closure representation tricks to accelerate curried applications of unknown functions [START_REF] Marlow | Making a fast curry: push/enter vs. eval/apply for higher-order languages[END_REF]. The closure of a curried function λ y 1 . . . λ y n . a contains two entry points: one to the uncurried function f = λ (y 1 , . . . , y n ). a that expects all n arguments at once, another to a piece of generic code corresponding to curry n ( f ) and expecting one argument at a time. Moreover, the arity n of the function is also recorded in the closure. This enables the definition of generic combinators for curried applications to n arguments, of the following shape: Then, a source-level curried application f a 1 . . . a n , where f is an unknown function, is compiled to multapp n ( f , a 1 , . . . , a n ). The run-time arity test performed by the multapp combinators avoids the cost of a fully curried application in the frequent case where arities match. It would be interesting to express this idiom and prove its correctness within our framework.

More generally, uncurrying is a paradigmatic instance of the very general theory of type isomorphisms [START_REF] Di Cosmo | Isomorphisms of types: from lambda calculus to information retrieval and language design[END_REF]. Semantically, type isomorphisms have been studied using syntactic equational theories and denotational semantics. Neither of these frameworks extend easily to imperative features such as general references, in contrast with step-indexed relations [START_REF] Ahmed | Semantics of types for mutable state[END_REF].

Step-indexed relations could, therefore, provide a new angle to reason about type isomorphisms and extend them to functional languages with effects.

  Constants: c ::= 0 | 1 | . . . Terms: a ::= x n variable (as its de Bruijn index n) | c constant | λ .a (unary) function abstraction | a a (unary) function application | let a in a local binding | letrec λ .a in a recursive binding of a function

  Terms: b ::= x n variable (as its de Bruijn index n) | c constant | λ n .b n-ary function abstraction | b(b 1 , . . . , b n ) n-ary function application | let b in b local binding | letrec λ n .b in b recursive binding of a n-ary function The term λ n .b denotes a function of n arguments, which are bound in b to x n-1 , . . . , x 1 , x 0 (in this order). In named syntax, such functions are written λ (y 1 , . . . , y n ). b. The target language naturally supports functions with no arguments (also known as thunks), but the uncurrying transformation will not generate them. The term b(b 1 , . . . , b n ) applies the function b to the n arguments b 1 , . . . , b n . Partial applications and over-applications are not supported: reduction takes place only if b evaluates to a function of exactly n arguments; evaluation is stuck otherwise. For a recursive function binding letrec λ n .b in b , variables x n-1 , . . . , x 1 , x 0 are bound in b to the function arguments, and x n is bound to the recursive function itself.

  y n : τ n → b : τ (In this diagram, ⇑ and ⇓ stand for coercions, and → denotes functions.) The term generated as the result of the coercion, let f = b in λ (y 1 , . . . , y n ). b , first binds b to a variable to avoid recomputing it, then returns the n-ary function appropriate for the destination type.

4 Semantic preservation 4 . 1

 41 Dynamic semanticsWe first give operational semantics to the source and target languages. To simplify the Coq mechanization, we use environments and function closures instead of substitutions at βreduction time. The values resulting from computations are therefore either constants c or closures (λ .a)[e] or (λ n .b)[ f ], that is, pairs of a λ -abstraction (unary in the source language, n-ary in the target language) and an evaluation environment e or f . Owing to the use of de Bruijn notation, evaluation environments are simply list of values accessed by position. Source language Target language Values: v ::= c | (λ .a)[e] w ::= c | (λ n .b)[ f ] Evaluation environments: e ::= v 0 . . . v n f ::= w 0 . . . w n

≈

  w : τ the values v and w are related at representation type τ for up to k computation steps -a / e k ≈ b / f : τ the source term a in environment e is related to the target term b in environment f , at type τ, for up to k computation steps.

  R5) a / e k ≈ w : τ The notion of k-relatedness between two values is specified by the first three rules (R1), (R2) and (R3). By rule (R1), a constant is related to itself at type . Rule (R2) relates a source closure (λ .a)[e] with a unary target closure (λ 1 .b)[e]. These closures are k-related if and only if for all j < k and j-related argument values v, w, the computations corresponding to the applications of the closures, namely a in environment v.e and b in environment w. f , are j-related. The notion of j-relatedness between two computations is defined by rule (R4) and explained below. Concerning types, rule (R2) offers two possibilities: either the closures are related at a unary function type τ 1 → τ 2 , in which case the argument values are related at type τ 1 and the result values at type τ 2 ; or the closures, the arguments and the results are all related at type . These two choices correspond closely to the transformation rules TAPPand TAPP-N (with n = 1) in section 2.3. Rule (R3) relates a source closure (λ .a)[e] with a nary target closure (λ n .b)[ f ] at an uncurried function type (τ 1 , . . . , τ n ) → τ, where n ≥ 2.

Lemma 2

 2 There exist unique smallest predicates v k ≈ w : τ and a / e k ≈ b / f : τ and a / e k ≈ w : τ that satisfy rules (R1) to (R5).

2 .

 2 λ .a / e k ≈ λ n .b / f : τ ⇐⇒ (λ .a)[e] k ≈ (λ n .b)[ f ] : τ 3. If e(n) = v and f (m) = w, then x n / e k ≈ x m / f : τ ⇐⇒ v k ≈ w : τ. Proof Note that the source terms c, λ .a and x n evaluate in exactly zero steps to c, (λ .a)[e] and v, respectively. The result then follows from (R4) and (R1).

Lemma 5

 5 If a / e k ≈ b / f : and a / e k ≈ b / f : , then a a / e k ≈ b(b ) / f : . Proof Consider an evaluation e a a j ⇒ v in j ≤ k steps. By inversion, we have e a p ⇒ (λ .a 1 )[e1] and e a q ⇒ v and v .e 1 a 1 r

Lemma 6

 6 ≈ w : Therefore, f b(b ) ⇒ w and the expected result follows. Zaynah Dargaye, Xavier Leroy If n > 0 and a / e k ≈ b / f : (τ 1 , . . . , τ n ) → τ and a i / e k ≈ b i / f : τ i for i = 1, . . . , n, then a a 1 . . . a n / e k ≈ b(b 1 , . . . , b n ) / f : τ.

Lemma 8

 8 If τ <: τ , then a / e k ≈ b / f : τ implies a / e k ≈ b / f : τ . Proof By (R4), it suffices to show that v k ≈ w : τ implies v k ≈ w : τ for all values v, w.

4. 4 1 .

 41 Correctness of the translationWe are now ready to prove the main correctness theorem: if the target term b is an uncurrying of the source term a at type τ in compilation environment Γ , then for any number of steps k, the computation a in e is k-related at τ to the computation b in f , provided the execution environments e and f are k-related at the compilation environment Γ . Relatedness between environments, written e k ≈ f : Γ , is defined straightforwardly as -e, Γ and f have the same length n;-e(i) k ≈ f (i) : Γ (i) for all i = 0, . . . , n -Theorem 12 If Γ a =⇒ b : τ and e k ≈ f : Γ , then a / e k ≈ b / f : τ.Most of the lemmas needed for the proof of theorem 12 have already been proved. To handle the case of function abstractions, we need the three additional lemmas below. (We write λ -n-. . . λ for n successive function abstractions in the source language.)Lemma 13 Assume ∀k, e, f , e k ≈ f : τ n . . . τ 1 .Γ =⇒ a / e k ≈ b / f : τ. If n > 0 and e k ≈ f : Γ , then (λ -n-. . . λ .a)[e] k ≈ (λ n .b)[ f ] : (τ 1 , . . . , τ n ) → τ. Proof If n = 1, the result follows from rule (R2). If n > 1, we first show that λ -n-. . . λ .a / e k ≈ (λ n .b)[ f ] : (τ 1 , . . . , τ n ) → τby induction over n, then conclude using rule (R3). Lemma 14 Assume ∀k, e, f , e k ≈ f : τ n . . . τ 1 .τ f .Γ =⇒ a / e k ≈ b / f : τ, where τ f is the type (τ 1 , . . . , τ n ) → τ. Let v = (λ -n-. . . λ .a)[v.e] and w = (λ n .b)[w. f ] be recursive closures of a and b. If n > 0 and e k ≈ f : Γ , then v k ≈ w : τ f .

Corollary 15

 15 Let a be a closed term. If ε a =⇒ b : τ and a evaluates a constant (ε a n ⇒ c for some n), then b evaluates to the same constant (ε b ⇒ c). Proof By theorem 12, a / ε n ≈ b / ε : τ. Therefore, there exists a value w such that ε b ⇒ w and c 0 ≈ w : τ. The latter implies w = c by definition of relatedness.

  Arity information: ρ ::= K(n) function of known arity n | U constant or function of unknown arity Arity environments: Θ ::= ρ 0 . . . ρ n

Corollary 17

 17 Let a be a closed term. If T (ε, a) = b and a evaluates to a constant (ε a n ⇒ c for some n), then b evaluates to the same constant (ε b ⇒ c).

  b type-checks the application of b : τ to the arguments b i : τ i and returns the uncurried application b and its type τ .

For part 3 ,

 3 all cases are straightforward except the case of applications. We show thatA (τ, b, (τ 1 , b 1 ) . . . (τ n , b n )) = τ , b and Γ a =⇒ b : τ and Γ a i =⇒ b i : τ i for all i imply Γ a a 1 • • • a n =⇒ b : τ ,by induction over n, and conclude. Corollary 21 Let A be a closed, annotated term. If V (ε, A) = τ, b and the erasure A↓ evaluates to a constant (ε A↓ n ⇒ c for some n), then b evaluates to the same constant (ε b ⇒ c). Proof By part 3 of lemma 20 and corollary 15.

Theorem 22

 22 The validating translation is complete: 1. If τ <: τ , then S (τ, τ ) = true. 2. If b : τ =⇒ b : τ , then for all terms b , C (b , τ, τ ) = / 0. 3. If Γ a =⇒ b : τ, there exists an annotated term A and a target term b such that A↓ = a and V (Γ , A) = τ, b .

Fig. 5

 5 Fig.5Characterization of the pairs of types τ =⇒ τ such that algorithm C succeeds in producing a coercion from τ to τ . Each inference rule is annotated by the number of the corresponding case of C in figure3.

6. 1

 1 Step-indexed logical relations and divergence As defined in sections 3 and 4.2 and in the original work of Appel and McAllester [7], the relation a / e k ≈ b / f : τ only states that if a / e terminates in some number j ≤ k of steps, then b / f terminates in any number of steps. If the computation a / e diverges, the relation holds vacuously and provides no guarantees on the behavior of the computation b / f . To prove semantic preservation for non-terminating source programs, we would need to strengthen the definition of step-indexed logical relations so that if a / e k ≈ b / f : τ holds for all k and a / e diverges, then b / f diverges as well.

  multapp n (clos, y 1 , ..., y n ) = if clos.arity = n then clos.n-ary-entry-point(clos, y 1 , ..., y n ) else let clos 1 = clos.unary-entry-point(clos, y 1 ) in let clos 2 = clos 1 .unary-entry-point(clos 1 , y 2 ) in ... clos n-1 .unary-entry-point(clos n-1 , y n )

In honor of the logician Haskell B. Curry. Curry himself attributes this technique to Schönfinkel[START_REF] Curry | Combinatory Logic[END_REF], but it was used earlier by Frege according to Cardone and Hindley[START_REF] Cardone | History of lambda-calculus and combinatory logic[END_REF].

Here and throughout this paper, λ (x, y) . . . denotes a two-argument function of the target language, not a function that takes a pair as single argument. Likewise, f (x, y) is an application to two arguments, as in C or Java, not an application to the pair (x, y) as in ML or Haskell.

List.map and List.map2 are the familiar higher-order functions that iterate a function over the elements of one or two lists, respectively.

One application initially envisioned for this work is as part of a larger effort to develop and prove correct a compiler for pure, formally verified functional programs directly written in the specification language of Coq.

Acknowledgements This work was supported in part by Agence Nationale de la Recherche, grant number ANR-05-SSIA-0019. We thank the three anonymous reviewers for their helpful suggestion for improving the presentation of this paper.