A Label-Selective Lambda-Calculus with Optional Arguments and its Compilation Method

Jun P. Furuse and Jacques Garrigue

Research Institute for Mathematical Sciences, Kyoto University Kitashirakawa-Oiwakecho, Sakyo-ku, Kyoto 606-01, JAPAN

E-mail: {furuse,garrigue}@kurims.kyoto-u.ac.jp

October 24, 1995

Abstract

The use of labels for argument passing has proved to be a useful extension to programming languages, particularly when we introduce optional arguments.

We propose here an adaptation of such a system, as can be found in Common LISP, to strongly-typed curried functional languages. For this we extend ML-style polymorphic typing to labeled arguments, out-of-order application, and optional arguments. We also provide a compilation method towards polymorphic lambdacalculus, which is proved syntactically sound for free reduction, and semantically correct for call-by-name semantics.

We implemented it, and showed the overhead caused by using this extension to be negligible when out-of-order parameter passing is used, and null when it is not.

Topics: language design, compilation methods, type theory.

1 Introduction

Labeled arguments are a way to both make more explicit the role of parameters in a function, and to permit out-of-order application. For instance, when we write the exponential function, let exp b n = b^{n} in a Caml-like syntax^{1}, there is no “natural” order for the arguments. We would rather write it,

let exp n base:b = b^{n}

where we attach a label base: to b. This also means that we can now write exp base:2 3 as well as exp 3 base:2 to compute 2^{3}.

1cf. [16]. let denotes non-recursive definition, fun x → e λ-abstraction, match e with p_{1} → e_{1} | … p_{n} → e_{n} for matching, etc…

Extending this, default parameters permit to write functions in a compacter and clearer way. In the above example —and in a computer science context— b will often happen to be 2. We would rather abbreviate it in such case. This can be done with the following definition.

     let exp n base:b⟨2⟩ = b^{n}

Now we can have two application patterns: expn, which computes 2^{n}, or expn base:b (or reverse order), which computes b^{n} as before.

But rather than default parameters, we chose to implement optional ones. We have a new type of matching pattern, ?l:p for optional matching, and two constructors, Some and None, respectively of arity 1 and 0. We are able to write a more optimal version of exp,

     let exp n ?base:o = match o with  Some b → b^{n}
                                  | None → shiftl(1, n)

where shiftl may be a bitwise operation. Application patterns are still expn and expn base:b, but now we signal explicitly the presence or absence of a parameter to the called function by automatically adding a constructor.

The use of labeled and default/optional arguments has become a common feature in untyped programming languages, starting with Common LISP [14], and continuing with object-oriented languages (Smalltalk [6], the Tcl interface language [11], etc…) Among typed languages, ADA [8] already has this feature, but then typing is explicit, and currying is not allowed, which makes the task easy. Another attempt at typing was proposed by Dzeng and Haynes in [4], Common LISP. However, here again, the absence of currying reduces the problem to record typing, as solved by Rémy [12] among others; the question of compilation is not studied, but might be solved by the method suggested by Ohori for records with optional arguments [10].

Our basis for this extension is the label-selective lambda-calculus [1], a conservative extension of lambda-calculus with labeled application and abstraction. A first polymorphic typing system was proposed in [5]. In both cases argument order was completely abstracted.

In this paper we propose a new typing system, where we can distinguish between different abstraction orders, and handle optional arguments as “typeful syntactic sugar” (syntactic sugar depending on the typing of expressions); and give type inference and compilation algorithms for an ML-like language with labels and optionals. The choice of classical λ-calculus as target language was done regarding both the clarity of the translation induced, the optimization techniques available to compile the resulting λ-expression, and the easy integration into existing functional programming languages.

The structure of this paper is as follows. In the next section we define a simple calculus handling labels, the weak selective λ-calculus, and a type system, along with examples of how one can use labels. Section 3 describes a more complete ML-like language, relates it explicitly to the typing system, and provides a type reconstruction algorithm, which also produces a type-annotated weak selective λ-term corresponding to its input. In section 4, this type-annotated term is compiled into classical λ-calculus. Finally section 5 explains how compilation can be made more efficient. Argument of proofs are given in appendix.

2 Programming with labels

In this section, we first present types, and a simple λ-calculus, giving semantics to labeled arguments. We then give examples of the different possible uses of labeled arguments.

2.1 Types

Types we will use throughout this paper are the same as in Damas-Milner polymorphism [2], but for the labels in function types.

τ ::= b | α | τ × … × τ | τ option | l:τ → τ | ?l:τ → τ monotypes
σ ::= τ | ∀α.σ  polytypes

option is the sum type defined as type α option = Some of α | None. Optional labels ?l: should only appear at the first level of types; arguments on optional labels may be omitted in applications.

We have a default label, 1:, which will be omitted in both types and terms.

2.2 A simple selective λ-calculus

The calculus we define here does not handle optional and default arguments. Those are only given semantics by translation into usual labeled arguments, during type reconstruction of the term (cf. Section 3, Figures 1 and 4), because their meaning is based on types^{2}.

This calculus differs from the selective λ-calculus of [5] by the absence of commutation between λ-abstractions^{3}. This is why we call it weak.

Terms only differ from classical λ-calculus by the introduction of labels in abstraction and application. As usual, they are identified modulo α-conversion.

M ::= x | c | λl:x.M | M l:M

The new formulation of β-reduction is:

((λl:M) l_{1}:N_{1} … l_{n}:N_{n} l:N) → (M[N/x] l_{1}:N_{1} … l_{n}:N_{n}) if (∀i ≤ n)l_{i} ≠ l

Theorem 1 The weak selective λ-calculus is confluent.

Example 1 A trivial reduction.

(λp:x.λq:y.(x, y)) q:a p:b → (λq:y.(b, y)) q:a → (b, a)

2.3 Labeled arguments

In the rest of this section we use Caml-like syntax for the above calculus.

Let’s first see a few functions using only labeled parameters. Continuing with our first exp example, its type is,

     let exp base:b n = b^{n}

exp = ⟨fun⟩ : base:int → int → int

2In this respect we differ from Common Lisp, where they are given reduction semantics.

3The calculus we propose here, and all the following systems, omit numeric labels. Their integration presents no difficulty, but would reduce the readability of this paper.

The above type means that you can apply exp to an integer, both on labels base: and 1:.

exp base:2 = ⟨fun⟩ : int → int exp 3 = ⟨fun⟩ : base:int → int

     exp 3 base:2 = 8 : int

Why would one want to use labels? We can see three kinds of reasons:

• to permit out-of-order partial applications

• not to have to remember parameter order

