Matthias Puech
email: matthias.puech@inria.fr

Typeful Continuations

Introduction

How should we design compilers so as to formally guarantee that the output code will behave the same way as the input one should? This vast research project, started some 30 years ago, comes today to fruition in particular for low-level languages like C [START_REF] Leroy | Formal certification of a compiler back-end or: programming a compiler with a proof assistant[END_REF]. An ongoing effort aims at extending it to higher-level ones, in particular functional languages, with the λ-calculus at their core [START_REF] Dargaye | Vérification formelle d'un compilateur optimisant pour langages fonctionnels[END_REF].

Continuation-passing style Among the compilation schemes for functional languages, Continuation-Passing Style, or CPS, is a popular choice [START_REF] Appel | Compiling with Continuations[END_REF]. CPS is a classic and powerful tool that has seen several decades of study and applications, in very diverse fields: functional programming, semantics, compiler design, proof theory. . . It notably transforms a functional program, potentially triggering non-local jumps (e.g., using Lisp's call/cc or delimited control operators), into a pure, higher-order program which makes the evaluation strategy explicit by sequentializing its computations.

Several features leave an important gap between the theoretical transform originally posited by Plotkin [START_REF] Plotkin | Call-by-name, call-by-value and the lambda-calculus[END_REF] and the actual implementations in compilers:

• first, the original transform generated far more redexes than initially present in the source term, the so-called "administrative redexes", as an artifact of the transformation itself. This well-studied problem led to the discovery of the one-pass CPS transforms [START_REF] Danvy | Representing control: A study of the CPS transformation[END_REF].

• even without administrative redexes, the output is still not optimized; in particular, it translated beta-redexes in a verbose way: transforming the nested beta-redex (λx 1 x 2 x 3 . M ) N 1 N 2 N 3 leads to unnecessary threading of continuations [START_REF] Danvy | CPS transformation of beta-redexes[END_REF], which requires six reduction steps instead of three.

Typeful programming We call typeful the style of light formalization of type preservation of program translations we adopt here; this research program was already initiated in the study of Normalization by Evaluation [START_REF] Danvy | Typeful normalization by evaluation[END_REF]. We first assign simple types to our source language. We then identify the tightest syntax to fit the target of the translation, so as to guarantee that the output conforms to the specification. We then code the translation itself, which gives us a type assignment for the target language. Contrarily to the standard practice of using a full-blown proof assistant, e.g., Coq or Agda, and formalize operational semantics preservation, we carry it out in the minimal setting of a generalpurpose programming language -here OCaml -with Generalized Abstract Data Types (GADTs for short) [START_REF] Garrigue | Ambivalent types for principal type inference with gadts[END_REF], which are a generalization of ML algebraic data types that allows a fine control on the return type of their constructors [20]. We use them to intrinsically represent simply typed terms of the various calculi, and to relate them through translation functions. They are sufficiently expressive to prove type preservation, and yet lightweight enough to be almost transparent to the programmer, as they enable a gradual approach to formalization: one can start by specifying syntax trees (abstract types) and transformations (functions), and later decorate them with object types, leaving the code unchanged. Beyond showcasing the expressive power of GADTs, we argue that this choice also shows that the gap between functional languages and proof assistants is shrinking.

Yet of course, OCaml does not provide the same safety guarantees as proof assistants; for instance, potential use of side-effects could compromise the safety of the results; we will have to be careful using them in a controlled fashion. Besides, in order to avoid the pitfall of variable binding, we use weak Higher-Order Abstract Syntax (wHOAS) to represent binders [START_REF] Chlipala | Parametric higher-order abstract syntax for mechanized semantics[END_REF]. These choices, which are theoretically unsafe in our case (see discussion Section 2), would not be possible in a proof assistant based on type theory, but they lighten the development greatly.

Outline The remainder of this article is an incremental, literate programming exposition of our implementation, in OCaml, of a typeful, one-pass, beta-normal, properly tail-recursive CPS transform.. 1 After briefly recalling GADTs in OCaml and Plotkin's call-by-value CPS transform (Section 2), we begin its gradual optimization. Starting from Danvy & Fillinski's one-pass CPS transform, we first exhibit its precise target syntax and typing (Section 3). The resulting system has no administrative redexes, and we show how to evaluate it. We then exhibit the inefficiency of translating multiple nested beta-redexes, show how to constrain the syntax to forbid this inefficiency, and modify the translation accordingly (Section 4). Finally, we show that the translation of tail calls gives rise to η-redexes which could be avoided (Section 5); again, we show how to constrain the syntax to forbid them, and modify the translation accordingly.

Background

The simply-typed λ-calculus with GADTs and HOAS

The starting point of our development is the simply-typed λ-calculus, equipped with a let construct for convenience.

M ::= λx. M | M M | x | let x = M in M Expressions
We leave out its typing rules, which are absolutely standard and can be found in any respectable textbook [START_REF] Girard | Proofs and Types[END_REF]. How should we encode this language in OCaml so that only well-typed terms, and function manipulating well-typed terms, are accepted? First of all, we will use a deep embedding of the language: each expression of our object language (the λ-calculus) will be represented by a value-more precisely an abstract data type-in the metalanguage (OCaml); this is essential because we need structural recursion on its structure. Secondly, we will use Higher-Order Abstract Syntax (HOAS) to encode variable binding. When it comes to representing abstract syntax which contains binders and variables, one must ensure that only wellbound terms will be representable, and the others rejected; many techniques are in use, including the well-known De Bruijn indices. HOAS is the most concise we know and the closest to pen-andpaper practices; it boils down to using the meta-language binding capabilities to represent the objectlanguage binders; in our case, it means using OCaml functions "fun x →" to introduce a variable named x in an encoded expression, and use "x" to refer to it in the body of the binder. Because of this confusion between function space and binding space, HOAS problematically lets us represent values which are not terms of our object language: the so-called "exotic terms" [START_REF] Washburn | Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism[END_REF]. Weak, or parametric HOAS [START_REF] Chlipala | Parametric higher-order abstract syntax for mechanized semantics[END_REF] rule out these exotic terms by leaving the type of the variables abstract; this is what we will use here.

Thirdly, we will use Generalized Abstract Data Types to encode the object type system (simple types). The recent introduction of GADTs into OCaml [START_REF] Garrigue | Ambivalent types for principal type inference with gadts[END_REF] makes it possible to declare abstract data types which are indexed by types: each constructor can fix the type parameters of its type.

All in all, the following snippet introduces the OCaml type of simply-typed λ-terms:

type α m = | MLam : (α x → β m) → (α → β) m | MApp : (α → β) m * α m → β m | MVar : α x → α m | MLet : α m * (α x → γ m) → γ m
The benefit of using GADTs is that object typing appear as simple type annotations on top the usual untyped abstract data type; whereas other techniques would draw the encoding further away from it [START_REF] Carette | Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages[END_REF]. As promised, the type of variables α x is separated from the type of terms α m. Think of this type of variables as abstract for the moment; it will be defined in Section 3.3 when discussing evaluation. For instance, the applicator term λf x. f x is encoded as the following OCaml value:

let ex : α β. ((α → β) → α → β) m = MLam (fun f → MLam (fun x → MApp (MVar f, MVar x)))
Note that only well-typed λ-terms are well-typed OCaml value of type α m. This is characteristic of intrinsically-typed representations.

x K = K[x] (4) λx. M K = K[λxk. M [λM. [k M ]]] (5)
M N K = M [λM. N (λN. M N (λv. K[v]))] (6)
let x = M in N K = M [λM. let x = M in N [λN. K[N ]]] (7)
M = λk. M [λM. k M ] (8)
Figure 1: One-pass CPS-transformation

Call-by-value CPS

In its seminal 1975 article [START_REF] Plotkin | Call-by-name, call-by-value and the lambda-calculus[END_REF], Plotkin proposed a pair of source-to-source program transformations on the λ-calculus that has two important and since then famous properties: simulation, i.e. transformed terms reduce to similar values as source terms, and indifference, i.e. the transformed terms reduce the same way in all reduction strategy. One transformation simulated the call-by-name strategy, the other the call-by-value strategy. In other words, the evaluation strategy, implicit in the source language, can be made explicit by CPS-translating its programs; it turns out that many control operators and nonlocal stack manipulations can also be simulated by CPS [START_REF] Danvy | Representing control: A study of the CPS transformation[END_REF]. This is why CPS is a form of compilation: it turns implicit notions, control and evaluation order, into an explicit one, continuation.

Here is the call-by-value transformation:

x = λk. k x (1)
λx. M = λk. k (λx. M ) (2)
M N = λk. M (λm. N (λn. m n k))

Each subterm is transformed into a functional (λk. . . . ) that awaits a continuation k, i.e., a function to which the result of the computation will be passed. A variable x becomes a term that passes x to its continuation; an abstraction becomes a term that passes to its continuation the abstraction body; an application becomes a term that passes sequentially to its subterms continuations (λm. . . . ) and (λn. . . . ), eventually forming an application m n k with the results. It should be therefore clear that the transformation has an effect on the types of the transformed term. for instance, if M : p ⊃ q, then M : ((p ⊃ (q ⊃ o) ⊃ o) ⊃ o) ⊃ o for any given answer type o. For this reason, directly transliterating the function • above as an OCaml function of the GADT α m would lead to an ill-typed program: inferring the type transformation is beyond the scope of GADTs.

One-pass CPS-transformation

Plotkin's original transformation had one major drawback: it generated far more redexes than present in the source term; reducing the additional "administrative" redexes on-the-fly became an interesting challenge, solved independently by Appel, Danvy & Filinski and Wand [START_REF] Appel | Compiling with Continuations[END_REF][START_REF] Danvy | Representing control: A study of the CPS transformation[END_REF]18]. By a control flow analysis of the original translation, one can classify lambdas and applications as either static, i.e., invariably forming redexes and therefore reducible at translation-time, or dynamic, i.e., to leave in the output term to be eventually reduced at run-time [START_REF] Danvy | Representing control: A study of the CPS transformation[END_REF]. The one-pass CPS transform then uses the meta-language's function space to represent static redexes, leading to a higher-order transformation. In this section, we use the higher-order nature of the one-pass CPS to derive the syntax and typing of the target language of CPS.

Notations Throughout this paper, we are going to define translations and evaluations of variants of the λ-calculus using a higher-order meta-language, itself akin to a λ-calculus. To distinguish this meta-language from the object languages, we will write respectively λX. E, E 1 [E 2 ] and X for the abstraction, application and variables in the meta-language. Meta-abstraction introduces the function space A → B; in contrast, the arrow type of the object language will be noted A ⊃ B.

Syntax

The original, one-pass call-by-value CPS-transform, reproduced on Figure 1, is presented as a sourceto-source program transformation, mapping λ-terms to λ-terms [START_REF] Danvy | Representing control: A study of the CPS transformation[END_REF]. It therefore consists of two functions: a top-level transformation • : M → M , and a recursive function with an additional functional argument

• • : M → (M → M ) → M .
If we look at the effect of the transformation on typing, it maps terms M of type A into terms M of type A , as discussed above. In other words, going through this CPS transform, the syntax is fixed (output syntax = input syntax), but the types vary. There is another way to look at it, where we fix types and let the syntax vary (output syntax = input syntax). Let us look at Figure 1 forgetting that the output language is the λ-calculus, and let us find the "tightest" grammar that will satisfy this transformation. Or, in other words, some constructs of the one-pass CPS transform always appear together in output terms, and we can aggregate them into compound syntactic nodes, leading to a specialized syntax of CPS terms. We now detail this analysis.

Let T (respectively S) be the smallest set of terms that are applied to (respectively are the result of applying) a context K. In Equation 4, we return the result of applying the context, so the codomain of function • • is an element of S. According to Equations 4, 5 and 6, terms in T include variables x and v, and double abstractions, which bodies are the result of the transformation, i.e., a term in S. According to Equations 5, 6 and 7, terms in S include the application of a continuation k to a term in T , a compound of two applications and an abstraction with subterms belonging respectively to T , T and S, and a let-binding, with subterms belonging respectively to T and S. Finally, let P be the codomain of function • . According to Equation 8, it contains an abstraction with subterm in S. Note that we distinguished three kind of variables: source variables x, common to the source language, continuation variables k and value variables v which are generated by the transform. All in all, the specialized target syntax of the one-pass CPS is:

S ::= k T | T T (λv. S) | let x = T in S
Serious terms

T ::= λxk. S | x | v
Trival terms

P ::= λk. S Programs
Terms in S, or serious terms after Reynolds, represent computations; terms in T , or trivial terms, represent values. A program P abstracts a serious term over an initial continuation k. The first two constructs of serious terms can be seen respectively as bind (T U (λv. S) and return (k T ) in the continuation monad. Note however the difference between a bind, which binds a value variable v to the value of the application in the source expression, and a let, which binds a source variable x to any trivial term, and stems from a let in the source expression. Interestingly, value variables have been shown to occur linearly and non-commutatively, as a stack, and there needs to be only one continuation variable in scope at any point of a CPS term [START_REF] Danvy | The occurrence of continuation parameters in CPS terms[END_REF].

All in all, the specialized one-pass CPS-transform is defined by the equations of Figure 1, but with the types:

• • : M → (T → S) → S • : M → P

Typeful transformation

We chose a type system for the source language-simple types-and we now have a target syntax and a specialized transform that maps to it. Can we assign types to the target syntax so that the transform preserves types? In other words, how should we annotate the syntax above with GADTs so that the following code, a transliteration of the functions on Figure 1, is accepted by OCaml?

let rec cps : type a. a m → (a t → s) → s = function | MVar x → fun c → c (TVar x) | MLam m → fun c → c (TLam (fun x k → cps (m x) (fun v → SRet (k, v)))) | MApp (m, n) → fun c → cps m (fun t → cps n (fun u → SBind (t, u, fun v → c (TVal v)))) | MLet (m, f) → fun c → cps m (fun m → SLet (m, fun x → cps (f x) (fun n → c n))) let cps : α. α m → α p = fun m → PInit (fun k → cps m (fun v → SRet (k, v)))
Look at the top-level function: the types assigned to CPS programs are the same as their direct-style image: an α m is mapped to an α p. It turns out that there is only one possible type assignment satisfying this constraint, the following GADT:

type s = ( * Serious terms * ) | SRet : α k * α t → s | SBind : (α → β) t * α t * (β v → s) → s | SLet : α t * (α x → s) → s and α t = ( * Trivial terms * ) | TLam : (α x → β k → s) → (α → β) t | TVar : α x → α t | TVal : α v → α t type α p = ( * Programs * ) | PInit : (α k → s) → α p
Again, think of the type of value variables α v and continuation variables α k as abstract; they will be defined in the next section. Serious terms do not carry a type like trivial terms α t and programs α p do; instead, their constructors act as existential types, matching up trivial terms, continuations and values by their types. Here is, for instance, the translation of the applicator expression λf x. f x, in CPS syntax:

let ex : α β. ((α → β) → α → β) p = PInit (fun k → SRet (k, TLam (fun f k → SRet (k, TLam (fun x k → SBind (TVar f, TVar x, fun v → SRet (k, TVal v)))))))
Let us now transliterate the transformation itself directly from Figure 1: As witnessed by its type annotation, this main function preserves types: it maps a source expression of type α to a CPS program of the same type α.

Evaluation

To get a better understanding of the target CPS syntax, let us give its semantics. The result of evaluating a trivial term is a CPS value, i.e., an OCaml function in CPS, returning an answer of abstract type o:

type o and α vl = VFun : (α vl → (β vl → o) → o) → (α → β) vl
For instance, here is the value corresponding to the applicator expression above:

let ex : α β. ((α → β) → α → β) vl = VFun (fun (VFun f) k → k (VFun (fun x k → f x (fun v → k v))))
As usual during evaluation, variables will be substituted by what they stand for; we therefore instantiate their respective namespaces by their semantics.

2 type α x = X of α vl type α v = V of α vl type α k = K of (α vl → o)
Unsurprisingly, source and value variables stand for values, and continuation variables stand for continuations, i.e., maps from values to answers. Evaluation consists of one function from trivial terms to values (eval) and one from serious terms to answers (exec).

let rec exec : s → o = function | SLet (t, f) → exec (f (X (eval t))) | SRet (K c, t) → c (eval t) | SBind (t, u, s) → match eval t with | VFun f → f (eval u) (fun v → exec (s (V v))) and eval : type a. a t → a vl = function | TVar (X x) | TVal (V x) → x | TLam f → VFun (fun x k → exec (f (X x) (K k)))
A let triggers the execution of its body, binding its variable to the value of its definition. A return k T evaluates its term T and passes its value to the continuation that k stands for. To execute a bind T U (λv. S), one binds the application of the value of U to the value of T as a new value variable v, and continue executing S. The type of exec might come as a surprise: since answer type o is abstract, executing a serious term has no result (if not for potential side effects if we had included e.g. a printf primitive) since we did not specify an initial continuation, i.e. what to do with the result of the computation. In Kennedy's words, "the only observations we can make on [pure CPS] programs is termination" [START_REF] Kennedy | Compiling with continuations, continued[END_REF]. When evaluating a program, one way to circumvent this is to use exceptions (or assignment [START_REF] Kiselyov | Monads for undelimited continuations[END_REF]) to let the final value jump out of a "trick" initial continuation, catch it at top-level, and return it: The second line defines a local exception which will not escape the scope of the function body: if the program was indeed generated by CPS-transformation of a source expression M , its use of continuations is linear [START_REF] Danvy | The occurrence of continuation parameters in CPS terms[END_REF], which means that the initial continuation will eventually be called once, and the exception triggered. Caught by the surrounding handler, the final value will finally be returned.

CPS-transformation of β-redexes

The transformation of Section 3 translates expression ((λxy. As you can see, each original β-reduction step takes two substitutions in this CPS form: one for the value and one for the argument's continuation. Yet, continuations are only threaded here, which is characteristic of nested β-redexes. This problem has been studied under the name "compacting CPS terms" [START_REF] Sabry | Reasoning about programs in continuation-passing style[END_REF][START_REF] Danvy | CPS transformation of beta-redexes[END_REF]. Indeed, a more compact CPS-term could however be obtained if we were to see redexes as lets in the source expression. The equivalent expression (let x = a in λy. x) b is translated into:

λk. let x = a in (λy. x) b (λv. kv)
which exposes the second redex; extra mileage is therefore obtained by seeing all nested β-redexes as lets. The equivalent expression let x = a in let y = b in x is translated into:

λk. let x = a in let y = b in k x
This residual CPS term is more compact and efficient; syntactically, it has no apparent β-redexes anymore. The formalization and typing of the "compacting CPS" optimization proposed by Danvy and Nielsen [START_REF] Danvy | CPS transformation of beta-redexes[END_REF] is the object of this section.

Syntax

Now, we want to write all explicit redexes in the target language as lets. Let us alter the syntax of CPS terms of Section 3 so as to ban the construction of redexes, such as (λxk. S 1 ) T (λv. S 2 ). In other words, the functional term T 1 in a "bind" T 1 T 2 (λv. S) must only be an identifier, i.e., a source or a value variable. We thus stratify the syntax of trivial terms into identifiers I and functions, and constrain the functional subterm of a "bind" to be an identifier, which rules out the possibility to write redexes:

P ::= λk
I ::= x | v Identifiers
This stratification is akin to the traditional syntax of normal forms of the (direct-style) λ-calculus, which stratify the syntax into normal forms and atomic terms. Identifiers play the role of atomic terms, trivial terms of normal forms; the applications nodes, which in the syntax of normal forms belong to atomic terms, are here "extruded" to binds in serious terms, which value variables range over.

Typeful transformation

Encoding the typed syntax is trivial; we just adapt the previous typing rules to the new, constrained syntax:

3 type α i = IVar of α x | IVal of α v ( * Identifiers * ) type s = ( * Serious terms * ) | SBind : (α → β) i * α t * (β v → s) → s | SRet : α k * α t → s | SLet : α t * (α x → s) → s and α t = ( * Trivial terms * ) | TLam : (α x → β k → s) → (α → β) t | TIdent : α i → α t type α p = PInit of (α k → s) ( * Programs * )
Now comes the transformation itself. Danvy and Nielsen's insight was that for the transformation to be done in one pass, it needs to be context-sensitive: the result of transforming the innermost beta-redex (λxy. x) a of the introductory example should "remember" the outermost application node, which forms a nested beta-redex. Each nested beta-redex is transforms like a let, and not like a regular application. Technically, their transformation was annotated by an integer, encoding how many nested redexes are in the context at any point; the higher-order type of the translation function depended on this integer.

Despite the absence of dependent types in OCaml, we can encode, as a GADT, the relation between the type of the input context and the type of the output value:

type (α, ξ) l = | Base : (α, α t) l | Arr : (β, ξ) l → (α → β, α t → (ξ → s) → s) l
Each inhabitant of type (α, ξ) l is a proof that an expression α m will be translated into a value ξ. For instance:

let ex : α β γ. (α → β → γ, α t → ((β t → (γ t → s) → s) → s) → s) l = Arr (Arr Base)
The main translation function follows:

let rec cps : type a x. (a, x) l → a m → (x → s) → s = fun l → function | MVar x → fun c → c (psi l (IVar x)) | MApp (m, n) → fun c → cps (Arr l) m (fun m → cps Base n (fun n → m n (fun a → c a))) | MLet (m, n) → fun c → cps Base m (fun t → SLet (t, fun x → cps l (n x) (fun u → c u))) | MLam m → fun c → match l with | Base → c (TLam (fun x k → cps Base (m x) (fun m → SRet (k, m)))) | Arr l → c (fun t k → SLet (t, fun x → cps l (m x) k))
It differs from its ancestor of Section 3 in the following points. First, it awaits one more argument, which encodes the relation above between the type of the input context a and the type of the output x; the type of the function is then explicit: it maps an input term of type a to a value of type (x → s) → s. The application case MApp does not build an SBind node right away as in the previous section: instead, it uses OCaml's application to combine the results of the translations of its subterms; eventually, the SBind node are produced at the variables; the auxiliary function psi unrolls the type relation and generates the function building the binds:

let rec psi : type a x. (a, x) l → a i → x = function | Base → fun i → TIdent i | Arr l → fun i t c → SBind (i, t, fun v → c (psi l (IVal v)))
At top level, we start in the empty context, obviously:

let cps : α. α m → α p = fun m → PInit (fun k → cps Base m (fun x → SRet (k, x)))
Once again, the type annotation of this top-level function says it all: it guarantees that direct-style terms are mapped to CPS programs in our restricted syntax (with no apparent redexes), and that types are preserved.

CPS-transformation of tail calls

The transformation of Section 4 translates expression λx. f x (g x) into the CPS term:

λxk. g x (λv 1 . f x (λv 2 . v 2 v 1 (λv 3 . k v 3 )))
Each of the source application nodes are translated into binds, each carrying a continuation (λv i . . . . ). The second continuation, (λv 3 . k v 3 ) is however trivial: it immediately returns the computed value to the initial continuation, which is characteristic of tail calls. Indeed, when executing this term (Section 3.3), the last continuation will allocate one stack frame, to then immediately pass control to the initial continuation. In fact, if we read for a minute this CPS term as a traditional λ-term, this continuation is an η-redex. For efficiency and conciseness, it is necessary to avoid the detour and directly translate tail call continuations into continuation variables: λxk. g x (λv. f v k). One solution would be to detect tail calls a posteriori, after CPS translation, and mark them as such; but it would require more computation and memory, so as before we embark in solving the problem in one pass. The formalization of this optimization, inspired by Danvy and Filinski's solution [START_REF] Danvy | Representing control: A study of the CPS transformation[END_REF] but combined with the previous β-redexes optimization, is the object of this section.

Syntax

Let us alter the syntax of CPS terms of Section 4 so as to accept the contracted serious term f v k, and reject its expanded form f v (λw. k w). This is delicate because obviously, the first "bind" g x (λv. f v k) must still be legal, so we cannot ban the production T U (λv. S) altogether from our grammar. In essence, we want to ban continuations that are trivial, i.e., which amount to a return, and replace them simply by the continuation variable.

For this, we introduce the grammar entry of (non-trivial) computations U , distinguishing them from any serious term S (trivial or not). Serious terms can be actual computations U or trivial ones (k T ) but computations cannot be trivial. Now, a continuation C, i.e., the last constituent of a bind, can then either refer directly to a continuation variable (the contracted form) or bind a value variable (the expanded form). In the latter case, the continuation cannot be a return: it needs to be a computation U . All in all, the syntax of properly tail-recursive CPS terms is:

I ::= x | v Identifiers
Note that a let is a computation U , even if its body can be any term S. Note also that this stratification rules out the possibility to write I T (λv. k T ), whatever T is. Yet, as the next section will show, this set of terms is large enough to be the image of CPS.

Typeful transformation

The modified syntax is easily typed and encoded into a GADT: The new constructor is CTail k, representing a tail continuation k. transform (see [START_REF] Dargaye | Vérification formelle d'un compilateur optimisant pour langages fonctionnels[END_REF] for a survey); it relies heavily on previous study of CPS and CPS optimizations [START_REF] Danvy | Representing control: A study of the CPS transformation[END_REF][START_REF] Danvy | CPS transformation of beta-redexes[END_REF][START_REF] Appel | Compiling with Continuations[END_REF].

Beyond compiler design, we are currently looking at the logical interpretation of these optimizations through the Curry-Howard isomorphism. Our source language, the simply-typed λ-calculus, corresponds to Natural deduction; what logical system are in correspondence with the different intermediate languages we have designed here? Striking connections to the proof-theoretic notion of focusing [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF] have already been observed.

Typeful programming

We have called "typeful" our style of lightweight formalization: infer dedicated syntax and constrain it so that it acts as a specification, prove type preservation by annotating the transformations with simple types, encoded by GADTs in OCaml. Besides the obvious interest of the formal guarantee, it also gives us a methodology to discover novel properties of the transformations (like the typing rules governing the dedicated syntax in Section 3). This research program was initiated with the formalization of Normalization by Evaluation [START_REF] Danvy | Typeful normalization by evaluation[END_REF] which gave us insight on the nature of normalization in the presence of sums. An endeavor sharing the same name was carried out by Chen et. al. [4], but in a slightly different context: proving type preservation in a dependently-typed setting (DML) with De Bruijn indices, with no particular focus on the output syntax nor on optimizations.

One question arises naturally: can we extend this encoding beyond simple types, adding e.g., primitive types, polymorphism etc. It is to our best knowledge an open issue whether polymorphism à la System F [START_REF] Girard | Proofs and Types[END_REF] can be deeply embedded into OCaml's type system. Finally, we have looked at a call-by-value strategy here, other strategies like call by name or call by need will surely be of interest as well, and offer insights on their behavior.

  let eval : type a. a p → a vl = fun (PInit s) → let module M = struct exception E of a vl end in try ignore (exec (s (K (fun x → raise (M.E x))))); assert false with M.E x → x

  x) a) b, which has two nested β-redexes, into the CPS term: λk. (λxk. k (λyk. k x)) a (λv. v b (λw. k w))

  . S Programs S ::= k T | I T (λv. S) | let x = T in S Serious terms T ::= λxk. S | I Trival terms

P

  ::= λk. S Programs S ::= k T | U Serious terms U ::= I T C | let x = T in S Computations C ::= λv. U | k Continuations T ::= λxk. S | I Trival terms

  type s = SRet : α k * α t → s | SComp : u → s and u = UBind : (α → β) i * α t * β c → u | ULet : α t * (α x → s) → u and α c = CCont : (α v → u) → α c | CTail : α k → α c and α t = TIdent : α i → α t | TLam : (α x → β k → s) → (α → β) t type α p = PInit of (α k → s)

We will however allow ourselves to reorder code snippets for pedagogical purposes. All the code presented here is available from the author's webpage.

One could object that this instantiation of the domain of variables takes us away from weak HOAS, and make our framework inconsistent. Indeed, one could forge a well-typed term containing a diverging value. This instantiation is only necessary to implement evaluation. It is a commodity to avoid more verbose solutions like De Bruijn indices or parametricity in α x.

Incidentally, if you see this typed language as a proof system through the Curry-Howard isomorphism, you will notice striking similarities with the LKQ focused sequent calculus. It is more than a coincidence, and is the subject of a work in preparation.

We have already proposed such an encoding of pattern-matching at syntaxexclamation.wordpress.com/2014/04/ 12/representing-pattern-matching-with-gadts/, which could be a starting point.

Acknowledgements

This work was carried out mainly when the author was employed at Aarhus University. We would like to thank Olivier Danvy who motivated and guided it, and transmitted us his passion for the topic.

Now, the transformation relies on the observation that being in tail position in the λ-calculus is an inherited attribute: whether a function call is a tail call can be determined only by the context in which it appears, i.e., we can stratify its syntax into two syntactic categories:

Terms in any position

Terms in tail position

We choose to track this information during the CPS transformation itself, by splitting the previous CPS function into two mutually recursive ones, depending on the position of the sub-term translated.

In tail position, we will use cpst; in another position, we will use cps:

( * all this is as before (except that it returns a u * )

( * new: the lambda is part of a nested redex in tail position so we produce a let with a body in tail position * )

( * identical to the previous section , except. . . * )

First, look at the types of these functions: the translation of a term in tail position cpst can give rise to any serious term S, computation or otherwise; but the translation of a term in non-tail position will have to return a computation U . Function cps takes a "translation-time" continuation function x → u as before (and therefore also a witness l of the type relation). Function cpst does not need such arguments: a tail call cannot have a context of nested redexes above him; therefore it only takes a "run-time" continuation α k that will eventually be inserted, marking the tail call.

Notice the new case when transforming a non-tail abstraction: we can now detect "at a distance" the lambdas that will be eventually give rise to redexes in tail positions (constructor Tail ). This case is generated when transforming an application in tail position.

This new constructor is added to the GADT l that relates source and target types:

( * new: tail position indicator . This marks a term in functional position of a tail application . * )

There is now two ways to relate function types: those in tail position, which therefore do not need a functional argument, and those who are not in tail position, as before. The function psi generating the binds is modified accordingly: it generates proper tail calls CTail when indicated by the Tail relation.

( * same as before * ) let rec psi : type a x.

( * new case: where we generate a tail bind * )

Finally, the top-level function calls the translation in tail position:

Its type annotation guarantees that all source terms are translated into CPS programs, with their types preserved.

Evaluation

To showcase the gain of this optimization, let us to conclude with the evaluation function for the modified syntax:

As you can see, the new function continue has two cases: in one (non-tail calls), a closure is allocated; in the other (tail calls), the continuation c is immediately returned. Tail calls are therefore more efficient at run time.

Related and further work

Optimizing CPS translations By exploring the design space of CPS translations, we hope to have given a better understanding of Plotkin's original translation, and paved the way to implementing safe and optimizing compilers based on call-by-value CPS, using only a general-purpose programming language and no external proof tools. Of course, there is still much work to scale this study to a real-world functional programming language, notably by adding syntactic constructs (abstract data types and pattern-matching 4 , exceptions and other control operators. . . ), and optimizations (CSE or some other partial evaluation mechanism). This work is by no means the first formalization of a CPS