• to make programs more readable.

The first reason is clear. For a good understanding of the others we must study the role of function arguments. A first remark is that there is no “natural” argument order. For instance in Caml Light [9] the list folding function is defined as it list : (α → β → α) → α → β list → α, but most people we discussed with have regularly to verify this order by looking at the type. One way to analyze arguments is to consider that, for most functions, like in object-oriented languages, we can distinguish an argument which is the object of the function, others being simply parameters for what does this function. Since it list is a list manipulation function, considering its last argument as its object seems natural. A quick look at the library of Caml Light shows that in most cases the object appears to be the last argument of the function, enabling partial application on parameters. But this is not always the case: in the string and CamlTk modules, the object is the first argument. This last order is more natural from an object-oriented point of view, the function and its object becoming closer. For other parameters, we can see no rationale to prefer an order rather than another: this is often purely random.

What we suggest is a coherent labeling of functions. We do not need to label the object since it is unique (or at most two, for arithmetic functions for instance), but should label all parameters with their role or nature. Here are a few examples taken from the standard library. We didn’t change parameter order, only added labels.

map : fun:(α → α) → α list → α

it list : fun:(st:α → β → α) → st:α → β list → α list it : fun:(α → st:β → β) → α list → st:β → β

     output string : chan:out channel → string → unit
     blit string : string → off:int → to:string → to off:int → len:int → unit

In these examples, fun: or chan: express the nature of their parameters, st: (for state), off: (for offset) or to: express their roles.

You can almost tell what a function does from its type. If I tell you once that in blit_string a substring of length len is copied from the object string, starting at offset off, to the to string, starting at offset to off, wouldn’t it be easier to remember than without labels? This is for our second reason.

The readability argument comes from our remark on argument order. There is no “natural” order in general, but there may be a more readable one when the function is used. It seems more natural to put the object of the function in first position. This also includes layout problems, like the length of each argument.

     let rec quicksort order:cmp = fun [] → []
       | [a] → [a]
       | (a::l) → let (l1,l2) = it list l st:([],[])
                      fun:(fun x st:(l1,l2) →
                               if cmp x a then (x::l1,l2) else (l1,x::l2))
                   in (quicksort l1 order:cmp) @ (a::quicksort l2 order:cmp)
     quicksort : order:(α → α → bool) → α list → α list

With labels we can pass it list’s function as last argument, avoiding enlarging the distance between the function and its object, and without any auxiliary definition^{4}. The label fun: at the head of the line makes clear that this is a parameter.

In [3] Di Cosmo proposes to use type isomorphisms in order to retrieve functions in libraries, according to their type. Labels can add flexibility and accuracy to this method.

2.4 Optional parameters

Optional parameters are in fact only a “typeful syntactic sugar”, playing between ?l:τ → τ′ and l:τ option → τ′:

fun ?l:x → x = ⟨fun⟩ : ?l:α → α option

The example of introduction gets typed,

     let exp n ?base:o = match o with  Some b → b^{n}
                                  | None → shiftl(1, n)

exp = ⟨fun⟩ : int → ?base:int → int

The verification for presence or absence of a parameter is done at type checking of applications.

     exp 3 = 8 : int

exp base:3 = ⟨fun⟩ : int → int

     exp 3 base:3 = 27 : int
     (fun x → x) exp = ⟨fun⟩ : int → int

In the first case type should be ?base:int → int. But all ?-labels appearing at the head of a type are then discarded, and None is passed as argument for each of them. As a result, it is interpreted as exp 3 base:None, which evaluates to 8.

On the other hand, for the second case, base: is available. It is converted to exp base:(Some3), and waits for its next parameter. Since the application typing rule is designed for simultaneous application on multiple arguments, this is also true for the third case, which evaluates to 27.

In the last example, when a function with optional parameters is passed as argument to another function, all its optional parameters are discarded, independently of their order (we actually pass exp base:None). Leaving them as optionals would result in incompleteness of the type inference.

Since the essential role of labels is in providing an interface for functions, we give the type og the creation method for a message widget, taken from our modified version of the CamlTk interface for Tcl/Tk.

4The usual way to write quicksort is to use an auxiliary definition, but the proliferation of those is not always good. In particular it makes it difficult to distinguish between which definition is local and which is not.

  message create : Widget → unit →

?anchor:Anchor → ?aspect:int → ?background:Color → ?foreground:Color → ?borderwidth:Units → ?cursor:Cursor → ?font:string → ?kanjifont:string → ?highlightbackground:Color → ?highlightcolor:Color → ?highlightthickness:Units → ?justify:Justification → ?name:string → ?padx:Units → ?pady:Units → ?relief:Relief → ?takefocus:bool → ?text:string → ?textvariable:TextVariable →

       ?width:Units → Widget

In the original version [13], options are represented as a list. Out of the visual inconvenient of a syntax departing largely from Tcl’s, the problem of typing is unsolved. There is a unique sum type for all widget options, but all widgets are not able to handle the same options. As a result, when an illegal option is used a run-time error occurs. The only way to avoid these is to refer to the documentation. With optional arguments, the type of the creation function contains only the options handled by the message widget, enabling compile-time checking, and also permitting to verify accepted options by simply looking at the type^{5}.

Such optional parameters are necessary when one wants to interface a strongly typed language with any object-oriented one. But they are also a useful programming style when defining a library in the language itself, since they avoid defining many functions with various parameters. Why not define assoc : α → in:(α × β) list → ?eq:(α → α → bool) → β, allowing the user to give his own equality predicate when needed, and using the builtin one otherwise?

Default parameters They may be included as syntactic sugar:

 let exp n base:b⟨2⟩ = b^{n} ⟶ let exp n ?base:o = let b = (match o with Some b → b | None → 2) in b^{n}

As such we consider them only as a subclass of optional parameters, eventually needing an optimized compilation method.

3 ML-like interface language and type reconstruction

In this section, we introduce an ML-like interface language with typeful syntactic sugar for optionals. We give both type inference rules and a type reconstruction algorithm which also generates type-annotated terms used for compilation.

3.1 Syntax

We extend terms of the simple calculus. Application now takes several arguments.

M ::= x | c | (M, …, M)  variable, constant, product
| λl:x.M  lambda abstraction
| λ?l:x.M  optional abstraction
| (M l:M … l:M)  multi-application
| let x = M in M  let expression
| let rec {x_{i} = M_{i}}_{i=1}^{n} in M recursive let

5The unit type before optional parameters is there to permit partial application of message create on a widget, without discarding options. A complete application will be written create w name:"My name" ...  ().

Types were defined in the previous section. F T V (σ) is the set of free type variables of σ, using the standard definition. We can abbreviate function types using the following notation:

{l_{i}:τ_{i}}_{1}^{n} → τ = l_{1}:τ_{1} → … → l_{n}:τ_{n} → τ

We define similar types, which differ only by some permutation on the order of labels in a monotype, and an instantiation order on types. For both relations we consider the reflexive and transitive closure.

\frac{l_{1} ≠ l_{2}}{l_{1}:τ_{1} → l_{2}:τ_{2} → τ ≃ l_{2}:τ_{2} → l_{1}:τ_{1} → τ}  \frac{τ_{i} ≃ τ′_{i} (1 ≤ i ≤ n)}{τ_{1} × … × τ_{n} ≃ τ′_{1} × … × τ′_{n}}

\frac{τ_{i} ≃ τ′_{i} (i ∈ \{1, 2\})}{l:τ_{1} → τ_{2} ≃ l:τ′_{1} → τ′_{2}}  \frac{τ ≃ τ′}{τ option ≃ τ′ option}  ∀α.σ > σ[τ/α]  \frac{σ > σ′}{∀α.σ > ∀α.σ′}

The pattern ρ matches all types except function types. A_{l}(τ) is the type of the first argument with label l or ?l in τ, and R_{l}(τ) is τ where this argument is omitted (i.e. [?]l:A_{l}(τ) → R_{l}(τ) ≃ τ). L(τ) indicates the multi-set of the labels occurring in τ. If τ = {l_{i}:τ_{i}}_{1}^{n} → ρ , then L(τ) is the multi-set {l_{i}}_{1}^{n} (identifying ?l with l). For example, L(R_{l}(τ)) = L(τ) \ {l} (removing only one occurrence of l).

3.2 Inference rules

The inference rules for the interface language are given in Figure 1. The notation Γ ⊢ M ≃ τ means ^{∃}τ′ ≃ τ, Γ ⊢ M : τ′. Typeof contains the the constructors for the option type, and the following constant types (cf. 4.2.1 for associated δ-rules):

case : ∀α.∀β.(α option × (α → β) × β) → β π_{i}^{n} : ∀α_{1} … ∀α_{n}.(α_{1} × … × α_{n}) → α_{i} fix : ∀α.(α → α) → α → α

We explain Abstraction, Optional abs, Application, and Letrec rules. The others are straightforward.

In the two abstraction rules, the abstracted variable is restricted to have a type in coerced form, that is, without optional labels ?l. This guarantees the principality of the system. The coerce function ⌈·⌉ returns a type where every optional argument ?l:τ is replaced by an argument l:τ option.

In the Optional abs rule, if an optional abstraction gets an argument M typed τ, it passes Some M to the body, None otherwise. So the abstracted variable must have type τ option.

The Application rule takes a function and its arguments, and returns the applied term. It iteratively checks the types of the arguments and generates a resulting type. Furthermore, we erase the optional types which appear at the head of the obtained type. This does for the hidden None arguments.

The types of function domains are not checked with the types of the corresponding arguments themselves, but with their reduced types ⌊τ⌋. The reduce function ⌊τ⌋ erases all the optional arguments ?l:θ from τ. That is to avoid indeterminism of unification with optional arguments, which is discussed with the unification algorithm.

In Letrec rule, the “spine” condition is added to the usual rule. spine(M_{i}) returns a template function type which contains information about the order of lambda and optional

Variable  Γ{x : σ} ⊢ x : τ σ > τ
Abstraction \frac{Γ\{x : ⌈τ⌉\} ⊢ M : τ′}{Γ ⊢ λl:x.M : l:⌈τ⌉ → τ′}

Constant  Γ ⊢ c : τ Typeof(c) > τ
Optional abs. \frac{Γ\{x : ⌈τ⌉ option\} ⊢ M : τ′}{Γ ⊢ λ?l:x.M : ?l:⌈τ⌉ → τ′}

Product  \frac{Γ ⊢ M_{i} : τ_{i} for 1 ≤ i ≤ n}{Γ ⊢ (M_{1}, …, M_{n}) : τ_{1} × … × τ_{n}}

Application \frac{Γ ⊢ M : τ_{0} Γ ⊢ N_{i} : θ_{i}}{Γ ⊢ (M l_{1}:N_{1} … l_{m}:N_{m}) : erase(τ_{m})} for 1 ≤ i ≤ m \{ \begin{matrix}A_{l_{i}}(τ_{i−1}) ≃ ⌊θ_{i}⌋ \\ τ_{i} = R_{l_{i}}(τ_{i−1}) \end{matrix}

Let  \frac{Γ ⊢ M : θ Γ\{x : gen(Γ, θ)\} ⊢ N : τ}{Γ ⊢ let x = M in N : τ}

Letrec  \frac{spine(M_{i}) > τ_{i} Γ\{x_{i} : τ_{i}\}_{1}^{m} ⊢ M_{i} ≃ τ_{i} Γ\{x_{i} : gen(Γ, τ_{i})\}_{1}^{m} ⊢ N : τ}{let rec \{x_{i} = M_{i}\}_{i=1}^{n} in N : τ}

Figure 1: Type inference rules

gen(Γ, τ) = ∀(F V (τ) \ F V (Γ)).τ
strip(∀α.σ) = strip([α_{fresh}/α]σ)
strip(τ)  = τ
⌈l:τ_{1} → τ_{2}⌉  = l:τ_{1} → ⌈τ_{2}⌉
⌈?l:τ_{1} → τ_{2}⌉ = l:τ_{1} option → ⌈τ_{2}⌉
⌈τ_{1} × … × τ_{n}⌉ = ⌈τ_{1}⌉ × … × ⌈τ_{n}⌉
⌈τ⌉  = τ otherwise
spine(c)  = strip(Typeof(c))
spine(λl:x.M)  = l:α → spine(M)
spine(λ?l:x.M)  = ?l:α → spine(M)
spine(let x = M in N) = spine(N)

spine(let rec {x_{i} = M_{i}}_{i=1}^{n} in N) = spine(N)

spine(M)  = α otherwise

Here, all α’s are fresh.

erase(l:τ_{1} → τ_{2}) = l:τ_{1} → τ_{2}
erase(?l:τ_{1} → τ_{2}) = erase(τ_{2})
erase(τ)  = τ otherwise
⌊l:τ_{1} → τ_{2}⌋  = l:τ_{1} → ⌊τ_{2}⌋
⌊?l:τ_{1} → τ_{2}⌋ = ⌊τ_{2}⌋
⌊τ_{1} × … × τ_{n}⌋ = ⌈τ_{1}⌉ × … × ⌈τ_{n}⌉
⌊τ⌋  = τ otherwise
sort(b)  = base_{b}
sort(τ_{1} × … × τ_{n}) = prod_{n}
sort(l:τ → τ)  = fun
sort(τ option)  = option
sort(α)  is left undefined
Napp(M_{:τ_{1}})_{:τ_{2}} = (M_{:τ_{1}} l_{1}:None … l_{n}:None)_{:τ_{2}}
where {l_{1}, …, l_{n}} = L(τ_{1}) \ L(τ_{2})

Figure 2: Some auxiliary functions for type inference rules

abstractions of M_{i}. We restrict x_{i} to only have a type obtained by instantiation of that template. Without this constraint, we could infer the type f : a:α → b:β → γ, for let rec f = λb:y.λa:x.f a:x b:y in …, which is due to the inference of f a:x b:y but does not reflect the actual order of abstraction.

3.3 Labeled type unification

We give the unification algorithm for monotypes without optionals in Figure 3; we will use it for type reconstruction. The algorithm is given as rewriting rules for a system of Failure \frac{φ, τ ≃ τ′}{⊥} sort(τ) ≠ sort(τ′)

\frac{φ, \{l_{i}:τ_{i}\}_{1}^{n} → τ ≃ \{l′_{i}:τ′_{i}\}_{1}^{m} → τ}{⊥} \{l_{i}\}_{i=1}^{n} ∩ \{l′_{i}\}_{i=1}^{m} = ∅

Recurrence  \frac{φ, α ≃ τ α ∈ F V (τ)}{⊥}
Orientation  \frac{φ, τ ≃ α}{φ, α ≃ τ}

Redundancy \frac{φ, τ ≃ τ}{φ}

Elimination \frac{φ, α ≃ τ α ∈ V ar(φ) \ V ar(τ)}{([τ/α]φ), α ≃ τ}

Product  \frac{φ, τ_{1} × … × τ_{n} ≃ τ′_{1} × … × τ′_{n}}{φ, τ_{1} ≃ τ′_{1}, …, τ_{n} ≃ τ′_{n}}

Option  \frac{φ, τ_{1} option ≃ τ_{2} option}{φ, τ_{1} ≃ τ_{2}}

Decomposition \frac{φ, τ ≃ τ′}{φ, A_{l}(τ) ≃ A_{l}(τ′), R_{l}(τ) ≃ R_{l}(τ′)} l ∈ L(τ) and l ∈ L(τ′)

Completion  \frac{φ, \{l_{i}:τ_{i}\}_{1}^{n} → ρ ≃ \{l′_{i}:τ′_{i}\}_{1}^{m} → ρ′}{φ, ρ ≃ \{l′_{i}:τ′_{i}\}_{1}^{m} → α, ρ′ ≃ \{l_{i}:τ_{i}\}_{1}^{n} → α} \begin{matrix}\{l_{i}\}_{i=1}^{n} ∩ \{l′_{i}\}_{i=1}^{m} = ∅ \\ ρ ≠ ρ′ \end{matrix}

Figure 3: Equation rewriting rules for unification

equations between similar types.

We do not allow to unify types with optional domains. They would introduce indeterminism. For instance, if we try to unify ?l:int → int and α, we cannot tell whether α should be unified with int or ?l:int → int, this only depends on the programmer’s intention, and we do not know it.

A set of type equations φ is in solved form if every equation has form α = τ and the type variable α occurs nowhere else in φ. Such a solved-form defines a variable substitution that can be applied to type expressions.

Upon termination, having started from a set φ of equations, the resulting set is either ⊥, the inconsistent equation indicating that no solution exists, or sol(φ), a set of equations in solved form equivalent to φ.

Theorem 2 There is a terminating algorithm to solve the mgu of a set of type equations.

The solution obtained with this rewriting system is unique modulo type similar equivalence of right hand side types. For example, if l ≠ r, then α ≃ l:τ_{l} → r:τ_{r} → ρ, α ≃ r:τ_{r} → l:τ_{l} → ρ has two solutions, each of them consisting of one of these equations. But they are type similar. Which solution is selected for type reconstruction depends on how the unification algorithm chooses equations to solve. The term λf.(f a:1 b:2, f b:3 a:4) can be typed either (a:int → b:int → α) → α or (b:int → a:int → α) → α. Since they are type similar, they can be used in the same contexts.

3.4 Type reconstruction algorithm

We define a type reconstruction algorithm in Figure 4. All α’s are fresh. sol(φ) is the mgu of φ by the unification algorithm.

T_{P}(Γ, c)  = ⟨∅, τ, c_{:τ}⟩  where τ = strip(Typeof(c))
T_{P}(Γ, x)  = ⟨∅, τ, x_{:τ}⟩  where τ = strip(Γ(x))
T_{P}(Γ, (M_{1}, …, M_{n}))  = ⟨sol(⋃_{1}^{n} φ_{i}), τ_{1} × … × τ_{n}, (M′_{1}, …, M′_{n})_{:τ_{1}×...×τ_{n}}⟩
where  ⟨φ_{i}, τ_{i}, M′_{i}⟩ = T_{P}(Γ, M_{i})
T_{P}(Γ, λl:x.M)  = ⟨φ, l:α → τ, (λl:x.M′)_{:l:α→τ}⟩
where  ⟨φ, τ, M′⟩ = T_{P}(Γ[x : α], M)
T_{P}(Γ, λ?l:x.M)  = ⟨φ, l:?α → τ, (λl:x.M′)_{:l:?α→τ}⟩
where  ⟨φ, τ, M′⟩ = T_{P}(Γ[x : α option], M)
T_{P}(Γ, (M l_{1}:N_{1} … l_{n}:N_{n}))= ⟨ψ_{n}, τ, Napp((M′_{:{l_{i}:θ′_{i}}_{1}^{n}→τ_{n}} l_{1}:(N′′_{1})_{:θ′_{1}} … l_{n}:(N′′_{n})_{:θ′_{n}})_{:τ_{n}})_{:τ}⟩

where \{ \begin{matrix}⟨φ_{0}, τ_{0}, M′⟩ & = & T_{P}(Γ, M) \\ ψ_{i} & = & sol(⋃_{j=0}^{i} φ_{j} ∪ φ′_{j}) \\ ⟨φ_{i}, θ_{i}, N′_{i}⟩ & = & T_{P}(ψ_{i−1}(Γ), N_{i}) \\ ⟨θ′_{i}, N′′_{i}⟩ & = & \{ \begin{matrix}⟨⌊θ_{i}⌋ option, Some(Napp(N′_{i})_{:⌊θ_{i}⌋})⟩ \\ if ?l_{i} is the first occurrence of l_{i} in τ_{i} \\ ⟨⌊θ_{i}⌋, Napp(N′_{i})_{:⌊θ_{i}⌋}⟩  otherwise \end{matrix} \\ φ′_{i} & = & sol\{⌈τ_{i−1}⌉ ≃ l_{i}:θ′_{i} → α\} \\ τ_{i} & = & R_{l_{i}}(ψ_{i}(τ_{i−1})) \\ τ & = & erase(τ_{n}) \end{matrix}

T_{P}(Γ, let x = M in N) = ⟨sol(φ ∪ φ′), τ′, (let x_{:σ} = M′ in N′)_{:τ′}⟩
where \{ \begin{matrix}⟨φ, τ, M′⟩ & = & T_{P}(Γ, M) \\ σ & = & gen(φ(Γ), φ(τ)) \\ ⟨φ′, τ′, N′⟩ & = & T_{P}(φ(Γ)[x : σ], N) \end{matrix}

T_{P}(Γ, let rec {x_{i} = M_{i}}_{i=1}^{n} in N) = ⟨sol(φ ∪ φ′), τ,

(let x_{:σ} = fix(λx.[π_{i}^{n} x/x_{i}]_{i=1}^{n}((M′_{1})_{:τ_{1}}, …, (M′_{n})_{:τ_{n}})) in [π_{i}^{n} x/x_{i}]_{i=1}^{n}N′)_{:τ}⟩

where \{ \begin{matrix}τ_{i} & = & spine(M_{i}) \\ ⟨φ_{i}, τ′_{i}, M′_{i}⟩ & = & T_{P}(φ′_{k}(Γ[x_{i} : τ_{i}]_{1}^{n}), M_{i}) \\ φ′_{k} & = & sol(⋃_{i=1}^{k−1} φ_{i}) \\ σ_{i} & = & gen(φ(Γ), φ(τ_{i})) \\ ⟨φ′, τ, N′⟩ & = & T_{P}(φ(Γ)[x_{i} : σ_{i}]_{i=1}^{n}, N) \end{matrix}

Figure 4: Type reconstruction algorithm

T_{P} takes a typing environment Γ and a term M of the interface language, and returns a tuple ⟨φ, τ, M′⟩, where φ is a set of type equations in solved form (that can be used as a type substitution). τ is such that gen(φ(Γ), φ(τ)) is the principal type of M. T_{P} also returns a type-annotated term M′ for M.

When we create a new environment by adding types of subterms (in application, let, and letrec part), we apply the substitutions obtained in the type reconstruction of subterms to normalize it. It is not needed in ordinary ML style type reconstruction. But we want the most accurate information about abstraction order to be in the newly created environment.

In let rec, each declaration is inferred under an extended environment in which the declared variables are assigned type templates generated by spine. Since these variables have (optional) monotypes, the mgu is obtained by unification of their coerced forms.

A type-annotated term M′ is created by resolving all syntactic additions — optionals and letrec-expressions — from M. The well-typed term is φ(⌈M′⌉), where ⌈M′⌉ is a typeannotated term obtained by replacing each type annotation τ of M′ by ⌈τ⌉. Optional abstractions are replaced by normal lambda abstractions. In application, for each applied argument N_{i}, we use Napp(N′_{i}_{:θ_{i}})_{:⌊θ_{i}⌋}, which is N_{i} applied to None on all its optional labels. Furthermore, if the label N_{i} is applied to is optional, we apply Some to it. For erased optional labels, None is applied. Finally, recursive let-expressions are rewritten with the fix constant.

Here is the definition of type-annotated terms, based on the simple calculus of section 2.

Definition 1 (type-annotated term) The type-annotated term M_{:τ} stands for M of type τ (monotype). We introduce three new kinds of term, product, type coercion, and let definition.

M_{:τ} ::= x_{:τ} | c_{:τ} | (λl:x.M_{:τ})_{:τ} | (M_{:τ} l:M_{:τ})_{:τ} | (M_{:τ}, …, M_{:τ})_{:τ} | (M_{:τ})_{:τ} | let x_{:σ} = M_{:τ} in M_{:τ}

Well-typed terms under an environment Γ are those inferred by the following rules:

\frac{Γ(x) > τ}{Γ ⊢ x_{:τ}}  \frac{Typeof(c) > τ}{Γ ⊢ c_{:τ}}  \frac{Γ ⊢ M_{:τ_{i}}^{i} for 1 ≤ i ≤ n}{Γ ⊢ (M_{:τ_{1}}^{1}, …, M_{:τ_{n}}^{n})_{:τ_{1}×...×τ_{n}}}

\frac{Γ[x ↦ θ] ⊢ M_{:τ}}{Γ ⊢ (λl:x.M_{:τ})_{:l:θ→τ}}  \frac{Γ ⊢ M_{:l:θ→τ} Γ ⊢ N_{:θ}}{Γ ⊢ (M_{:l:θ→τ} N_{:θ})_{:τ}}

\frac{Γ ⊢ M_{:τ} τ ≃ τ′}{Γ ⊢ (M_{:τ})_{:τ′}} \frac{Γ ⊢ M_{:τ} Γ[x ↦ ∀α_{1} … ∀α_{n}.τ] ⊢ N_{:τ′}}{Γ ⊢ let x_{:∀α_{1}...∀α_{n}.τ} = M_{:τ} in N_{:τ′}} (∀i ≤ n) α_{i} ∉ F T V (Γ)

Theorem 3 If a term M of the interface language is typable, T_{P} returns the principal type of M and a well-typed annotated term for M. Otherwise T_{P} reports a type error.

4 Compilation

From any type-annotated weak selective λ-term, we can compile away labels, to obtain a classical λ-calculus term. We propose here a method to do that, and prove its syntactic soundness and semantic correctness.

4.1 Compilation method

[M_{:τ′}]_{τ}, the compilation of the type-annotated selective λ-term M_{:τ′} under the labeled type τ” is defined as follows. [M]_{τ} is an abbreviation for [M_{:τ}]_{τ}.

[M_{:τ′}]_{τ} = T ([M]_{τ′}, τ′, τ)_{[x]_{τ}  = x}_{[c]_{τ}  = c} [λl:x.M_{:τ′}]_{l:θ→τ}  = λx.[M_{:τ′}]_{τ}
[M_{:τ′} l:N_{:θ}]_{τ}  = [M_{:τ′}]_{l:θ→τ} [N]_{θ}
[let x_{:σ} = M_{:τ} in N_{:τ′}]_{τ′} = let x = [M]_{τ} in [N]_{:τ′}

(let)  let x_{:∀α_{1}...α_{n}.τ} = M_{:τ} in N_{:τ′} → [M_{:τ}/x_{:∀α_{1}...α_{n}.τ}]N_{:τ′}
(β)  ((… (λl:x.M_{:τ})_{:τ_{1}} …)_{:τ_{n}} l_{1}:N_{:θ_{1}}^{1} … l_{n}:N_{:θ_{n}}^{n} l:N_{:θ})_{:τ′} if ∀i ≤ n, l_{i} ≠ l
→ ((… ([N′/x]M_{:τ})_{:ν_{1}} …)_{:ν_{n}} l_{1}:N_{:θ_{1}}^{1} … l_{n}:N_{:θ_{n}}^{n})_{:τ′}
where N′ = (… (N_{:θ})_{:A_{l}(τ_{n})} …)_{:A_{l}(τ_{1})} and ν_{i} = R_{l}(τ_{i})
(δ)  ((… c_{:l:θ_{1}→τ_{1}} …)_{:l:θ_{n}→τ_{n}} l:N_{:θ_{n}})_{:τ_{n}} → (… δ(c, l:(… N_{:θ_{n}} …)_{:θ_{1}})_{:τ_{1}} …)_{:τ_{N}}
Convert ((M_{:l:θ→τ} l:N_{:θ})_{:τ})_{:τ′} → ((M_{:l:θ→τ})_{:l:θ→τ′} l:N_{:θ})_{:τ′}  if τ_{1} ≃ τ_{2}
Simplify (M_{:τ})_{:τ} → M_{:τ}

Figure 5: Typed reduction rules

The above definition just handles type annotations. The real work is delegated to the type conversion T . (In the second case, ξ is a permutation of [1, n].)

T (M, τ, τ)  = M
T (M, {l_{ξ_{i}}:τ_{ξ_{i}}}_{1}^{n} → τ, {l_{i}:τ′_{i}}_{1}^{n} → τ′)=λ^{∗}x_{1} … x_{n}.T (M T (x_{ξ_{1}}, τ′_{1}, τ_{ξ_{1}}) … T (x_{ξ_{n}}, τ′_{n}, τ_{ξ_{n}}), τ, τ′)
T (M, τ_{1} × … × τ_{n}, τ′_{1} × … × τ′_{n}) = (λ^{+}x.(T (π_{1}^{n}^{∗} x, τ_{1}, τ′_{1}), …, T (π_{n}^{n}^{∗} x, τ_{n}, τ′_{n}))) M
T (M, τ option, τ′ option)  = case^{∗}(M, λx.Some(T (x, τ, τ′)), None)

The marks (∗ and +) introduced by type conversion do not change the meaning of terms. We can use them to optimize the translation: β and η-redexes including a marked λ^{∗} can be reduced without changing intuitive semantics — for β-redexes, use of the abstracted variable is linear, and for η-redexes, they were absent before the translation. —This is also true for λ^{+}, but only when applied to an actual tuple, and the following π^{∗}’s are immediately δ-reduced. Similarly case^{∗}’s can be δ-reduced.

We note [M]_{τ}^{∗} for the optimized compilation of M, that is [M]_{τ} where all the above was done. We define also a weaker compilation, [M]_{τ}^{∗n}, where all η∗-redexes are reduced, but other ∗ and + redexes are only reduced when they appear at the leftmost position of the compiled term (i.e. (λ^{∗}x.M) N_{1} … N_{n}, (λ^{+}x.M) (N_{11}, …, N_{1n}) … N_{n}, or case^{∗}(M, N, P) N_{1} … N_{n}). That is, we only reduce at compilation what could be done by the call-by-name λ-calculus.

4.2 Correctness of compilation

Before proving correctness, we need some referent calculus before compilation. For this we add a typed reduction system to our type-annotated terms.

4.2.1 Typed reduction

The typed reduction rules are in Figure 5. When the variable to substitute is not annotated by a polytype, variable substitution needs no special care, out of renaming bound variables as usual. But when it is annotated by a polytype, as may happen with let-conversion, we need to do some type variable substitution on all annotations of the substituted term:

[M_{:τ}/x_{:∀α_{1}...α_{n}.τ}]x_{:τ′} = S(M_{:τ}) if \{ \begin{matrix}D_{S} = \{α_{1}, …, α_{n}\} \\ S(τ) = τ′ \end{matrix}

In (β), there should be only first conversions, then applications on the path between M and N. Type conversions are pushed inside by Conversion, or eliminated by Simplify.

(δ) applies only if there is a corresponding δ-rule^{6}.

δ(π_{i}^{n}, 1:(M_{1}, …, M_{n}))  = M_{i}
δ(case, 1:(Some M, N, P)) = N 1:M
δ(case, 1:(None, N, P))  = P
δ(fix, 1:M)  = M 1:(fix 1:M)

All these rules preserving type information,

Proposition 1 (subject reduction) For each typed reduction step M_{:τ} → N_{:τ′}, if Γ ⊢ M_{:τ} then τ = τ′ and Γ ⊢ N_{:τ′}.

Theorem 4 The type-annotated weak selective λ-calculus is confluent.

4.2.2 Correctness properties

One may think of several ways to prove a compilation algorithm correct. The most usual one is to use a common model before and after compilation, and prove the algorithm correct with respect to this model. We do this for call-by-name evaluation.

The property we prove first here is slightly different. Since we are translating into the lambda calculus, and one may think of various models (or evaluation strategies) for it, we do not commit to one of them, and prove a more general property on rewrite systems.

Theorem 5 (syntactic soundness) If M_{:τ} → N_{:τ} in the type-annotated weak selective λ-calculus, then [M]_{τ}^{∗}→^{∗}[N]_{τ}^{∗}.

Theorem 6 (semantic correctness) [·]_{τ}^{∗} compilation is correct with respect to call-by-name operational semantics. That is, if M_{:τ} is a closed term of base type, then

1. when call-by-name strategy leads to a normal form N_{:τ}, then [M]_{τ}^{∗} is reduced to the normal form [N]_{τ}^{∗} by the same strategy.

2. when call-by-name strategy leads to an infinite reduction, its application to [N]_{:τ}^{∗} also leads to an infinite reduction.

Remark that we do not have correctness with respect to call-by-value semantics: every time call-by-value evaluation of M_{:τ} terminates, call-by-value evaluation of [M]_{:τ}^{∗} also terminates, which gives us soundness, but since we introduce abstractions in the compilation process, the inverse is not true.

6This is a simplified version: we require the parameter of the δ-rule to be the first argument. This is not a limitation since we recover full generality by an η-expansion for the parameter.

5 Efficiency considerations

The goal of the above compilation method (including the simplifications done by type inference) is to produce code, of course correct, but also with a minimal overhead against a non-labeled program. In particular the choice to compile towards classical lambda-calculus rather than a new abstract machine avoids handicapping programs using labels in a nonessential way (with no out-of-order partial applications). Actually, in a program containing only full applications of functions (or in-order partial applications), the ∗-optimized compilation just reorders the arguments in function applications, to match the definition template.

We still need to extend a little ∗-compilation to handle efficiently out-of-order partial applications. By substituting all marked redexes at compilation, we may happen to move a function application inside an abstraction:

[M_{:p:θ→q:τ→τ′} q:(f a)_{:τ}]_{p:θ→τ′}^{∗} = (λ^{∗}x.λ^{∗}y.M y x) (f a) → λ^{∗}y.M y (f a)

This results potentially into multiple evaluations of (f a). To avoid this, we: 1) put terms in Convert/Simplify normal form before compiling them; 2) introduce let-definitions to keep non-values (head-reducible terms, that includes applications and let-definitions containing applications) out of abstractions; 3) limit compile-time β-reduction to values.

let^{∗} z = f a in (λ^{∗}x.λ^{∗}y.M y x) z → let^{∗} z = f a in λ^{∗}y.M y z

These let-definitions are transparent: (let^{∗} x = N in M) N′ → let^{∗} x = N in M N′.

With this compilation method, we only depart from usual operational semantics (either lazy or strict) in that no reduction of the function is done when there is an “hole” in the partial application of a function, like in (f_{:p:i→q:i→r:i→i} p:a r:b) : a and b are shared, but f a is not reduced. One may of course force the reduction by doing the application in two stages, but this problem is generally not very important: real evaluation of partial application is very rare, a fortiori in such an unintentional way.

As a conclusion, no overhead is involved by using labels, other than what would have been needed anyway in order to write an out-of-order partial application, and semantics are kept even with strict evaluation, except for side-effects in out-of-order partial applications (we should give a warning for functions that return an unprotected function type after having side-effects, they are ambiguous).

For optional parameters, two sources of inefficiency can be seen. One is the need for using an explicit constructor Some for all actually passed parameters, the other is that even if a parameter is not passed, None must be passed in its place. In most implementations, the first inefficiency can be reduced by a little cooperation from the back-end. This is based on the following remark: a value of type (… (τ option) …) option can only be either Some(… Some(a_{:τ}) …) or Some^{n}(None) (where 0 ≤ n ≤ the number of option levels in the type). In an implementation distinguishing between scalars and pointers by the highest bit of words (like Caml Light [9] for instance), we can view the latter as an array containing all constants of this form (a finite number is enough), its location completely distinct from any other value. As a result, we do not need the Some constructor in representations, and all option manipulation can be done without any heap access. On the other hand, the second problem seems intrinsic to currying.

6 Conclusion

Labeled and optional arguments were not handled by strongly typed functional programming languages. This is now done… in theory!

Our proposal leaves to the user the choice between writing labeled programs or not, without adding any new cost to the last alternative.

Advantages of labeled programs and libraries are

• Better readability of the source code.

• More information in the type.

• No parameter order to remember.

• Easier to add parameters to library functions.

• Syntax closer to object-oriented style.

Concern about semantics remains. While integration of this system in a lazy functional programming language like Haskell [7] creates no difficulty (in the worse —and exceptional— case, some sharing will be lost), for ML-style strict languages with sideeffects we must be more careful. Faulty programs have in common a dangerous use of partial application, producing side-effects. If all functions are defined such that they may only have side-effects when all their parameters are applied, this concern disappears. Since such a constraint also makes possible other source code transformations, we think that it may be worth considering it.

References

[1] Hassan Aït-Kaci and Jacques Garrigue. Label-selective λ-calculus: Syntax and confluence. In Proc. of the Conference on Foundations of Software Technology and Theoretical Computer Science, pages 24–40, Bombay, India, 1993. Springer-Verlag LNCS 761. Journal version to appear in Theoretical Computer Science.

[2] L. Damas and R. Milner. Principal type-schemes for functional programs. In Proc. ACM Symposium on Principles of Programming Languages, pages 207–212, 1982.

[3] Roberto Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkhauser, 1995. ISBN-0-8176-3763-X.

[4] Hsianlin Dzeng and Christopher T. Haynes. Type reconstruction for variable-arity procedures. In Proc. ACM Conference on LISP and Functional Programming, pages 239–249, 1994.

[5] Jacques Garrigue and Hassan Aït-Kaci. The typed polymorphic label-selective λcalculus. In Proc. ACM Symposium on Principles of Programming Languages, pages 35–47, 1994.

[6] Adele Goldberg and David Robson. Smalltalk-80: The Language and its Implementation. Addison-Wesley, Reading, Mass., 1983.

[7] Haskell committee. Haskell report 1.2. SIGPLAN Notices, 27(5), May 1992.

[8] Henry Ledgard. ADA : An Introduction, Ada Reference Manual (July 1980). Springer-Verlag, 1981.

[9] Xavier Leroy. The Caml Light System Documentation, release 0.7. INRIA, Rocquencourt, France, July 1995. Available at URL http://pauillac.inria.fr/caml/man-caml.

[10] Atsushi Ohori. A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages and Systems, to appear.

[11] John K. Ousterhout. Tcl and the Tk toolkit. Addison-Wesley, 1994. ISBN 0-201-63337-x.

[12] Didier Rémy. Typechecking records and variants in a natural extension of ML. In Proc. ACM Symposium on Principles of Programming Languages, pages 77–87, 1989.

[13] François Rouaix. The CamlTk Interface. INRIA, Rocquencourt, France, July 1995. Available at URL http://pauillac.inria.fr/camltk.

[14] Guy L. Steele. Common LISP : The Language. Digital Press, 1984.

[15] Masako Takahashi. Parallel reductions in λ-calculus. Information and Computation, 118:120–127, 1995.

[16] Pierre Weis et al. The CAML Reference Manual, version 2.6.1. Projet Formel, INRIA-ENS, 1990.

A Proofs

Theorem 1 The weak selective λ-calculus is confluent.

PROOF: Like for classical λ-calculus, this is easily proved by parallel reductions [15]. □

Theorem 2 There is a terminating algorithm to solve the mgu of a set of type equations.

PROOF: System correctness. In each rule, any unifier of the denominator unifies also the numerator, and conversely, any unifier of the numerator can be extended to a unifier of the denominator by introducing new variables missing in the numerator. We only detail the case of Completion. If σ is a solution of the numerator, then

{l_{i}:σ(τ_{i})}_{1}^{n} → σ(ρ) ≃ {l′_{i}:σ(τ′_{i})}_{1}^{m} → σ(ρ′)

Since all l_{i} and l′_{i} are distinct each other, σ(ρ) must have labels which correspond with {l′_{i}:τ′_{i}}_{1}^{m}. More correctly,

σ(ρ) = {l′_{i}:τ′_{i}}_{1}^{m} → τ and σ(ρ′) = {l_{i}:τ_{i}}_{1}^{n} → τ′

for some τ ≃ τ′. Then if we extend σ such that σ(α) = τ, σ can be a solution of the denominator. The converse is clear by construction.

Termination. We show that the algorithm terminates if we give priority to failure rules. A variable is solved when it appears only once and as the left-hand-side of an equation. And the size of a type is the total number of labels, variable occurrences, base types, × and option it contains. We adopt (number of unsolved variables, sum of sizes) as lexicographical measure to show the termination. All rules except Completion reduce the measure. For Completion, if one of ρ and ρ′ is not a variable, then next step is a failure. Otherwise we introduce one new variable, but solve two.

Well-formedness of the result. Last we must show that our result is in solved form. First, in every equation, at least one side is a solved variable. If the two sides are functional types, then either Decomposition, Completion, or one of failure rules applies. If one side is a base type, then the other side is a solved variable, otherwise Redundancy or Failure applies. If the two sides are variables, then at least one is solved. We construct the substitution σ by taking for each equation α = τ, α solved, σ(α) = τ. σ is a most general unifier of the final system, and as a consequence, if we suppress definitions for all variables introduced by Completion, σ′ is a most general unifier of the original system. □

Theorem 3 If a term M of the interface language is typable, T_{P} returns the principal type of M and a well-typed annotated term for M. Otherwise T_{P} reports a type error.

PROOF: (Sketch) All type inference rules correspond exactly to one case of the type reconstruction algorithm, except generalization and instantiation. Since the algorithm only adds the constraints insured by type inference rules and introduces generalization and instantiation at most general places, it is sound and complete. Together with the principal type τ, T_{P} returns a type-annotated term of type ⌈τ⌉. When T_{P} does not introduce any polymorphism, it is easy to check T_{P} returns a well-typed annotated term, particularly in application M′ is type converted to the order and types of its arguments. When introducing polymorphism (let and let rec), type-annotated terms of each declarations are generalized, but these generalizations are all syntactically correct for the type annotated calculus. □

Proposition 1 (subject reduction) For each typed reduction step M_{:τ} → N_{τ′}, if Γ ⊢∈ M_{:τ}, then Γ ⊢ N_{:τ′} and τ = τ′.

PROOF: This is clear for Convert and Simplify.

For (β) and δ-rule, we reconstruct all the type conversions necessary. Thanks to type-variable substitution when needed, (let) works also. □

Theorem 4 The type-annotated weak selective λ-calculus is confluent.

PROOF: (sketch). We first remark that Convert and Simplify commute with themselves and each other. This solves their critical pairs. This is also true for δ-rules, except fix. However one-step (β), (let) and δ-fix may duplicate some redexes, which prohibits immediate commutation. Following Takahashi [15], we define their parallel reduction as the simultaneous reduction of any number of non-overlapping (β), (let) and δ-fix redexes. The result for classical lambda-calculus directly extends to give us local confluence of parallel (β)-(let)-δ-fix, and confluence of the combination of (β), (let) and δ-fix. We may then show that one-step (β), (let) or δ-fix commutes with multiple steps of other rules. As a result multi-step (β)-(let)-δ-fix commutes with multiple steps of other rules. If we have two confluent rewriting systems, and they commute with each other, then their union is confluent. □

18 A. PROOFS

Theorem 5 (syntactic soundness) If M_{:τ} → N_{:τ} in the type-annotated weak selective λ-calculus, then [M]_{τ}^{∗}→^{∗}[N]_{τ}^{∗}.

PROOF: Remark first that Convert and Simplify change nothing to the compiled term: see the translation of type coercion when τ′ ≃ τ, and that of application, and apply ∗-normalization afterwards.

For (β) and (let), the proof is by induction on the structure of the term in which the variable is substituted. After reducing the translated redex in [M]_{τ}^{∗} → M′, the term we obtain contains potentially reducible ∗ and +-redexes, created by the application of the substituted term to its new contexts, or by the reduction of a redex. By reducing them, we reach [N]_{τ}^{∗}. □

Lemma 1 If τ is a base type, and M_{:τ} → N_{:τ} in the call-by-name evaluation strategy, then [M]_{τ}^{∗n}→^{∗}[N]_{τ}^{∗n} in the call-by-name evaluation strategy.

PROOF: Similar to Theorem 5. We give only the differences.

Since τ is a base type, M_{:τ} is either a variable, a basic constant or an application. As a result, after ∗n-normalization, the leftmost position of [M]_{τ}^{∗n} corresponds to that of M_{:τ}, so if we can reduce M_{:τ} in the call-by-name evaluation strategy, then we can also do [M]_{τ}^{∗n} → M′ in it. By applying ∗n-normalization to the resulting M′, we obtain [N]_{τ}^{∗n}. □

Theorem 6 (semantic correctness) [·]_{τ}^{∗} compilation is correct with respect to call-by-name operational semantics. That is, if M_{:τ} is a closed term of base type, then: (1) when call-by-name strategy leads to a normal form N_{:τ}, then [M]_{τ}^{∗} is reduced to the normal form [N]_{τ}^{∗} by the same strategy; (2) when call-by-name strategy leads to an infinite reduction, its application to [N]_{:τ}^{∗} also leads to an infinite reduction.

PROOF: From Theorem 5 and confluence of both systems, we obtain (1): call-by-name leads to a normal form whenever it exists.

Since [M]_{τ}^{∗n}→^{∗}[M]_{τ}^{∗}, whenever call-by-name evaluation of [M]_{τ}^{∗} leads to a normal form, evaluation of [M]_{τ}^{∗n} leads to the same one. By Lemma 1, there exist N_{:τ}, such that [N]_{τ}^{∗} —in this case this is equal to [N]_{τ}^{∗n}— is this normal form. Once normalized by Convert and Simplify, N_{:τ} is also a normal form, and it is obtained by call-by-name normalization of M_{:τ}. By negation of this, (2) stands. □