Once upon a type^{∗}

David N. Turner Philip Wadler University of Glasgow^{†}

 dnt,wadler@dcs.glasgow.ac.uk

Christian Mossin University of Copenhagen^{‡}

                                    mossin@diku.dk.

November 13, 1997

Abstract

A number of useful optimisations are enabled if we can determine when a value is accessed at most once. We extend the Hindley-Milner type system with uses, yielding a type-inference based program analysis which determines when values are accessed at most once. Our analysis can handle higher-order functions and data structures, and admits principal types for terms.

Unlike previous analyses, we prove our analysis sound with respect to call-by-need reduction. Call-by-name reduction does not provide an accurate model of how often a value is used during lazy evaluation, since it duplicates work which would actually be shared in a real implementation.

Our type system can easily be modified to analyse usage in a call-by-value language.

1 Introduction

This paper describes a method for determining when a value is used at most once. Our method is based on a simple modification of the Hindley-Milner type system. Each type is labelled to indicate whether the corresponding value is used at most once, or may possibly be used many times.

Our type system has a number of applications:

∗Technical Report TR-1995-8, Computing Science Department, University of Glasgow. Conference version in 7’th International Conference on Functional Programming and Computer Architecture, San Diego, California, June 1995. This work was supported by EPSRC (GR/J 527099), ‘Save space with linear types’, ESPRIT (6809) ‘Semantique’, ESPRIT (ECUS025) ‘Atlantique’, and the Danish Technical Research Council.

†Computing Science Department, University of Glasgow, Glasgow G12 8QQ, Scotland.

‡DIKU, University of Copenhagen, Universitetsparken 1, 2100 Copenhagen Ø, Denmark. This work was performed while Mossin was visiting the University of Glasgow.

Program transformation: If it is determined that a variable is accessed at most once, then one may safely inline the expression bound to the variable without reducing efficiency. In particular, we can determine when it is safe to inline an expression into the body of a function.

Avoiding closure update: Implementations of lazy languages use updates to share the evaluation of closures. If it is determined that a closure is accessed at most once, then there is no need to overwrite the closure with the result of evaluation.

Enabling data structure update: If it is determined that a structure such as a ‘cons’ cell or an array is accessed at most once, then the structure may safely be updated in place.

The last of these application areas has received considerable attention, the second of these some attention, and the first almost none. This is quite surprising, since expression inlining is central to a wide range of program transformations. In particular, our method provides a sound basis for a number of transformations that were previously dealt with in an ad hoc manner in the Glasgow Haskell Compiler.

Previous analyses to determine when a value is used at most once have been based on either call-by-name reduction (Wright and Baker-Finch [WB93], Courtenage and Clack [CC94]) or call-by-need reduction (Launchbury et al. [Lau92], Marlow [Mar93]). The call-by-name analyses have been proved sound, but are not well-suited for optimisation of lazy languages. Our analysis is the first call-by-need analysis to be proved sound, and sometimes provides more accurate information than other call-by-need analyses. Our proof of soundness is based on the operational semantics of Launchbury [Lau93] and the call-by-need calculus of Ariola et al. [AFMOW95].

The type system presented here is based on ideas taken from the linear logic of Girard [Gir87] and its successor the Logic of Unity [Gir93]. However, it turns out to be convenient to present this work without reference to linear logic. Some of the connections are traced in a companion paper [MOTW95], which relates linear logic to the call-by-need calculus of Ariola et al.

We modify the Hindley-Milner type system [Hin69, DM82] by attaching uses to types. Type judgements include a constraint set relating uses, similar to the constraint sets relating subtypes in the work of Mitchell [Mit84, Mit91]. As with the Hindley-Milner system, there is an algorithm that determines a principal type for an expression. Annotating types with usage information also provides a convenient mechanism for communicating usage information across module boundaries, since typed languages such as Haskell already import type information from separately-compiled modules.

A small modification to our analysis enables it to determine when variables are used exactly once (as opposed to at most once), making it suitable for use with call-by-value (as opposed to call-by-need) evaluation.

1.1 The problem

Some examples may help to illustrate the nature of the problem solved.

We wish to attach uses to values. The use 1 indicates that a value is used at most once, while the use ω indicates that a value may be used any number of times.

Consider the following. (Example 1.)

let x = 1 + 2 in

\begin{matrix}let y = x + 3 in \\ y + y \end{matrix}

Here it is safe to replace x by 1 + 2 within the body of the outer ‘let’. But it is not safe to replace y by x+3 within the body of the inner ‘let’, as the resulting program would compute x + 3 twice rather than once. Our type system attaches use 1 to x and use ω to y.

Our argument depends crucially on the use of a call-by-need semantics. Under a callby-name semantics x + 3 is always computed twice. A call-by-name analysis must therefore attach a use equivalent to ω to both x and y, showing why such analyses are not suited for our purpose.

At first glance, it may seem child’s play to determine if a value is used at most once under call-by-need. Surely, if a variable appears at most once in a program, then the value it is bound to is used at most once? In fact, this is not the case.

Consider the following. (Example 2.)

let x = 1 + 2 in

\begin{matrix}let f = λz. x + z in \\ f 3 + f 4 \end{matrix}

Even though x appears only once in the body of the outer ‘let’, replacing x by 1 + 2 is unsafe, as the resulting program will compute 1+2 twice rather than once. Our type system attaches use ω to both x and f.

Consider the following. (Example 3.)

let x = 1 + 2 in
let f = (let y = x + 3 in λz. y + z) in
f 4 + f 5

Here, again, one can safely replace the one occurrence of x by 1 + 2, although it may require a moment’s thought to convince oneself this is the case. Indeed, this example is sufficiently difficult that the analyses proposed by Launchbury et al. [Lau92] and by Marlow [Mar93] are both overly conservative, and in effect attach use ω to x. However, our type system attaches use 1 to x and use ω to y and f.

1.2 Call-by-need

Our work is based on the operational semantics of call-by-need proposed by Launchbury [Lau93], and on the call-by-need lambda calculus of Ariola et al. [AFMOW95]. A correspondence between these two approaches has already been shown in the latter work.

Launchbury’s rules include an explicit treatment of closure update. By modifying his rules to allow some closures to be non-updating, we verify that our type system can be used to avoid unnecessary closure updates.

The soundness of our type system is established by showing that it satisfies a subject reduction property: applying a call-by-need reduction to a term leaves its type unchanged, including type information regarding usage.

Launchbury restricts functions to be applied to variables, while Ariola et al. allow functions to be applied to arbitrary expressions. As we explain in Section 6, the difference between these approaches is significant for our chosen implementation, the Glasgow Haskell Compiler [PHHPW93], which is closely based on the STG-machine of Peyton Jones [Pey92]. Therefore, in this paper we adopt Launchbury’s syntax (which was influenced by the Haskell compiler and the STG-machine), and adapt the results of Ariola et al. to it. (In the conference version of this paper [MTW95], we disallowed mutually-recursive let-bindings so as to simplify the presentation of our analysis. We remove that restriction here.)

1.3 Program transformation

If we want to use program transformation as the basis of efficient compilation of a functional language, it is not only important that transformation preserves meaning but also that the transformed program executes at least as fast as the original.

Consider Church’s beta rule:

(λx. e_{1}) e_{2} ⟹ [e_{2}/x]e_{1}.

This rule is good in that it eliminates one application step, but bad in that it may duplicate some computation. (In particular, computation of e_{2} may be duplicated if x is used more than once in e_{1}.)

The call-by-need calculus of Ariola et al. addresses this problem by modifying the above rule:

(λx. e_{1}) e_{2} ⟹ let x = e_{2} in e_{1}.

This rule, together with a number of rules for manipulating ‘let’, allow us to safely transform programs, without the risk of duplicating work.

However, there are a number of transformations that are useful and safe and which are not part of the call-by-need calculus. The most important of these is that the beta rule

(λx. e_{1}) e_{2} ⟹ [e_{2}/x]e_{1}

is safe when x has use 1. Another is that the rule

let x = e_{1} in λy. e_{2} ⟹ λy. let x = e_{1} in e_{2}

is safe when the function λy. e_{2} has use 1. Both of these transformations are used extensively in the Glasgow Haskell Compiler. Until now, their safety was ensured only by ad hoc techniques. And the ad hoc techniques were not adequate – an unsafe version of the second rule was accidentally allowed, with the result that the compiler itself (which is bootstrapped) was slowed by as much as one third [SP95].

Another example of program transformation is the deforestation algorithm [Wad90a]. In order to ensure safety, this algorithm requires that variables be used at most once. The definition of ‘used at most once’ is easy because deforestation applies to a first-order language. Attempts to apply deforestation to higher-order [MW92] have been hindered by the lack of a suitable definition of ‘used at most once’ at higher-order. This paper provides such a definition.

1.4 Outline

This paper is organised as follows. Section 2 introduces the language and its semantics. Section 3 describes the fundamentals of the type system. Section 5 discusses principal types and polymorphism, and presents a type inference algorithm. Section 6 summarises the callby-need reduction rules. Section 7 discusses how to adapt the analysis so that it is appropriate for a call-by-value language. Section 8 describes related work. Section 9 concludes.

Note that this paper extends the results presented in the conference version of this paper [MTW95] in three respects: we extend our analysis to include mutually-recursive letbindings; we show that our typing rules can be reformulated as a set of simple, syntaxdirected, typing rules; and we present a type inference algorithm.

2 Language

We now present the syntax and operational semantics of a call-by-need lambda calculus extended with integers, lists, and recursion.

2.1 Terms

The syntax of the language is given below. We use the syntax of Launchbury [Lau93] where arguments in applications and in ‘cons’ are restricted to variables and ‘let’ is mutually recursive. When the length of a sequence is clear from the context, or is unimportant, we let \overline{x} denote x_{1}, …, x_{n} and ‘let \overline{x} = \overline{e} in e’ denote ‘let x_{1} = e_{1}, …, x_{n} = e_{n} in e’.

Variables x, y, z
Values  v ::= λx. e | n | nil | cons x y
Terms  e ::= v | x | e x | e_{1} + e_{2} |
case e_{1} of {nil → e_{2}; cons x y → e_{3}} |
let x_{1} = e_{1}, …, x_{n} = e_{n} in e

It is trivial to translate terms with the standard syntax for application and ‘cons’ into the restricted syntax, for example we can translate ‘e_{1} e_{2}’ to ‘let x = e_{2} in e_{1} x’. The syntax closely resembles the STG language [Pey92].

2.2 Use annotations

The operational semantics of this section and the reduction rules of Section 6 require that let-bound variables be annotated with uses.

Each let-bound variable x is annotated with a use |x|, which is either 1 or ω. If |x| = 1, then x may be used at most once during evaluation, and if |x| = ω then x may be used any number of times. Note that we do not specify how one chooses annotations for variables (in particular, we do not require terms to be well-typed).

2.3 Heaps

A heap abstracts the state of the store at a point in the computation. It is an unordered set of bindings associating variables with terms. A configuration pairs a heap with a term, and is written ⟨H⟩ e.

Heaps H ::= x_{1} : e_{1}, …, x_{n} : e_{n}

2.4 Evaluation rules

The figure below presents a natural semantics for lazy evaluation, which closely resembles the one given by Launchbury. The key difference is that the evaluation of a let-bound variable depends on its use annotation.

Evaluation rules have the form ⟨H_{1}⟩ e ⇓ ⟨H_{2}⟩ v, meaning that evaluating expression e in initial heap H_{1} returns value v and final heap H_{2}.

Rule Var-Once evaluates a variable that is used at most once. It looks up the expression e that is bound to the variable x in the heap and then evaluates e. As the variable will no longer be used, its binding is removed from the heap.

Rule Var-Many evaluates a variable that may be used many times. It looks up the expression e that is bound to the variable x in the heap, evaluates e, and updates the heap to bind x to the resulting value. In practice, the update required by Var-Many may have a significant cost, whereas Var-Once avoids this cost.

Var-Once \frac{|x| = 1 ⟨H_{1}⟩ e ⇓ ⟨H_{2}⟩ v}{⟨H_{1}, x : e⟩ x ⇓ ⟨H_{2}⟩ v}  Var-Many \frac{|x| = ω ⟨H_{1}⟩ e ⇓ ⟨H_{2}⟩ v}{⟨H_{1}, x : e⟩ x ⇓ ⟨H_{2}, x : v⟩ v}

Abs \overline{⟨H⟩ λx. e ⇓ ⟨H⟩ λx. e}  App \frac{⟨H_{1}⟩ e_{1} ⇓ ⟨H_{2}⟩ λx. e_{2} ⟨H_{2}⟩ [y/x]e_{2} ⇓ ⟨H_{3}⟩ v}{⟨H_{1}⟩ e_{1} y ⇓ ⟨H_{3}⟩ v}

Int \overline{⟨H⟩ n ⇓ ⟨H⟩ n}  Plus \frac{⟨H_{1}⟩ e_{1} ⇓ ⟨H_{2}⟩ n_{1} ⟨H_{2}⟩ e_{2} ⇓ ⟨H_{3}⟩ n_{2}}{⟨H_{1}⟩ e_{1} + e_{2} ⇓ ⟨H_{3}⟩ \underline{n_{1} + n_{2}}}

Nil

⟨H⟩ nil ⇓ ⟨H⟩ nil

Cons

⟨H⟩ cons x y ⇓ ⟨H⟩ cons x y

Case-Nil \frac{⟨H_{1}⟩ e_{1} ⇓ ⟨H_{2}⟩ nil ⟨H_{2}⟩ e_{2} ⇓ ⟨H_{3}⟩ v}{⟨H_{1}⟩ case e_{1} of \{nil → e_{2}; cons x y → e_{3}\} ⇓ ⟨H_{3}⟩ v}

Case-Cons \frac{⟨H_{1}⟩ e_{1} ⇓ ⟨H_{2}⟩ cons y_{1} y_{2} ⟨H_{2}⟩ [y_{1}/x_{1}, y_{2}/x_{2}]e_{3} ⇓ ⟨H_{3}⟩ v}{⟨H_{1}⟩ case e_{1} of \{nil → e_{2}; cons x_{1} x_{2} → e_{3}\} ⇓ ⟨H_{3}⟩ v}

Let \frac{fresh y_{1}, …, y_{n} ⟨H_{1}, y_{1} : [\overline{y}/\overline{x}]e_{1}, …, y_{n} : [\overline{y}/\overline{x}]e_{n}⟩ [\overline{y}/\overline{x}]e ⇓ ⟨H_{2}⟩ v}{⟨H_{1}⟩ let x_{1} = e_{1}, …, x_{n} = e_{n} in e ⇓ ⟨H_{2}⟩ v}

Rule Abs is trivial, since a lambda abstraction is already a value. Rule App evaluates applications by evaluating the function to yield a lambda abstraction, then evaluating the body of the abstraction with the argument substituted for the bound variable of the abstraction.

Rules Int and Plus are easy. Rules Nil and Cons are trivial since both ‘nil’ and ‘cons x y’ are already values. The two Case rules are again straightforward.

The Let rule creates a number of new bindings on the heap. In this rule y_{1}, …, y_{n} are all fresh names not appearing in the expression or the heap.

Observe that all bindings added to the heap use fresh variables, so it trivially follows that all bindings in the heap are unique. (In Launchbury’s formulation, renaming occurs during variable access rather than during evaluation of a binding construct.)

3 A use type system

We now present a type system which indicates when values will be accessed at most once. For simplicity, the type system is monomorphic; extensions which allow polymorphism are discussed in Section 5.

3.1 Uses and Constraints

Types will be annotated with uses. A type is annotated with use 1 if each value of that type is used at most once, and annotated with ω otherwise. To enable type inference, we also allow use variables (ranged over by j, k, l, m).

Uses κ ::= j | 1 | ω

We use Θ to record the constraints generated by our typing rules. We define Θ to be a set of constraints of the form j ≤ {k_{1}, …, k_{n}}. The constraint set Θ is essential if we wish to have principal types for terms, since it allows us to accumulate constraints on a use variable without forcing it to be (prematurely) instantiated to 1 or ω.

The following rules define an ordering on uses, parameterised on a constraint set Θ:

Omega \overline{κ ≤_{Θ} ω}  One \overline{1 ≤_{Θ} κ}  Refl \overline{κ ≤_{Θ} κ}

Taut \frac{(j ≤ \{k_{1}, …, k_{n}\}) ∈ Θ}{j ≤_{Θ} k_{i}}

3.2 Types

Types include type variables (let a, b, c range over these), function types, integers, and list types.

Types τ ::= a^{κ} | τ →^{κ} τ′ | Int^{κ} | [τ]^{κ}

The type a^{κ} indicates that the type variable a ranges over types with use κ. The type τ →^{κ} τ′ denotes functions from type τ to type τ′ that can be used at most κ times, Int^{κ} denotes integer values that can be used at most κ times, and [τ]^{κ} denotes lists with elements of type τ, where the list can be accessed at most κ times.

Write |τ| for the use attached to type τ, defined as below:

|a^{κ}| = κ |τ →^{κ} τ′| = κ |Int^{κ}| = κ |[τ]^{κ}| = κ

We impose the following well-formedness condition on list types:

The type [τ]^{κ} is well-formed only if κ ≤_{Θ} |τ|.

In other words, if a list can be accessed many times, then its elements also might be accessed many times (through the list). A similar restriction appears in the type systems of Guzmán and Hudak [GH90] and Wadler [Wad90b, Wad91].

3.3 Contexts

A context associates a type with each variable that may appear in a term, and is represented by a list of entries of the form x : τ.

Contexts Γ, Δ ::= x_{1} : τ_{1}, …, x_{n} : τ_{n}

Each variable in a context must be distinct. If x : τ is in Γ, we say that x has use κ if |τ| = κ. If Γ and Δ are contexts containing no variables in common, write Γ, Δ to denote the concatenation of the two contexts.

We extend our ordering on uses so that it applies to complete contexts, written κ ≤_{Θ} |Γ| and defined as below:

κ ≤_{Θ} |x_{1} : τ_{1}, …, x_{n} : τ_{n}| iff κ ≤_{Θ} |τ_{i}| for all i

Consider the constraint κ ≤_{Θ} |Γ|. If κ = 1, then no constraint is placed on any use in Γ. But if κ = ω then for every entry x_{i} : τ_{i} in Γ, our definition implies that |τ_{i}| = ω.

3.4 Typing judgements

Typing judgements take the form Γ ⊢_{Θ} e : τ, indicating that in context Γ, and under the constraints Θ, the term e has type τ. The structural typing rules have the more general form Γ ⊢_{Θ} e_{1}, …, e_{n} : τ_{1}, …, τ_{n}, indicating that in context Γ, and under the constraints Θ, each term e_{i} has type τ_{i}. (This n-ary form of typing rule is only required to typecheck mutually-recursive let-bindings.) The type rules are shown in Figure 1.

The type rules are quite similar to the usual rules for lambda calculus, so we concentrate on explaining the unusual features: the structural rules, and the constraints on uses.

3.5 Structural rules

The manipulation of contexts is carefully designed so that if any variable is used more than once this will be indicated by the presence of the structural rule contraction (Cont), which introduces the use ω.

Terms that may be evaluated together are typed in different contexts which are then combined, as can be seen in rules App, Plus, Cons, Case, and Let. As all variables in a context must be distinct, the only way for the same variable to be used more than once is via the Cont rule. In this rule, the substitution [z/x, z/y]e replaces all occurrences of the placeholder variables x and y in term e by the variable z. The type of z (and its placeholders x and y) must be annotated with the usage ω. For instance, here is a type tree for the term z + z.

\overline{Var}

x : Int^{ω} ⊢_{Θ} x : Int^{ω}

\overline{Var}

y : Int^{ω} ⊢_{Θ} y : Int^{ω}

\overline{Plus}

x : Int^{ω}, y : Int^{ω} ⊢_{Θ} x + y : Int^{j}

\overline{Cont}

z : Int^{ω} ⊢_{Θ} z + z : Int^{j}

As one would expect, the variable z has use ω. The use variable j on the result type may be instantiated to 1 or ω, depending on how the result of the addition is used.

If a variable is never used, this is indicated by the presence of the structural rule weakening (Weak). This rule places no constraints on the use, since the use 1 (at most once) and the use ω (any number of times) are both compatible with not being used at all. However, the weakening rule may be helpful in devising a type system for strictness analysis, and is certainly important in usage analysis for call-by-value languages (see Section 7).

The last structural rule, exchange (Exch), simply indicates that the order of bindings in a context is irrelevant.

The contraction, weakening, and exchange rules are not syntax directed, but do not pose an impediment to the existence of principal types since it easy to devise an algorithm which determines whether contraction or weakening must be used on each variable, placing these rules as close to the root of the type tree as possible.

A subtlety in the manipulation of contexts is revealed by the Case rule. In the Case rule, the term e_{1} is always evaluated, and then either e_{2} or e_{3} is evaluated. Hence it makes sense to type e_{1} in a different context from e_{2} and e_{3}, but to type e_{2} and e_{3} in the same context. For instance, the following is a valid typing.

x : Int^{1}, xs : [Int^{1}]^{1} ⊢_{Θ}
case xs of {nil → x; cons y ys → x + y} : Int^{1}

Although x appears twice in the term, it is only labelled as being used once, which is correct because only one branch of the ‘case’ term will ever be evaluated.

3.6 Term rules

In rule Abs, the constraint κ ≤_{Θ} |Γ| reflects the fact that if a function abstraction may be accessed more than once, then every free variable of that abstraction may be accessed more than once.

Consider again Example 3 from the introduction.

let x = 1 + 2 in

\begin{matrix}let f = λz. x + z in \\ f 3 + f 4 \end{matrix}

Since f appears twice in f 3 + f 4 it has use ω. Since x is a free variable of a lambda abstraction with use ω, it is in turn forced to have use ω. Thus, despite appearing only once in the term, x must be labelled with use ω, as indeed it should be since it will be accessed twice in the course of evaluation.

In the following example, we do not know how many times the abstraction λz. x + z will be used (since such usage information is, in general, a property of the enclosing program). Fortunately, we can give λz. x + z usage j, where j is a use variable which can be instantiated to either 1 or ω at some later point in the analysis.

x : Int^{k} ⊢_{Θ} λz. x + z : Int^{1} →^{j} Int^{1}, Θ = {j ≤ {k}}

In the above example, the usage variables j and k are not independent, since setting j to ω should force k to be ω (x will certainly be used many times if the abstraction is). The constraint set Θ records this dependency, allowing us to satisfy the constraint κ ≤_{Θ} |Γ| in the Abs rule without (prematurely) instantiating j and k.

Consider the following example, where the term ‘cons x y’ is used twice.

let l = cons x y in case l of ⋯ case l of ⋯

Our typing rules give ‘consxy’ the type [a^{ω}]^{ω} which in turn forces x to have type a^{ω} and y to have type [a^{ω}]^{ω} as expected, since both x and y may be accessed twice. Note that the Nil and Cons rules implicitly include the condition κ ≤_{Θ} |τ| because of our global well-formedness condition on list types (see Section 3.2).

The Plus rule deserves some explanation. Our addition operator is strict, so the result of evaluating e_{1} + e_{2} will simply be an integer constant which will not refer to any part of the results of evaluating e_{1} and e_{2}. Therefore, the usage assigned to the expression e_{1} + e_{2} need not depend at all on the usages κ_{1} and κ_{2}. A similar argument applies to the App rule, since application is strict in its first argument.

3.7 Recursion

The Let rule captures both recursive and non-recursive definitions. It checks (in parallel) that the expressions e_{1}, …, e_{n} have type τ_{1}, …, τ_{n} and the expression e has type τ (in a context where x_{1}, …, x_{n} have type τ_{1}, …, τ_{n}). Clearly, either e_{1}, …, e_{n} or e can use the let-bound variables x_{1}, …, x_{n}.

In the following example, only the body of the let-expression uses x, and we can therefore give x usage 1.

let x = (cons y nil) in (case x of …)

It is necessary to typecheck the let-bound expressions e_{1}, …, e_{n} and the body e in parallel so that multiple uses of let-bound variables are caught by the Cont rule. For example, x is assigned use ω in the following (recursive) let-expression:

let x = (cons y x) in (case x of …)

Mutually-recursive let-expressions behave similarly. For example, x is assigned use ω in the following let-expression, since it appears once in the body and once in the term ‘consq x’. This in turn forces y to have use ω, since y has the same type as x.

let x = (cons p y), y = (cons q x) in (case x of …)

Note that it is not the case that whenever recursion is involved all uses must degenerate to ω. If a function is defined recursively, the argument and result of the function may still have use 1. For example, here is a function to append two lists.

let append = λxs. λzs. case xs of { nil → zs cons y ys → let as = append ys zs in cons y as}

in ⋯ append ⋯

It has the following (principal) type

[a^{j}]^{k} →^{ω} [a^{j}]^{l} →^{m} [a^{j}]^{l}, k ≤ {j}, l ≤ {j}, m ≤ {k}

The constraints k ≤ {j} and l ≤ {j} are generated by our global well-formedness condition on list types, and indicate that if the argument or result lists are accessed more than once, then the elements of those lists may also be accessed more than once. The constraint m ≤ {k} is generated by the Abs rule, and indicates that if append is partially applied and then used more than once, the first argument list may be accessed more than once.

One instance of the above type is

[Int^{ω}]^{ω} →^{ω} [Int^{ω}]^{ω} →^{ω} [Int^{ω}]^{ω}

indicating that append can take two lists to which there may be multiple pointers, and return a list to which there may be multiple pointers. Another instance is

[Int^{1}]^{1} →^{ω} [Int^{1}]^{1} →^{1} [Int^{1}]^{1}

indicating that append may be applied multiple times to two lists to each of which there is only one pointer, returning a list to which there is only one pointer. (Attaching the use 1 to the second arrow guarantees that one cannot create extra pointers to the first argument list by creating and duplicating a partial application.) For this version of append it is possible to generate code that reuses the ‘cons’ cells of the first argument in producing the result.

3.8 Typeability

The ordinary rules for simply typed lambda calculus can be derived by simply omitting all use annotations and use constraints from the rules given here. It follows that if a term is typeable in this system, it is typeable in simply typed lambda calculus. Conversely, if a term is typeable in simply typed lambda calculus, then it is also typeable in this system (just take all uses to be ω).

4 Syntax-directed typing rules

In Figure 2 we present a syntax-directed version of our typing rules. The syntax-directed rules are significantly simpler to reason about in proofs, and give a much clearer intuition as to how type inference can be implemented. Surprisingly, the syntax-directed typing rules are more compact than the original rules.

The syntax-directed typing rules make heavy use of three operations on contexts, Γ × Δ, Γ + Δ and Γ − Δ, which we define below. We assume that the entries in Γ and Δ are given in some canonical order, thereby substantially simplifying our definitions of ×, + and −.

The operation Γ × Δ combines the contexts Γ and Δ so that the types of any variables which are used in both Γ and Δ are forced to have use ω. In terms of the original typing rules, the × operation is a combination of the contraction rule and context concatenation.

()  × Δ  = Δ
(Γ, x : τ) × (Δ, x : τ) = (Γ × Δ), x : τ |τ| = ω
(Γ, x : τ) × Δ  = (Γ × Δ), x : τ x ∉ Δ

The operation Γ + Δ combines the contexts Γ and Δ, placing no constraints on usages. The operation Γ+Δ is only defined whenever the types of all variables in Γ agree with those present in Δ.

()  + Δ  = Δ
(Γ, x : τ) + (Δ, x : τ) = (Γ + Δ), x : τ
(Γ, x : τ) + Δ  = (Γ + Δ), x : τ x ∉ Δ

The operation Γ − Δ removes Δ from Γ, placing no constraints on usages. The operation Γ − Δ is only defined whenever the types of all variables in Γ agree with those present in Δ.

()  − Δ  = ()
(Γ, x : τ) − (Δ, x : τ) = Γ − Δ
(Γ, x : τ) − Δ  = (Γ − Δ), x : τ x ∉ Δ

The following propositions relate the syntax-directed rules with the original typing rules.

Proposition 4.0.1 (Soundness of ▷_{Θ}) If Γ ▷_{Θ} e : τ then Γ ⊢_{Θ} e : τ.

Proof We use induction on the structure of e. We only show the Abs, Plus and Let cases, since the other cases are similar. case Γ − x : τ ▷_{Θ} λx. e : τ →^{κ} τ′ where Γ ▷_{Θ} e : τ′ and κ ≤_{Θ} |Γ − x : τ|

We have, using induction, that Γ ⊢_{Θ} e : τ′. It is easy to show, using induction on the length of Γ, that (Γ − x : τ), x : τ ⊢_{Θ} e : τ′ (the fact that Γ − x : τ is well-defined ensures that we can apply the Weak rule as many times as necessary). The result follows immediately, using the Abs rule.

case Γ_{1} × Γ_{2} ▷_{Θ} e_{1} + e_{2} : Int^{κ} where Γ_{1} ▷_{Θ} e_{1} : Int^{κ_{1}} and Γ_{2} ▷_{Θ} e_{2} : Int^{κ_{2}}

We have, using induction, that Γ_{1} ⊢_{Θ} e_{1} : Int^{κ_{1}} and Γ_{2} ⊢_{Θ} e_{2} : Int^{κ_{2}}. It is easy to show, using induction on the length of Γ_{1}, that Γ_{1} × Γ_{2} ⊢_{Θ} e_{1} + e_{2} : Int^{κ} as required (the fact that Γ_{1} × Γ_{2} is well-defined ensures that we can apply the Cont rule as many times as necessary).

case (Γ_{1} × ⋯ × Γ_{n} × Δ) − (x_{1} : τ_{1}, …, x_{n} : τ_{n}) ▷_{Θ} let x_{1} = e_{1}, …, x_{n} = e_{n} in e : τ where Γ_{1} ▷_{Θ} e_{1} : τ_{1} and … and Γ_{n} ▷_{Θ} e_{n} : τ_{n} and Δ ▷_{Θ} e : τ

We have, using induction, that Δ ⊢_{Θ} e : τ and Γ_{i} ⊢_{Θ} e_{i} : τ_{i} for 1 ≤ i ≤ n. Thus, using induction on the sum of the lengths of Γ_{1}, …, Γ_{n} and Δ we can prove that Γ_{1} × ⋯ × Γ_{n} × Δ ⊢_{Θ} \overline{e}, e : \overline{τ}, τ (by applying the Comb and Cont rules). A similar induction on the length of Γ_{1} × ⋯ × Γ_{n} × Δ proves that (Γ_{1} × ⋯ × Γ_{n} × Δ − (x_{1} : τ_{1}, …, x_{n} : τ_{n})), x_{1} : τ_{1}, …, x_{n} : τ_{n} ⊢_{Θ} \overline{e}, e : \overline{τ}, τ. The result follows using the Let rule. □

Before proving that the syntax-directed rules are complete, we prove the following lemmas about contraction. (We say that Γ ⊆ Δ if there exists a context Γ′ such that Γ, Γ′ = Δ.)

Lemma 4.0.2 (Contraction) If Δ ⊆ Γ, x : τ, y : τ and Δ ▷_{Θ} e : τ and |τ| = ω then there exists a Δ′ ⊆ Γ, z : τ such that Δ′ ▷_{Θ} [z/x, z/y]e : τ.

Proof A simple induction on the structure of e. □

Proposition 4.0.3 (Completeness of ▷_{Θ}) If Γ ⊢_{Θ} e_{1}, …, e_{n} : τ_{1}, …, τ_{n} then there exist Δ_{1}, …, Δ_{n} such that Δ_{i} ▷_{Θ} e_{i} : τ_{i} for 1 ≤ i ≤ n and Δ_{1} × … × Δ_{n} ⊆ Γ.

Proof We use induction on the depth of the derivation of Γ ⊢_{Θ} \overline{e} : \overline{τ}. We just give some representative cases below.

case Γ, z : τ ⊢_{Θ} [z/x, z/y]\overline{e} : \overline{τ} where Γ, x : τ, y : τ ⊢_{Θ} \overline{e} : \overline{τ}

Using induction, we have that there exist Δ_{1}, …, Δ_{n} such that Δ_{i} ▷_{Θ} e_{i} : τ_{i} and Δ_{1} ×…× Δ_{n} ⊆ Γ, x : τ, y : τ. Clearly, Δ_{i} ⊆ Γ, x : τ, y : τ for each i, so we can use Lemma 4.0.2 to show that there exists a Δ′_{i} ⊆ Γ, z : τ such that Δ′_{i} ▷_{Θ} [z/x, z/y]e_{i} : τ_{i}. The result follows since Δ′_{1} × … × Δ′_{n} ⊆ Γ, z : τ. case Γ ⊢_{Θ} λx. e : τ →^{κ} τ′ where Γ, x : τ ⊢_{Θ} e : τ′ and κ ≤_{Θ} |Γ|

Using induction, we have that there exists a Δ ⊆ Γ, x : τ such that Δ ▷_{Θ} e : τ′. This clearly implies that Δ − x : τ is well-defined and Δ − x : τ ⊆ Γ. The result follows since κ ≤_{Θ} |Γ| implies that κ ≤ |Δ − x : τ|.

case Γ_{1}, Γ_{2} ⊢_{Θ} e x : τ′ where Γ_{1} ⊢_{Θ} e : τ →^{κ} τ′ and Γ_{2} ⊢_{Θ} x : τ

We have, using induction, that there exist Δ_{1} ⊆ Γ_{1} and Δ_{2} ⊆ Γ_{2} such that Δ_{1} ▷_{Θ} e : τ →^{κ} τ′ and Δ_{2} ▷_{Θ} x : τ. In fact, it must be the case that Δ_{2} = x : τ. Now, since the concatenation Γ_{1}, Γ_{2} is well-formed, it cannot be the case that x is mentioned in Δ_{1} so we therefore have that Δ_{1} × x : τ = Δ_{1}, x : τ and the result follows since Δ_{1}, x : τ ⊆ Γ_{1}, Γ_{2}.

case Γ ⊢_{Θ} let x_{1} = e_{1}, …, x_{n} = e_{n} in e : τ where Γ, x_{1} : τ_{1}, …, x_{n} : τ_{n} ⊢_{Θ} e_{1}, …, e_{n}, e : τ_{1}, …, τ_{n}, τ

Using induction, we have that there exist Δ_{1}, …, Δ_{n} and Δ such that Δ_{i} ▷_{Θ} e_{i} : τ_{i}, Δ ▷_{Θ} e : τ and Δ_{1} × … × Δ_{n} × Δ ⊆ Γ, x_{1} : τ_{1}, …, x_{n} : τ_{n}. This clearly implies that (Δ_{1} × … × Δ_{n} × Δ) − (x_{1} : τ_{1}, …, x_{n} : τ_{n}) is well-defined and smaller than Γ. The result follows immediately using the Let rule. □

5 Principal types and polymorphism

Before discussing what it means for a type to be principal for a given term, we first need to define when a type is an instance of another type. Our definition of instantiation is closely related to Mitchell’s definition of instantiation for a type system with simple subtypes [Mit84, Mit91].

5.1 Instantiation

A substitution is a pair of finite maps. One component maps type variables to types, while the other maps use variables to uses. Whenever a type variable is replaced by a type, the new type must have the same usage: for each (a_{i}^{κ_{i}} ↦ τ_{i}) ∈ S we require that S(κ_{i}) = |τ_{i}|.

Type substitutions TS ::= {a_{1}^{κ_{1}} ↦ τ_{1}, …, a_{n}^{κ_{n}} ↦ τ_{n}}
Use substitutions US ::= {k_{1} ↦ κ_{1}, …, k_{n} ↦ κ_{n}}
Substitutions  S ::= (TS, US)

We can derive an instance of the typing Γ ⊢_{Θ} e : τ by applying a substitution S to Γ and τ, and replacing Θ with a stronger constraint set Θ′. The behaviour of S on types and contexts is defined in the usual way. We define the conditions under which Θ′ is stronger than Θ (under the substitution S) below.

Θ′ ⊧ SΘ iff for each (j ≤ {k_{1}, …, k_{n}}) ∈ Θ we have that S(j) ≤_{Θ′} S(k_{i}) for each i.

A straightforward induction on the structure of typing derivations proves the following substitution lemma.

Lemma 5.1.1 (Type substitution) If Γ ⊢_{Θ} e : τ and Θ′ ⊧ SΘ then SΓ ⊢_{Θ′} e : Sτ.

5.2 Unification

It is easy to modify Robinson’s unification algorithm [Rob65] so that it unifies types containing usage information. However, whenever we unify a usage variable with another usage, we need to update the current constraint set. Suppose Θ is the following constraint set:

j ≤ {l}, k ≤ {m}, l ≤ {m}, m ≤ {}

If we unify the types a^{j} and Int^{k} we get the substitution:

({a^{j} ↦ Int^{k}}, {j ↦ k})

Since we have unified j and k, we must modify the constraint set Θ so that it merges the constraints for j and k:

k ≤ {l, m}, l ≤ {m}, m ≤ {}

Alternatively, if we unify the types a^{j} and Int^{ω} we get the substitution:

({a^{j} ↦ Int^{ω}}, {j ↦ ω})

We have instantiated j to ω, which in turn forces us to also instantiate l and m to ω. The constraint k ≤ {m} then simplifies to k ≤ {ω}, which can be eliminated, since ω is the maximal usage.

If we unify usage variables with other usage variables, or with ω, we can always derive a new constraint set, as explained above. We can only fail to produce a new constraint set if we unify use variables with 1 (for instance, we might unify j with ω and l with 1, generating the unsatisfiable constraint ω ≤ 1). Fortunately, it is easy to show that during type inference we never generate such constraints.

We say that a substitution S solves a set of equations E if Sτ = Sτ′ for all (τ, τ′) ∈ E. We will not give an algorithm for Unify, but state the following Lemma’s as properties of the algorithm.

Lemma 5.2.1 (Correctness of Unify) If Unify(E) = S then S solves E.

Lemma 5.2.2 (Principality of Unify) If S solves E then Unify(E) succeeds, returning R, and there exists a substitution R′ such that S = R′ ∘ R.

5.3 Principal types

We now present a type inference algorithm reflecting the syntax directed rules of figure 2. First we present the ⊗, ⊕ and ⊖ operators, which are operational versions of the ×, + and − operations. Each operation takes two contexts as arguments, and returns a pair of a new context and a set of equations between types.

\overline{() ⊗ Γ = Γ, \{\}}  \frac{Γ_{1} ⊗ Γ_{2} = Δ, E  x ∉ Γ_{2}}{(Γ_{1}, x : τ) ⊗ Γ_{2} = (Δ, x : τ), E}

\frac{Γ_{1} ⊗ Γ_{2} = Δ, E a fresh}{(Γ_{1}, x : τ_{1}) ⊗ (Γ_{2}, x : τ_{2}) = (Δ, x : τ_{1}), E ∪ \{(τ_{1}, τ_{2}), (τ_{1}, a^{ω})\}}

The following properties follow easily from the definition of ⊗.

Lemma 5.3.1 (Correctness of ⊗) If Γ_{1} ⊗ Γ_{2} = Δ, E and S solves E then SΓ_{1} × SΓ_{2} is well defined and equal to SΔ.

Lemma 5.3.2 (Principality of ⊗) If Dom(S_{1}) ∩ Dom(S_{2}) = ∅ and S_{1}Γ_{1} × S_{2}Γ_{2} = Γ then Γ_{1} ⊗ Γ_{2} = (Δ, E), S_{1} ∘ S_{2} solves E and Γ = (S_{1} ∘ S_{2})Δ.

\overline{() ⊕ Γ = Γ, \{\}}  \frac{Γ_{1} ⊕ Γ_{2} = Δ, E  x ∉ Γ_{2}}{(Γ_{1}, x : τ) ⊕ Γ_{2} = (Δ, x : τ), E}

\frac{Γ_{1} ⊕ Γ_{2} = Δ, E}{(Γ_{1}, x : τ_{1}) ⊕ (Γ_{2}, x : τ_{2}) = (Δ, x : τ_{1}), E ∪ \{(τ_{1}, τ_{2})\}}

The following properties follow easily from the definition of ⊕.

Lemma 5.3.3 (Correctness of ⊕) If Γ_{1} ⊕ Γ_{2} = Δ, E and S solves E then SΓ_{1} + SΓ_{2} is well defined and equal to SΔ.

Lemma 5.3.4 (Principality of ⊕) If Dom(S_{1}) ∩ Dom(S_{2}) = ∅ and S_{1}Γ_{1} + S_{2}Γ_{2} = Γ then Γ_{1} ⊕ Γ_{2} = (Δ, E), S_{1} ∘ S_{2} solves E and Γ = (S_{1} ∘ S_{2})Δ.

\overline{() ⊖ Γ = (), \{\}}  \frac{Γ_{1} ⊖ Γ_{2} = Δ, E  x ∉ Γ_{2}}{(Γ_{1}, x : τ) ⊖ Γ_{2} = (Δ, x : τ), E}

\frac{Γ_{1} ⊖ Γ_{2} = Δ, E}{(Γ_{1}, x : τ_{1}) ⊖ (Γ_{2}, x : τ_{2}) = Δ, E ∪ \{(τ_{1}, τ_{2})\}}

The following properties follow easily from the definition of ⊖.

Lemma 5.3.5 (Correctness of ⊖) If Γ_{1} ⊖ Γ_{2} = Δ, E and S solves E then SΓ_{1} − SΓ_{2} is well defined and equal to SΔ.

Lemma 5.3.6 (Principality of ⊖) If Dom(S_{1}) ∩ Dom(S_{2}) = ∅ and S_{1}Γ_{1} − S_{2}Γ_{2} = Γ then Γ_{1} ⊖ Γ_{2} = (Δ, E), S_{1} ∘ S_{2} solves E and Γ = (S_{1} ∘ S_{2})Δ.

For convenience, we allow the ⊗, ⊕ and ⊖ operators to be composed. For example, the expression Γ_{1} ⊗(Γ_{2} ⊕Γ_{3}) denotes (Δ′, E ∪E′) where Γ_{2} ⊕Γ_{3} = (Δ, E) and Γ_{1} ⊗Δ = (Δ′, E′). Similarly, Γ_{1} ⊗…⊗Γ_{n} = Δ_{n}, (E_{1} ∪…∪E_{n}) where Δ_{1} = Γ_{1}, E_{1} = {} and Δ_{i−1} ⊗Γ_{i} = Δ_{i}, E_{i} for 2 ≤ i ≤ n.

We now present our type inference algorithm which, given an expression, computes the most general Γ, Θ and τ such that Γ ⊢_{Θ} e : τ. We assume that each recursive call returns a result which contains type and use variables distinct from any other recursive call.

\frac{a, j fresh}{e ≻ (\{x : a^{j}\}, \{\}, a^{j})}

\frac{e ≻ (Γ, Θ, τ) Γ ⊖ (x : a^{j}) = (Δ, E) Unify(E) = S a, j, k fresh}{λx. e ≻ (SΔ, S(Θ ∪ \{k ≤ |Γ|\}), S(a^{j} →^{k} τ))}

\frac{e ≻ (Γ, Θ, τ) Γ ⊗ (x : a^{j}) = (Δ, E) Unify(E ∪ \{(τ, a^{j} →^{k} b^{l})\}) = S a, b, j, k, l fresh}{e x ≻ (SΔ, SΘ, S(b^{l}))}

\frac{j fresh}{n ≻ ((), \{\}, Int^{j})}

\frac{e_{1} ≻ (Γ_{1}, Θ_{1}, τ_{1}) e_{2} ≻ (Γ_{2}, Θ_{2}, τ_{2}) Γ_{1} ⊗ Γ_{2} = (Δ, E) Unify(E ∪ \{(τ_{1}, Int^{j_{1}}), (τ_{2}, Int^{j_{2}})\}) = S k, j_{1}, j_{2} fresh}{e_{1} + e_{2} ≻ (SΔ, SΘ_{1} ∪ SΘ_{2}, Int^{k})}

\frac{a, j, k fresh}{nil ≻ ((), \{k ≤ \{j\}\}, [a^{j}]^{k})}

\frac{a, j, k fresh}{cons x y ≻ ((x : a^{j}, y : [a^{j}]^{k}), \{k ≤ \{j\}\}, [a^{j}]^{k})}

\frac{e_{1} ≻ (Γ_{1}, Θ_{1}, τ_{1}) e_{2} ≻ (Γ_{2}, Θ_{2}, τ_{2}) e_{3} ≻ (Γ_{3}, Θ_{3}, τ_{3}) Γ_{1} ⊗ (Γ_{2} ⊕ (Γ_{3} ⊖ (x : a^{j}, y : [a^{j}]^{k}))) = (Δ, E) Unify(E ∪ \{(τ_{1}, [a^{j}]^{k}), (τ_{2}, τ_{3})\}) = S}{case e_{1} of \{nil → e_{2}; cons x y → e_{3}\} ≻ (SΔ, S(Θ_{1} ∪ Θ_{2} ∪ Θ_{3} ∪ \{k ≤ \{j\}\}), Sτ_{2})}

\frac{e_{1} ≻ (Γ_{1}, Θ_{1}, τ_{1})  …  e_{n} ≻ (Γ_{n}, Θ_{n}, τ_{n}) e ≻ (Γ, Θ, τ) (Γ_{1} ⊗ … ⊗ Γ_{n}) ⊖ (x_{1} : τ_{1}, …, x_{n} : τ_{n}) = (Δ, E) Unify(E) = S}{let x_{1} = e_{1}, …, x_{n} = e_{n} in e ≻ (SΔ, S(Θ_{1} ∪ ⋯ ∪ Θ_{n} ∪ Θ), Sτ)}

Proposition 5.3.7 (Correctness: ▷_{Θ}) If e ≻ (Γ, Θ, τ) then Γ ▷_{Θ} e : τ.

Proof We use induction on the depth of the inference of e ≻ (Γ, Θ, τ). We just give some representative cases below.

case e x ≻ (SΔ, SΘ, S(b^{l})) where e ≻ (Γ, Θ, τ), Γ ⊗ (x : a^{j}) = (Δ, E), Unify(E ∪ {(τ, a^{j} →^{k} b^{l})}) = S and a, b, j, k, l fresh

We have, by induction, that Γ ▷_{Θ} e : τ. Using Lemma 5.2.1 we have that S solves E ∪ {(τ, a^{j} →^{k} b^{l})}. We therefore have, using Lemma 5.3.1, that SΓ × S(x : a^{j}) is welldefined and equal to SΔ. Now, using Lemma 5.1.1, we have that SΓ ▷_{SΘ} e : Sτ where Sτ = S(a^{j}) →^{Sk} S(b^{l}), so we can use the App rule to prove that SΓ ▷_{SΘ} e x : S(b^{l}) as required.

case λx. e ≻ (SΔ, S(Θ ∪ {k ≤ |Γ|}), S(a^{j} →^{k} τ)) where e ≻ (Γ, Θ, τ), Γ ⊖ (x : a^{j}) = (Δ, E), Unify(E) = S and a, j, k fresh

We have, by induction, that Γ ▷_{Θ} e : τ. Using Lemma 5.2.1 we have that S solves E. We therefore have, using Lemma 5.3.5, that SΓ − S(x : a^{j}) is well-defined and equal to SΔ. Now, it is clear that S(Θ ∪ {k ≤ |Γ|}) ⊧ SΘ so we have, using Lemma 5.1.1, that SΓ▷_{SΘ}e : Sτ and we can use the Abs rule to prove that SΓ▷_{S(Θ∪{k≤|Γ|})}λx. e : S(a^{j} →^{k} τ) as required.

case e_{1} + e_{2} ≻ (SΔ, SΘ_{1} ∪ SΘ_{2}, Int^{k}) where e_{1} ≻ (Γ_{1}, Θ_{1}, τ_{1}), e_{2} ≻ (Γ_{2}, Θ_{2}, τ_{2}), Γ_{1} ⊗ Γ_{2} = (Δ, E), Unify(E ∪ {(τ_{1}, Int^{j_{1}}), (τ_{2}, Int^{j_{2}})}) = S and k, j_{1}, j_{2} fresh

We have, by induction, that Γ_{1} ▷_{Θ_{1}} e_{1} : τ_{1} and Γ_{2} ▷_{Θ_{2}} e_{2} : τ_{2}. Using Lemma 5.2.1 we have that S solves E ∪ {(τ_{1}, Int^{j_{1}}), (τ_{2}, Int^{j_{2}})}. We therefore have, using Lemma 5.3.1, that SΓ_{1} × SΓ_{2} is well-defined and equal to SΔ. Now, it is clear that S(Θ_{1} ∪ Θ_{2}) ⊧ SΘ_{i} for i = 1, 2 so we have, using Lemma 5.1.1, that SΓ_{1} ▷_{S(Θ_{1}∪Θ_{2})} e_{1} : Sτ_{1} and SΓ_{2} ▷_{S(Θ_{1}∪Θ_{2})} e_{2} : Sτ_{2} where Sτ_{1} = Int^{Sj_{1}} and Sτ_{2} = Int^{Sj_{2}}. We can therefore use the Plus rule to prove that SΔ ▷_{S(Θ_{1}∪Θ_{2})} e_{1} + e_{2} : Int^{k} as required.

case let x_{1} = e_{1}, …, x_{n} = e_{n} in e ≻ (SΔ, S(Θ_{1} ∪⋯∪Θ_{n} ∪Θ), Sτ) where e_{i} ≻ (Γ_{i}, Θ_{i}, τ_{i}) for 1 ≤ i ≤ n, e ≻ (Γ, Θ, τ), (Γ_{1}⊗…⊗Γ_{n})⊖(x_{1} : τ_{1}, …, x_{n} : τ_{n}) = (Δ, E) and Unify(E) = S

We have, by induction, that Γ_{i} ▷_{Θ_{i}} e_{i} : τ_{i} for 1 ≤ i ≤ n and Γ ▷_{Θ} e : τ. Using Lemma 5.2.1 we have that S solves E. We therefore have, using Lemmas 5.3.1 and 5.3.5, that S(Γ_{1} ⊗ … ⊗ Γ_{n}) ⊖ (x_{1} : τ_{1}, …, x_{n} : τ_{n}) is well-defined and equal to SΔ. Now, it is clear that S(Θ_{1} ∪ … ∪ Θ_{n} ∪ Θ) ⊧ SΘ_{i} for 1 ≤ i ≤ n so we have, using Lemma 5.1.1, that SΓ_{i} ▷_{S(Θ_{1}∪...∪Θ_{n}∪Θ)} e_{i} : τ_{i}. Similarly, we have that SΓ▷_{S(Θ_{1}∪...∪Θ_{n}∪Θ)} e : τ. We can therefore use the Let rule to prove that SΔ ▷_{S(Θ_{1}∪...∪Θ_{n}∪Θ)} let x_{1} = e_{1}, …, x_{n} = e_{n} in e : Sτ as required. □

Proposition 5.3.8 (Principal types: ▷_{Θ}) If Γ ▷_{Θ} e : τ then e ≻ (Γ′, Θ′, τ′) and there exists an S such that SΓ′ = Γ, Sτ′ = τ and Θ ⊧ SΘ′.

Proof We use induction on the depth of the inference of Γ ▷_{Θ} e : τ.

case x : τ ▷_{Θ} x : τ

We have that x ≻ ({x : a^{j}}, a^{j}, { }) where a and j are fresh. Let S be the substitution ({a ↦ τ}, {j ↦ |τ|}). We clearly have that S{x : a^{j}} = x : τ, S(a^{j}) = τ and Θ ⊧ S{ }.

case Γ − x : τ_{1} ▷_{Θ} λx. e : τ_{1} →^{κ} τ_{2} where Γ ▷_{Θ} e : τ_{2} and κ ≤_{Θ} |Γ − x : τ_{1}|

We have, by induction, that e ≻ (Γ′, Θ′, τ′_{2}) and there exists an S such that SΓ′ = Γ, Sτ′_{2} = τ_{2} and Θ ⊧ SΘ′. Now, let S′ = S ∪ ({a ↦ τ_{1}}, {j ↦ |τ_{1}|}) where a and j are fresh. We clearly have that S′Γ′ − S′(x : a^{j}) = Γ − x : τ_{1}, so we can use Lemma 5.3.6 to prove that Γ′ ⊖(x : a^{j}) = (Δ, E) for Δ and E such that S′ solves E and S′Δ = Γ−x : τ_{1}. Now, since S′ solves E, we have using Lemma 5.2.2 that Unify(E) = S′′ and there exists an R such that S′ = R ∘ S′′.

Let Γ′′, Θ′′ and τ′′ be given such that Γ′′ ▷_{Θ′′} λx. e : τ′′. By the type rule, Γ′′ must have the form Γ′′_{0} − x : τ′′_{0} for some τ′′_{0} and τ′′ must have the form τ′′_{0} →^{κ′′} τ′′_{1}.

By the induction hypothesis Infer(e) succeeds returning (Γ′_{0}, Θ′, τ′_{1}) such that there exists S such that SΓ′_{0} = Γ′′_{0}, Sτ′_{1} = τ′′_{1} and Θ′′ ⊧ SΘ′.

Let S′′_{1} = [a^{j} ↦ τ′′_{0}, k ↦ κ′′] (where a, j and k are fresh). Now Γ′′ = SΓ′_{0} − S′′_{1}(x : a^{j}) and Dom(S) ∩ Dom(S′′_{1}) = ∅. From Lemma 5.3.6 we have that Minus(Γ′_{0}, x : a^{j}) succeeds returning (E, Γ′) such that S ∘ S′′_{1} solves E and (S ∘ S′′_{1})Γ′ = SΓ′_{0} − S′′_{1}(x : a^{j}).

Let{k_{0}, …, k_{n}} = {i | y : τ ∈ Γ′, |τ| = i}. Since Θ′′ ⊧ SΘ′ and κ′′ ≤_{Θ′′} |Γ′′_{0} − x : τ′′_{0}| we have Θ′′ ⊧ (S ∘ S′′_{1})(Θ′ ∪ {k ≤ {k_{0}, …, k_{n}}})

From Lemma 5.2.2 we have that Unify(E) succeeds returning S′ and there exists a substitution R such that S ∘ S′′_{1} = R ∘ S′ and Θ′′ ⊧ R(S′(Θ′ ∪ {k ≤ {k_{0}, …, k_{n}}}))

Now Infer(λx. e) succeeds returning (S′Γ′, S′(a^{j} →^{k} τ′_{1}), S′(Θ′ ∪ {k ≤ {k_{0}, …, k_{n}}})) and we have R(S′Γ′) = S(S′′_{1}Γ′) = SΓ′′_{0} − S′′_{1}(x : τ′′_{0}) = Γ′′, R(S′(a^{j} →^{k} τ′_{1})) = S(S′′_{1}(a^{j} →^{k} τ′_{1})) = τ′′_{0} →^{κ′′} τ′′_{1} = τ′′ and Θ′′ ⊧ R(S′(Θ′ ∪ {k ≤ {k_{0}, …, k_{n}}}))

case Γ ⊎ x : τ_{0} ▷_{Θ} e x : τ_{1}

By assumption Γ ▷_{T} e : τ_{0} →^{κ} τ_{1}. Let Γ′′, Θ′′ and τ′′_{1} be given such that Γ′′ ▷_{Θ′′} e x : tau′′_{1}. Clearly Γ′′ must have the form Γ′′_{0} ⊎ x : τ′′_{0}. By the type rule we have Γ′′_{0} ▷_{Θ′′} e : τ′′_{0} →^{κ′′} τ′′_{1} for some κ′′

By the induction hypothesis Infer(e) succeeds returning (Γ′_{0}, Θ′, τ′) such that there exists a substitution S such that SΓ′_{0} = G′′_{0}, Sτ′ = τ′′_{0} →^{κ′′} τ′′_{1} and Θ′′ ⊧ SΘ′.

Let E = {τ′, a^{j} →^{k} b^{l}} where a, j, k, b, l are fresh. Let S′′_{1} be given such that S′′_{1}(a^{j} →^{k} b^{l}) = τ′ (it is clear that such a thing exists). By Lemma 5.3.2 we have that Combine(Γ′_{0}, (x : a^{j})) succeeds returning (E′, Γ′) such that G′′ = SΓ′_{0} ⊎ S′′_{1}(x : a^{j}) and Dom(S) ∩ Dom(S′′_{1}) = ∅ implies S ∘ S′′_{1} solves E′ and (S ∘ S′′_{1})Γ′ = SΓ′_{0} ⊎ S′′_{1}(x : a^{j}).

We clearly have that S ∘S′′_{1} solves E ∪E′. From Lemma 5.2.2 we have that Unify(E ∪E′) succeeds returning S′ and there exists a substitution R such that R ∘ S′ = S ∘ S′′_{1} and Θ′′ ⊧ R(SΘ′).

Now Infer(e x) succeeds returning (S′Γ′, S′(b^{l}), S′Θ′). Want: R(S′Γ′) = S(S′′_{1}Γ′) = SΓ′_{0} ⊎ S′′_{1}(x : a^{j}) = Γ′′_{0} ⊎ x : τ′′_{0} = Γ′′, R(S′(b^{l})) = S(S′′_{1}(b^{l})) = τ′′_{1} and Θ′′ ⊧ R(S′Θ′).

case Γ_{1} ⊎ Γ_{2} ▷_{Θ} e_{1} + e_{2} : Int^{κ} where Γ_{1} ▷_{Θ} e_{1} : Int^{κ_{1}} and Γ_{2} ▷_{Θ} e_{2} : Int^{κ_{2}}

Using induction, we have that Infer(e_{1}) succeeds, returning (Γ′_{1}, Θ′_{1}, τ′_{1}) and for all Γ′′_{1}, Θ′′_{1} and τ′′_{1} such that Γ′′_{1} ▷_{Θ′′_{1}} e_{1} : τ′′_{1} there exists an S_{1} such that S_{1}Γ′_{1} = Γ′′_{1}, S_{1}τ′_{1} = τ′′_{1} and Θ′′_{1} ⊧ S_{1}Θ′_{1}. Similarly Infer(e_{2}) succeeds, returning (Γ′_{2}, Θ′_{2}, τ′_{2}) and for all Γ′′_{2}, Θ′′_{2} and τ′′_{2} such that Γ′′_{2} ▷_{Θ′′_{2}} e_{2} : τ′′_{2} there exists an S_{2} such that S_{2}Γ′_{2} = Γ′′_{2}, S_{2}τ′_{2} = τ′′_{2} and Θ′′_{2} ⊧ S_{2}Θ′_{2}.

Let Γ′′, Θ′′ and τ′′ such that Γ′′ ▷_{Θ′′} e_{0} + e_{0} : τ′′ be given. We have τ′′ = Int^{κ} and Γ′′ = Γ′′_{0} ⊎ Γ′′_{1} by the type rule. Further we have S_{0}, S_{1} such that Γ′′ = S_{0}Γ′_{0} ⊎ S_{1}Γ′_{1}.

Let E = {(τ_{0}, Int^{j_{0}}), (τ_{1}, Int^{j_{1}})} where τ_{0} = Int^{κ_{0}} and τ_{1} = Int^{κ_{1}}. Then S_{0} ∘ S_{1} ∘ {j_{0} ↦ κ_{0}, j_{1} ↦ κ_{1}} solves E.

By Lemma 5.3.2 we have that Combine(Γ′_{0}, Γ′_{1}) succeeds returning (E′, Γ) such that S_{0}∘S_{1} solves E′ and S_{0} ∘ S_{1}(Γ) = S_{0}Γ′_{0} ⊎ S_{1}Γ′_{1}. Clearly this implies S_{0} ∘ S_{1} ∘ {j_{0} ↦ κ_{0}, j_{1} ↦ κ_{1}} solves E′ and S_{0} ∘ S_{1} ∘ {j_{0} ↦ κ_{0}, j_{1} ↦ κ_{1}}(Γ) = S_{0}Γ′_{0} ⊎ S_{1}Γ′_{1} and finally S_{0} ∘ S_{1} ∘ {j_{0} ↦ κ_{0}, j_{1} ↦ κ_{1}} solves (E ∪ E′).

From (S_{0} ∘ S_{1} ∘ {j_{0} ↦ κ_{0}, j_{1} ↦ κ_{1}})(Θ′_{0} ∪ Θ′_{1}) = (S_{0} ∘ S_{1})(Θ′_{0} ∪ Θ′_{1}) = S_{0}(Θ′_{0}) ∪ S_{1}(Θ′_{1}) and the fact that Θ′′ ⊧ S_{0}(Θ′_{0}) and Θ′′ ⊧ S_{1}(Θ′_{1}) we conclude that Θ′′ ⊧ (S_{0} ∘ S_{1} ∘ {j_{0} ↦ κ_{0}, j_{1} ↦ κ_{1}})(Θ′_{0} ∪ Θ′_{1})

Now by Lemma 5.2.2 we have that Unify(E ∪ E′) succeeds returning S and there exists a substitution R such that S_{0} ∘ S_{1} ∘ {j_{0} ↦ κ_{0}, j_{1} ↦ κ_{1}} = R ∘ S and Θ′′ ⊧ R(S(Θ′_{0} ∪ Θ′_{1})).

Now Infer(Γ_{0} ⊎ Γ_{1} ▷_{Θ} e_{0} + e_{1} : Int^{κ}) succeeds returning (SΓ, Int^{k}, S(Θ_{0} ∪ Θ_{1})). We now check that (R ∘ {k ↦ κ}) is the substitution we are looking for:

(R ∘ {k ↦ κ})(S(Γ)) = S_{0} ∘ S_{1} ∘ {j_{0} ↦ κ_{0}, j_{1} ↦ κ_{1}}(Γ)
= S_{0}Γ′_{0} ⊎ S_{1}Γ′_{1}
= Γ′′
(R ∘ {k ↦ κ})Int^{k} = Int^{κ}
Θ′′ ⊧ (R ∘ {k ↦ κ})(S(Θ′_{0} ∪ Θ′_{1}))

case Γ_{1} ⊎ (Γ_{2} + (Γ_{3} − (x : τ, y : [τ]^{κ}))) ▷_{Θ} case e_{1} of {nil → e_{2}; cons x y → e_{3}} : τ′

case (Γ_{1} ⊎ ⋯ ⊎ Γ_{n} ⊎ Δ) − (x_{1} : τ_{1}, …, x_{n} : τ_{n}) ▷_{Θ} let x_{1} = e_{1}, …, x_{n} = e_{n} in e : τ

□

The following propositions are obvious corollaries of Proposition 5.3.7, Proposition 5.3.8, Proposition 4.0.1 and Proposition 4.0.3.

Proposition 5.3.9 (Correctness: ⊢_{Θ}) If Infer(e) = (Γ, Θ, τ) then Γ ⊢_{Θ} e : τ.

Proposition 5.3.10 (Principal types: ⊢_{Θ}) If Γ ⊢_{Θ} e : τ then Infer(e) succeeds, returning (Γ′, Θ′, τ′) and for all Γ′′, Θ′′ and τ′′ such that Γ′′ ⊢_{Θ′′} e : τ′′ there exists an S such that SΓ′ ⊆ Γ′′, Sτ′ = τ′′ and Θ′′ ⊧ SΘ′.

5.4 Inferring usage annotations

The operational semantics of Section 2 and the reduction rules of Section 6 require that each let-bound variable x is annotated with a use |x| which is either 1 or ω. Such annotations may be inferred as follows. First, determine a principal typing for the given term, and a corresponding principal type derivation. One component of the principal typing is a constraint set Θ, which may be instantiated using any substitution S such that {} ⊧ SΘ. Naturally, we choose the substitution that maps each use variable to 1, since this yields the best usage information. One can now extract the relevant usage information from the (instantiated) type derivation.

5.5 Polymorphism

The next step is to use ‘let’ terms to introduce polymorphism in the usual way. There are two possibilities. The first is to allow polymorphism only on type variables. For instance, the polymorphic type for append would be

∀a^{j}. [a^{j}]^{k} →^{ω} [a^{j}]^{l} →^{m} [a^{j}]^{l}

with the same constraints as before. This allows append to be used on lists of different types, but every occurrence of append in the program must have the same usage labelling. Although crude, an analysis of this sort may be suitable for some purposes, such as update analysis. An existing update analyser, based on abstract interpretation, has a similar limitation but has proved reasonably effective [Mar93].

The second possibility is to allow polymorphism on both type and use variables. For instance, the polymorphic type for append would be

\begin{matrix}∀j. ∀k ≤ \{j\}. ∀l ≤ \{j\}. ∀m ≤ \{k\}. \\ ∀a^{j}. [a^{j}]^{k} →^{ω} [a^{j}]^{l} →^{m} [a^{j}]^{l} \end{matrix}

In order to maximise the potential for optimisation, the compiler needs to generate different versions of append for different instantiations of the use variables. A similar technique is used in Haskell compilers to specialise code involving overloaded functions, and experience to date suggests that this is feasible and does not necessarily lead to an explosion in code size [Aug93, Jon93]. In some situations, instead of specialising append for different uses, we might consider having just one version of append, and interpret the use variables j, k, l, m as additional arguments to the append function, enabling run-time selection of the behaviour of append.

The trade-off between these two possibilities is similar to the trade-off between monovariant and polyvariant binding time analysis in partial evaluation. Further experimentation will be necessary to better understand the strengths and weaknesses of each approach.

Type contexts Σ are used to indicate which type variables can be generalised.

Type contexts Σ ::= a_{1}^{κ_{1}}, …, a_{n}^{κ_{n}}

Figure 3 presents the additional type rules — in the monomorphic rules, replace Γ ⊢ e : τ by Γ ⊢_{(Σ; Θ)} e : τ everywhere, and replace ι ≤ κ by ι ≤_{Θ} κ everywhere. The generalisation rules have the usual side condition, that the generalised variable must not occur free in Γ or Θ. Note that the rules are given in sequent style

6 Reduction and subject-reduction

We previously described the semantics of our language using Launchbury’s operational semantics of call-by-need [Lau93]. We now give an alternative characterisation of that semantics using a modification of the call-by-need calculus of Ariola et al. [AFMOW95].

Working in the framework of a calculus with reduction rules simplifies our proof of subject-reduction, but more importantly, gives a set of rules which can be used by a compiler to optimise programs without danger of duplicating work (or returning the wrong result). We show how our usage information enables additional “safe” reduction rules to be formulated, allowing more aggressive optimisation when values are known to be used at most once.

6.1 Reduction rules

In the call-by-need calculus of Ariola et al, a closure is created for the argument of each function application, whereas in Launchbury’s operational semantics only ‘let’ creates closures. This difference is significant: it means that the model of Ariola et al. may create many more closures than the model of Launchbury. For example, consider the following recursive function.

letrec f = λl. λy.
case l of {nil → y; cons x xs → f xs y}
in let l = e_{0} in let y = e_{1} in f l y

Launchbury’s model does not create closures for the arguments (xs and y) to the recursive call of f. The model of Ariola et al. creates two (redundant) closures for these arguments during every recursive call of f.

Fortunately, it is straightforward to adapt the calculus of Ariola et al. so that it corresponds to the model of Launchbury. The required contextual forms are given below, and the reduction rules are given in Figure 4.

The first group of reduction rules are straightforward. Note that the reduction rules of Ariola et al. would reduce the application ‘(λx. e) y’ to ‘let x = y in e’, but our syntactic restriction on application (which forces all arguments to be variables) means that we can easily avoid creating the (redundant) closure for x, and substitute y for x instead.

The second group of rules are a generalisation of the let-floating and garbage collection rules of Ariola et al., which are necessary to guarantee that every closed term can be reduced to a weak head normal form. The Let contexts, defined below, enumerate those positions from which a let-expression can float outwards.

Let contexts L::= [ ] x | let x = [ ] in e | [ ] + e | e + [ ] |
case [ ] of {nil → e_{1}; cons x y → e_{2}}

A context C is a term with a hole. Note that the hole cannot appear in the argument of an application or ‘cons’, since these positions can only contain variables and cannot be replaced by arbitrary terms.

Contexts C ::= [ ] | C x | let x = C in e | let x = e in C |

letrec x = C in e | letrec x = v in C | case C of {nil → e_{1}; cons x y → e_{2}} | C + e | e + C

The key change from the work of Ariola et al. involves the rules that allow substitution of a value.

let x = v in C[x] ⟹ let x = v in C[v], if |x| = ω

The above rule is safe because, since v is already a value, the substitution cannot duplicate computation. However, in order to guarantee that reductions preserve use types, we must restrict this rule to the case where all free variables of v have use ω; otherwise we may duplicate a variable with use 1 resulting in an ill-typed term. An adequate restriction is to require that x has use ω, since this implies that all free variables of v also have use ω, as the reader may easily check (the two important cases are when v is a function abstraction and when v is a ‘cons’).

In the case where x has use 1, we must eliminate the let-expression as soon as we substitute for x (this reduction corresponds to the Var-Once rule in the operational semantics, which avoids updating closures for variables which are used at most once).

let x = v in C[x] ⟹ C[v], if |x| = 1

We take the compatible closure of the rules shown in Figure 4 as our reduction relation. Capture of free variables is disallowed, so context C should not bind x in the three rules containing C, and context L should not have x as a free variable in the two rules containing L.

6.2 Soundness and completeness

If H is a heap, as used in the operational semantics of Section 2, and e is a term then the configuration ⟨H⟩ e corresponds to the term ‘let ⟨H⟩ in e’, defined as follows.

let ⟨x_{1} : e_{1}, …, x_{n} : e_{n}⟩ in e = let x_{1} = e_{1}, …, x_{n} = e_{n} in e

The following lemma does most of the work of proving that the reduction rules capture all of the evaluations possible using the operational semantics. In fact, we do not even need the garbage-collection rules to capture all possible evaluations. Let ⟶ be the reduction relation minus the garbage collection rules. (The following result is clearly false if we replace ⟶ with ⟹, since some let-bindings which appear to be garbage-collectable in let ⟨H⟩ in e might in fact be used in L[e].)

Lemma 6.2.1 (Reduction in a context) If let ⟨H⟩ in e ⟶ let ⟨H′⟩ in e′ then, for all L, let ⟨H⟩ in L[e] ⟶^{∗} let ⟨H′⟩ in L[e′].

Proof A case analysis on the possible reductions proves the result. The “local” reductions (such as application and addition) are easy, since the reduction let ⟨H⟩in e ⟶ let ⟨H′⟩in e′ must occur completely inside either H or e. In the case of the substitution rules, the result follows immediately, since we can simply compose the context C with the let-context L. In the case of the let-floating rules, we need to apply a second let-floating reduction to move the ‘let’ outside of the extra context L. □

We can now prove that the reduction rules are sound and complete with respect to the operational semantics. (We have not checked the soundness proof in detail, but believe that it should be a straightforward adaption of the soundness result proved by Ariola et al.)

Conjecture 6.2.2 (Soundness) If let ⟨H⟩ in e ⟹^{∗} let ⟨H′′⟩ in v′′ then there exist H′ and v′ such that ⟨H⟩ e ⇓ ⟨H′⟩ v′ and let ⟨H′⟩ in v′ ⟹^{∗} let ⟨H′′⟩ in v′′.

Proposition 6.2.3 (Completeness) If ⟨H⟩ e ⇓ ⟨H′⟩ v′ then let ⟨H⟩ in e ⟹^{∗} let ⟨H′⟩ in v′

Proof We use induction on the depth of the inference of ⟨H⟩ e ⇓ ⟨H′⟩ v′. In fact, we prove a slightly stronger conclusion: let ⟨H⟩ in e ⟶^{∗} let ⟨H′⟩ in v′.

case Abs,Int,Nil,Cons,Var-Rec

Immediate.

case App,Case-Nil,Case-Cons

We have, by induction, that let ⟨H_{1}⟩ in e_{1} ⟶^{∗} let ⟨H_{2}⟩ in λx. e_{2}. Using Lemma 6.2.1, we have that let ⟨H_{1}⟩ in e_{1} y ⟶^{∗} let ⟨H_{2}⟩ in (λx. e_{2}) y which reduces in one step to let ⟨H_{2}⟩ in [y/x]e_{2}. The result follows by applying induction again. Similar arguments apply for the Case-Nil and Case-Cons cases.

case Plus

We have, by induction, that let ⟨H_{1}⟩ in e_{1} ⟶^{∗} let ⟨H_{2}⟩ in n_{1} and let ⟨H_{2}⟩ in e_{2} ⟶^{∗} let ⟨H_{3}⟩in n_{2}. Using Lemma 6.2.1, we have that let ⟨H_{1}⟩in e_{1}+e_{2} ⟶^{∗} let ⟨H_{2}⟩in n_{1}+e_{2}. A further application of Lemma 6.2.1 proves that let ⟨H_{2}⟩in n_{1} +e_{2} ⟶^{∗} let ⟨H_{3}⟩in n_{1} + n_{2}, which reduces in one step to the required result. case Let,Letrec

The terms let ⟨H, let x′ = e_{1}⟩ in [x′/x]e_{2} and let ⟨H⟩ in let x = e_{1} in e_{2} are alphaconvertable, and the result follows since reduction is closed under alpha-conversion. A similar argument applies for the Letrec case.

case Var-Once,Var-Many

We have, by induction, that let ⟨H_{1}⟩in e ⟶^{∗} let ⟨H_{2}⟩in v. Using Lemma 6.2.1, we have that let ⟨H_{1}⟩ in let x = e in let ⟨H_{3}⟩ in x ⟶^{∗} let ⟨H_{2}⟩ in let x = v in let ⟨H_{3}⟩ in x, which then reduces in one step to let ⟨H_{2}⟩ in let ⟨H_{3}⟩ in v as required. A similar argument applies to the Var-Many case. □

The soundness and completeness results take an even simpler form for terms of type integer.

Corollary 6.2.4 (Soundness and completeness) There exists a heap H′ such that ⟨H⟩ e ⇓ ⟨H′⟩ n if and only if let ⟨H⟩ in e ⟹^{∗} n.

6.3 Confluence

The following example (S is a constructor) shows that our system does not satisfy the Church-Rosser property (and thus is not confluent). We leave the problem of finding a confluent reduction system for the call-by-need calculus with recursion as a topic for future research.

6.4 Subject Reduction

Lemma 6.4.1 (Value substitution) If Γ ▷_{Θ} C[x] : τ, Γ(x) = τ′, Γ ⊎ Δ is well defined and Δ ▷_{Θ} v : τ′ then there exists Γ′ ⊆ Γ ⊎ Δ such that Γ′ ▷_{Θ} C[v] : τ.

Proof Trivial induction on the structure of C[x]. □

Lemma 6.4.2 (Affine substitution) If Γ ▷_{Θ} e : τ, Γ(x) = τ′, |τ′| = 1, Γ ⊎ Δ is well defined and Δ ▷_{Θ} e′ : τ′ then (Γ − (x : τ′)) ⊎ Δ ▷_{Θ} {e′/x}e : τ.

Proof

Induction over the structure of e. case x

Assume x : τ ▷_{Θ} x : τ, |τ| = 1, (x : τ) ⊎ Δ is well defined and Δ ▷_{Θ} e′ : τ. Then clearly ((x : τ) − (x : τ)) ⊎ Δ ▷_{Θ} {e′/x}x : τ.

case x ≠ y

Does not apply.

case e x

Assume Γ ▷_{Θ} e x : τ, Γ(x) = τ′, |τ′| = 1, Γ ⊎ Δ well defined and Δ ▷_{Θ} e′ : τ′. Now (Γ − (x : τ′)) ⊎ Δ ▷_{Θ} let x = e′ in e x : τ′ by the type rule for ‘Let’ (since |τ′| = 1 and Γ ⊎ Δ is well defined, we have that x does not appear in Δ).

case e y, y ≠ x

Assume Γ⊎(y : τ′′)▷_{Θ} ey : τ, (Γ⊎(y : τ′′))(x) = τ′, |τ′| = 1, (Γ⊎(y : τ′′))⊎Δ well defined and Δ ▷_{Θ} e′ : τ′. By the type rule for application Γ ▷_{Θ} e : τ′′ →^{κ} τ, and by induction (Γ − (x : τ′)) ⊎ Δ ▷_{Θ} {e′/x}e : τ′′ →^{κ} τ. By the type rule we conclude (Γ − (x : τ′)) ⊎ (y : τ′′)⊎Δ▷_{Θ} ({e′/x}e)y : τ which is equivalent to ((Γ⊎(y : τ′′))(x : τ′))⊎Δ▷_{Θ} {e′/x}(ey) : τ

case λy. e

Simple induction as above.

case e_{1} + e_{2}

Assume Γ_{1} ⊎ Γ_{2} ▷_{Θ} e_{1} + e_{2} : Int^{κ}, (Γ_{1} ⊎ Γ_{2})(x) = τ′, |τ′| = 1, (Γ_{1} ⊎ Γ_{2}) ⊎ Δ well defined and Δ ▷_{Θ} e′ : τ′. By the type rule Γ_{1} ▷_{Θ} e_{1} : Int^{κ_{1}} and Γ_{2} ▷_{Θ} e_{2} : Int^{κ_{2}}. Since |τ′| = 1, either Γ_{1}(x) = τ′ and Γ_{2}(x) is undefined or vice versa. In either case the proof proceeds by simple induction as above.

case let \overline{x} = \overline{e} in e′

Essentially as the case above.

case case e_{1} of {nil → e_{2}; cons y_{1} y_{2} → e_{3}}

Essentially as above. Just note that either x appears in Γ_{1} or in both Γ_{2} and Γ_{3}, and this matches the definition of {e′/x}. □

Lemma 6.4.3 (Free variables of an ω-value) If Γ ▷_{Θ} v : τ and |τ| = ω then |Γ| = ω.

Proof Simple case analysis of the syntax of values. □

Use types are preserved by reduction. The proof is straightforward, verifying each rule in Figure 4 separately, and using structural induction over terms for the compatible closure.

Proposition 6.4.4 (Subject reduction) If Γ ▷_{Θ} e : τ and e ⟹ e′ then there exists Γ′ such that Γ′ ▷_{Θ} e′ : τ and Γ′ ⊆ Γ.

Proof

case n_{0} + n_{1} ⟹ \underline{n_{0} + n_{1}}

Trivial.

case (λx. e) y ⟹ [y/x]e

Assume Γ ▷_{Θ} (λx. e)y : τ. There must exists Δ, τ′ such that Γ = Δ ⊎ x : τ′ and Δ ▷_{Θ} λx. e : τ′ →^{κ} τ. Further Δ′ exists such that Δ = Δ′ − x : τ′ and Δ′ ▷_{Θ} e : τ. Then [y/x]Δ′ ▷_{Θ} [y/x]e : τ so since [y/x]Δ′ = [y/x]Δ′ − (y : τ′) ⊎ (y : τ′) = [y/x](Δ′ − (x : τ′)) ⊎ (y : τ′) = Δ′ − x : τ′ ⊎ y : τ′ = Γ we get Γ ▷_{Θ} [y/x]e : τ.

case case nil of {nil → e_{1}; cons x y → e_{2}} ⟹ e_{1}

Assume Γ ▷_{Θ} case nil of {nil → e_{1}; cons x y → e_{2}} : τ. Then we must have Γ = Γ_{1} ⊎ (Γ_{2} + (Γ_{3} − (x : τ′, y : [τ′]^{κ}))) such that Γ_{2} ▷_{Θ} e_{1} : τ. Clearly Γ_{2} ⊆ Γ.

case case (cons y_{0} y_{1}) of {nil → e_{1}; cons x_{0} x_{1} → e_{2}} ⟹ [y_{0}/x_{0}, y_{1}/x_{1}]e_{2}

Assume Γ ▷_{Θ} case nil of {nil → e_{1}; cons x y → e_{2}} : τ. Then we must have Γ = Γ_{1} ⊎(Γ_{2} +(Γ_{3} −(x : τ′, y : [τ′]^{κ}))) such that Γ_{1}sdΘconsy_{0} y_{1} : [τ′]^{κ} and Γ_{3} ▷_{Θ} e_{2} : τ. Clearly Γ_{1} = y_{0} : τ′, y_{1} : [τ′]^{κ}. Now [y_{0}/x_{0}, y_{1}/x_{1}]Γ_{3} ▷_{Θ} [y_{0}/x_{0}, y_{1}/x_{1}]e_{2} : τ and [y_{0}/x_{0}, y_{1}/x_{1}]Γ_{3} = Γ_{1} ⊎ ([y_{0}/x_{0}, y_{1}/x_{1}]Γ_{3} − (y_{0} : τ′, y_{1} : [τ′]^{κ})) = Γ_{1} ⊎ [y_{0}/x_{0}, y_{1}/x_{1}](Γ_{3} − (x_{0} : τ′, x_{1} : [τ′]^{κ})) = Γ_{1} ⊎ (Γ_{3} − (x_{0} : τ′, x_{1} : [τ′]^{κ})) ⊆ Γ.

case L[let \overline{x} = \overline{e} in e′] ⟹ let \overline{x} = \overline{e} in L[e′]

Assume Γ ▷_{Θ} L[let \overline{x} = \overline{e} in e′] : τ. Then (by checking the cases for L) there exists Δ, Δ′, τ′ such that Γ = Δ ⊎ Δ′ and Δ ▷_{Θ} let \overline{x} = \overline{e} in e′ : τ′. Now Δ = (Δ_{1} ⊎ ⋯ ⊎ Δ_{n} ⊎ Δ′′) − (x_{1} : τ_{1}, …, x_{n} : τ_{n}) such that Δ′′ ▷_{Θ} e′ : τ′. Then if x_{1}, …, x_{n} is not in the domain of Δ′ we have that Δ′′ ⊎ Δ′ is well defined and Δ′′ ⊎ Δ′ ▷_{Θ} L[e′] : τ. Then (Δ_{1} ⊎ ⋯ ⊎ Δ_{n} ⊎ Δ′′ ⊎ Δ′) − (x_{1} : τ_{1}, …, x_{n} : τ_{n}) is well defined and equal to Γ, so we can conclude Γ ▷_{Θ} let \overline{x} = \overline{e} in L[e′] : τ by the let rule.

case let x_{0} = e_{0}, …, x_{i} = v, …, x_{n} = e_{n} in C[x_{i}] ⟹ let x_{0} = e_{0}, …, x_{i} = v, …, x_{n} = e_{n} in C[v] where |v| = ω

Assume Γ ▷_{Θ} let x_{0} = e_{0}, …, x_{i} = v, … x_{n} = e_{n} in C[x_{i}] : τ. We have Γ = (Γ_{0} ⊎ ⋯ Γ_{i} ⋯ ⊎ Γ_{n} ⊎ Δ) − (x_{1} : τ_{1}, …, x_{i} : τ_{i}, …, x_{n} : τ_{n}) where Γ_{0} ▷_{Θ} e_{0} : τ_{0}, …, Γ_{i} ▷_{Θ} v : τ_{i}, …, Γ_{n} ▷_{Θ} e_{n} : τ_{n}. By Lemma 6.4.1 we get Δ′ ⊆ Δ ⊎ Γ_{i} such that Δ′ ▷_{Θ} C[v] : τ. Now Γ′ = (Γ_{1} ⊎ ⋯ Γ_{i} ⋯ ⊎ Γ_{n} ⊎ Δ′) − (x_{1} : τ_{1}, …, x_{i} : τ_{i}, …, x_{n} : τ_{n}) is well defined and a subset of Γ since |v| = ω implies |Γ_{i}| = ω by Lemma 6.4.3. This gives us Γ′ ▷_{Θ} let x_{0} = e_{0}, …, x_{i} = v, …, x_{n} = e_{n} in C[v] : τ. case let x_{0} = e_{0}, …, x_{i−1} = e_{i−1}, x_{i} = e_{i}, x_{i+1} = e_{i+1}, … x_{n} = e_{n} in C[x_{i}] ⟹ let x_{0} =

e_{0}, …, x_{i−1} = e_{i−1}, x_{i+1} = e_{i+1}, …, x_{n} = e_{n} in C[v] where |v| = 1

Assume Γ ▷_{Θ} let x_{0} = e_{0}, …, x_{i−1} = e_{i−1}, x_{i} = e_{i}, x_{i+1} = e_{i+1}, … x_{n} = e_{n} in C[x_{i}] : τ. Then Γ_{0} ▷_{Θ} e_{0} : τ_{0}, …, Γ_{i−1} ▷_{Θ} e_{i−1} : τ_{i−1}, Γ_{i} ▷_{Θ} e_{i} : τ_{i}, Γ_{i+1} ▷_{Θ} e_{i+1} : τ_{i+1}, …, Γ_{n} ▷_{Θ} e_{n} : τ_{n} where Γ = (Γ_{0} ⊎ ⋯ Γ_{i−1} ⊎ Γ_{i} ⊎ Γ_{i+1} ⋯ ⊎ Γ_{n} ⊎ Δ) − (x_{1} : τ_{1}, …, x_{i−1} : τ_{i−1}, x_{i} : τ_{i}, x_{i+1} : τ_{i+1}, …, x_{n} : τ_{n}). Now by Lemma 6.4.2 we get (Δ − (x_{i} : τ_{i})) ⊎ Γ_{i} ▷_{Θ} C[e_{i}] : τ. We have that (Γ_{0} ⊎ ⋯ Γ_{i−1} ⊎ Γ_{i+1} ⋯ ⊎ Γ_{n} ⊎ (Δ − (x_{1} : τ_{i})) ⊎ Γ_{i}) − (x_{1} : τ_{1}, …, x_{i−1} : τ_{i−1}, x_{i+1} : τ_{i+1}, …, x_{n} : τ_{n}) is well defined and equal to Γ since |τ_{i}| = 1 and x_{i} appears in Δ.

case let x_{0} = e_{0}, …, x_{i} = let y_{0} = e′_{0}, …, y_{m} = e′_{m} in e′, …, x_{n} = e_{n} in e ⟹ let y_{0} = e′_{0}, …, y_{m} = e′_{m}, x_{0} = e_{0}, …, x_{i} = e′, …, x_{n} = e_{n} in e

Straightforward.

case let x_{0} = e_{0}, …, x_{i−1} = e_{i−1}, x_{i} = e_{i}, x_{i+1} = e_{i+1}, …, x_{n} = e_{n} in e ⟹ let x_{0} = e_{0}, …, x_{i−1} = e_{i−1}, x_{i+1} = e_{i+1}, …, x_{n} = e_{n} in e if x_{i} ∉ fv(e) ∪ fv(e_{0}) ∪ ⋯ ∪ fv(e_{i−1}) ∪ fv(e_{i+1}) ∪ ⋯ ∪ fv(e_{n})

Straightforward. □

Combining Propositions 6.4.4 and 6.2.3 yields a soundness result for our type system with respect to the operational semantics.

Corollary 6.4.5 (Operational subject reduction) If ⊢_{Θ} let ⟨H⟩ in e : τ and ⟨H⟩ e ⇓ ⟨H′⟩ v then ⊢_{Θ} let ⟨H′⟩ in v : τ.

6.5 Additional transformations

There are many useful program transformation rules that we might add to those appearing in Figure 4.

For instance, it is helpful to have the reduction

let \overline{x} = \overline{e} in (let y = e_{1} in e_{2}) ⟹
let y = (let \overline{x} = \overline{e} in e_{1}) in e_{2}, if \overline{x} ∉ fv(e_{2}),

which avoids the creation of a closure for \overline{e} if, say, y is not evaluated at run time. By the way, note that the rule L[let \overline{x} = \overline{e} in e′] ⟹ let \overline{x} = \overline{e} in L[e′] has as an instance

let y = (let \overline{x} = \overline{e} in e_{2}) in e_{3} ⟹
let \overline{x} = \overline{e} in (let y = e_{2} in e_{3}), if \overline{x} ∉ fv(e_{3}),

which is helpful if, say, further simplification reduces e_{2} to a value. The Glasgow Haskell compiler makes extensive use of both reductions [PS94]. The fact that the latter rule undoes the effect of the former is not a problem in practice, since one can apply the rules in separate phases: first flatten out as many ‘let’s as possible using the second rule, do any transformations which were enabled by the flattening phase, then finally push any remaining ‘let’s back inwards using the first rule.

We could, in fact, continue and write a number of additional rules which can float letbound expressions inwards towards their uses. Such transformations complement the substitution rules already present in the reduction rules, since they allow arbitrary let-bound expressions to move inwards (rather than just values, as is the case in the reduction rules).

Most such rules can be formulated purely syntactically (for example, using conditions on free variables such as the condition x ∉ fv(e_{3}) above). However, we require usage information to safely control the following reduction rule, which moves a ‘let’ inside a lambda abstraction.

let \overline{x} = \overline{e} in (λy. e′) ⟹ λy. (let \overline{x} = \overline{e} in e′), if |λy. e| = 1.

We need to add a further use annotation to terms: we assume that each abstraction λx. e is annotated with a use of 1 or ω which we write |λx. e|. The use information is crucial for safety: the above reduction might duplicate computation if |λy. e| = ω (the expression ‘λy. (let x = e′in e)’ evaluates e′ every time it is applied, while ‘let x = e′in (λy. e)’ evaluates e′ at most once). Again, this reduction is extensively used in the Glasgow Haskell compiler. It turns out to be particularly important for one form of deforestation [GLP93].

Let-floating rules such as those described above can be used to achieve the effect of “safe” expression inlining. Moreover, the let-floating rules all preserve the type of a term in our system, enabling efficient type-based optimisation (since usage information need not be recalculated during optimisation).

7 Use analysis for call-by-value calculi

Our use analysis can easily be adapted for call-by-value calculi. In such calculi, we are interested in variables which are used exactly once (rather than at most once). For example, if f is used exactly once, and x is only used in the body of f, then we can safely transform

let x = e in let f = λy. x + 3 in …

into

let f = λy. e + 3 in …

(hopefully reducing the maximum amount of storage used by the program, and potentially exposing other optimisations). This transformation is clearly unsafe if f is never used, since the expression e might be non-terminating — we would have transformed a non-terminating program into a terminating program.

Changing our type system to determine when a value is used exactly once is easy. We simply change the weakening rule as below:

Weak \frac{Γ ⊢_{Θ} \overline{e} : \overline{τ}  |τ′| = ω}{Γ, x : τ′ ⊢_{Θ} \overline{e} : \overline{τ}}

We can now interpret the use 1 as meaning that a value is used exactly once. This transforms our type system into something much closer to a linear type system. In a companion paper [MOTW95], we elaborate on the connections between linear logic and call-by-value reduction, and affine logic and call-by-need reduction.

We conjecture that usage-based program transformation in the presence of side-effects could be handled by combining our usage analysis with an effect system [Luc87, LG88, JG91]. (Effect systems can be used to distinguish side-effecting computation from purely functional computation.)

8 Related work

8.1 Linear logic

The type system presented here is based on ideas taken from the linear logic of Girard [Gir87] and its successor, the Logic of Unity [Gir93]. A companion paper describes the embedding of the call-by-need calculus into linear logic that underlies the type system used here [MOTW95]. Interested readers are referred to that paper for a survey of related work on linear logic.

Inspired by Girard’s Logic of Unity, we might be tempted to refine our type system by annotating variables separately from types, thus allowing a variable to be annotated with 1 even if its type has use ω. For example, in the following expression our type system assigns both x and y use ω (since x and y are forced to have the same type).

let x = 1 + 2 in

\begin{matrix}let y = x in \\ ⋯ x ⋯ y ⋯ \end{matrix}

Examples such as the one above are relatively common in practice, but do not cause any problems since trivial let-bindings such as ‘let y = x in ⋯’ can always be eliminated during optimisation. It is possible that there exist other inaccuracies which cannot be circumvented so easily, but we choose to retain our simpler analysis until we have implemented it in the Glasgow Haskell compiler and measured the effect (if any) of such refinements on real-life programs.

8.2 Call-by-need analyses

We are aware of two other analyses that attempt to determine when a value is used at most once under call-by-need evaluation. One is a type system due to Launchbury and others [Lau92], the other is an abstract interpretation due to Marlow [Mar93]. We note three points of comparison.

First, unlike ours, neither of the other analyses possess a proof of soundness. Second, our system sometimes derives more precise information than the other two; see Example 3 in Section 1.1. Third, unlike the above analyses, our type system does not detect the case where closures are never used (we omitted the zero usage from our analysis so as to simplify our usage constraints).

Our next step is to implement our analysis in the Glasgow Haskell compiler, allowing us to compare it directly with Marlow’s. By observing how our analysis performs on real programs we can test whether omitting zero usages has a significantly impact.

Concurrent Clean’s uniqueness types [BS93] are related to our call-by-need analysis since they are proved sound with respect to a graph-reduction semantics which correctly models the sharing of reductions that occur in an implementation. However, uniqueness types are designed to deal with data structure update, rather than program transformation and closure update (see Section 8.4 for a more detailed comparison).

8.3 Call-by-name analyses

We also are aware of two analyses that determine usage information for values under call-by-name reduction, one due to Wright and Baker-Finch [WB93], the other due to Courtenage and Clack [CC94]. Both are based on type systems, and both have been argued to be sound. We note three points of comparison.

First, choosing call-by-name evaluation instead of call-by-need prevents even fairly simple optimisations from being discovered. For instance, in Example 1 of Section 1.1, the variable x is used once under call-by-need, as our system discovers, but twice under call-by-name. Experience suggests this difference is significant, as the situation encountered in Example 1 is fairly common.

Second, even if we are satisfied to limit our attention to call-by-name, neither system provides an especially useful analysis. The Wright and Baker-Finch system discovers too much information: function types are annotated with natural numbers which indicate the number of times a function uses its argument, and this level of accuracy renders the type system undecidable. The Courtenage and Clack system discovers too little information: they can determine when an argument is used zero times, exactly once, or at least once; but (because of the lack of disjunctive types) they cannot determine when an argument is used at most once, which is most helpful for the problems we are interested in.

Third, unlike our system, the other systems also provide information about when a value is used at least once, which is useful for strictness analysis. For this question, the distinction between call-by-need and call-by-name is irrelevant, which may explain why the authors of these systems were willing to settle for a call-by-name analysis.

8.4 Data structure update

A number of analyses for in-place update of data structures have been proposed, including those by Schmidt [Sch85], Hudak [Hud86], Baker [Bak90], Guzmán and Hudak [GH90], Wadler [Wad90b, Wad91], and Barendsen and Smetsers [BS93]. In such analyses it is sufficient to check that there can be at most one live pointer to a data structure.

For example, in the following expression the ‘then’ and ‘else’ clauses can only be executed after the predicate p(x) has evaluated to a boolean. But a boolean cannot contain a reference to x, so the second reference to x in the ‘then’ clause is never live at the same time as the reference to x in the predicate p(x).

let x = e in (if p(x) then x else y)

This refined usage information, which is not discovered by our analysis, is extremely useful when considering in-place update of data structures. However, inspection of the above example also reveals that such information is of little use for program transformation or update analysis: even though x has at most one live reference, we cannot substitute e for x without duplicating work, nor can we avoid updating the closure for x.

9 Conclusions

We have presented a simple type system which can determine when a value is used at most once, even in the presence of higher-order functions and data structures. Our analysis is tailored to the precise reduction strategy used in the Glasgow Haskell compiler, and therefore yields more accurate results than analyses which assume call-by-name reduction. We have proved our type system sound with respect to Launchbury’s natural semantics of lazy evaluation, and have provided safe reduction rules which the compiler can use to transform programs without risking duplicating work.

A prototype type inference algorithm has already been implemented. Our next step is to incorporate our type system into the Glasgow Haskell compiler [PHHPW93]. This will enable us to measure the effect of our optimisations on large Haskell programs. The Glasgow Haskell compiler uses an explicitly-typed core language to express most of its program transformations. By adding our usage information to the core language type system we can conveniently provide information to the optimiser, enabling additional program transformations, and allowing the code generator to omit unnecessary closure updates.

Our annotated types also provide a convenient way of communicating usage information across module boundaries (we simply add usage information to the user-level type information which is already exported from a module).

We intend to further explore how our type system enables in-place update of data structures. An interesting question is how much of this should be done automatically by the compiler, how much should be under the control of the user, and to what extent the type system acts as an effective mechanism to let the user understand and control optimisations.

The information computed by our analysis seems at first glance to be similar to that which is required for strictness analysis. However, for the purposes of strictness analysis one needs to know when an expression is used at least once. We conjecture that a generalisation of our type system might be able to provide simple strictness information at the same time as inferring information for use in program transformation and update analysis.

10 Acknowledgements

The ideas described here grew out of collaboration with the Glasgow functional programming group, especially Simon Peyton Jones, John Launchbury, Andy Gill, Simon Marlow, Will Partain, Patrick Sansom, and Andre Santos. The Semantique II working group provided helpful feedback, especially Patrick Cousot, Sebastian Hunt, Torben Mogensen, Dave Sands, and Yan-Mei Tang.

References

[AFMOW95] Z. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. A call-by-need lambda calculus. Symposium on Principles of Programming Languages, ACM Press, San Francisco, California, January 1995.

[Aug93] L. Augustsson, Implementing Haskell overloading. In Functional Programming Languages and Computer Architecture, Copenhagen, Denmark, June 1993. ACM Press.

[Bak90] H. Baker, Unify and conquer (garbage, updating, aliasing …) in functional languages. In Conference on Lisp and Functional Programming, ACM Press, Nice, June 1990.

[BS93] E. Barendsen, and S. Smetsers. Conventional and Uniqueness Typing in Graph Rewrite Systems (extended abstract). In Proceedings 13th Conference on the Foundations of Software Technology and Theoretical Computer Science, Springer-Verlag LNCS 761, 1993.

[CC94] S. A. Courtenage and C. D. Clack, Analysing resource use in the λ-calculus by type inference, In ACM Sigplan Workshop on Partial Evaluation and Semantics-Based Program Manipulation, 1994.

[DM82] L. Damas and R. Milner, Principal type schemes for functional programs. In Proceedings 9’th ACM Symposium on Principles of Programming Languages, Albuquerque, N.M., January 1982.

[Gir87] J.-Y. Girard, Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[Gir93] J.-Y. Girard, On the unity of logic. Annals of Pure and Applied Logic, 59:201–217, 1993.

[GH90] J. Guzmán and P. Hudak, Single-threaded polymorphic lambda calculus. In Proceedings 5’th IEEE Symposium on Logic in Computer Science, Philadelphia, Pa., June 1990.

[GLP93] A. Gill, J. Launchbury, and S. Peyton Jones, A short-cut to deforestation. In Functional Programming Languages and Computer Architecture, Copenhagen, Denmark, June 1993. ACM Press.

[Hin69] R. Hindley, The principal type scheme of an object in combinatory logic. Trans. Am. Math. Soc., 146:29–60, December 1969.

[Hud86] P. Hudak, A semantic model of reference counting and its abstraction. In Proceedings ACM Conference on Lisp and Functional Programming, Cambridge, Mass., August 1986.

[Jon93] M. Jones, Partial evaluation for dictionary-free overloading. Technical report TR-959, Computer Science Department, Yale University, April 1993.

[JG91] Pierre Jouvelot and D.K. Gifford, Algebraic reconstruction of types and effects. In ACM Symposium on Principles of Programming Languages, 1991.

[Lau92] J. Launchbury, A. Gill, J. Hughes, S. Marlow, S. Peyton Jones, and P. Wadler. Avoiding unnecessary updates. In Glasgow Workshop on Functional Programming, Ayr, July 1992. Springer Verlag Workshops in Computing Series.

[Lau93] J. Launchbury, A natural semantics for lazy evaluation. In Proceedings 20’th ACM Symposium on Principles of Programming Languages, Charleston, S.C., January 1993.

[Luc87] J.M. Lucassen, Types and effects, towards an integration of functional and imperative programming. PhD thesis, MIT Laboratory for Computer Science, 1987.

[LG88] J.M. Lucassen and D.K. Gifford, Polymorphic effect systems. In ACM Symposium on Principles of Programming Languages, 1988.

[Mar93] S. Marlow, Update avoidance analysis by abstract interpretation. In Glasgow Workshop on Functional Programming, Ayr, July 1993. Springer Verlag Workshops in Computing Series.

[Mit84] J. C. Mitchell, Coercion and type inference (summary). In Proceedings 11’th ACM Symposium on Principles of Programming Languages, January 1984.

[Mit91] J. C. Mitchell, Type inference with simple subtypes. Journal of Functional Programming, 1(3):245–286, July 1991.

[MOTW95] J. Maraist, M. Odersky, D. Turner, and P. Wadler. Call-by-name, call-by-value, call-by-need, and the linear lambda calculus. In 11’th International Conference on the Mathematical Foundations of Programming Semantics, New Orleans, Louisiana, April 1995.

[MTW95] C. Mossin, D.N. Turner, and P. Wadler, Once Upon A Type. In 7’th International Conference on Functional Programming and Computer Architecture, San Diego, California, June 1995.

[MW92] S. Marlow and P. Wadler, Deforestation for higher order functions. In Glasgow Workshop on Functional Programming, Ayr, July 1992. Springer Verlag Workshops in Computing Series.

[Pey92] S. Peyton Jones, Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine Journal of Functional Programming, 2(2):127–202, April 1992.

[PHHPW93] S.L. Peyton Jones, C.V. Hall, K. Hammond, W.D. Partain, and P.L. Wadler, The Glasgow Haskell compiler: a technical overview. In Joint Framework for Information Technology (JFIT), Technical Conference Digest, March, 1993.

[PS94] S. Peyton Jones and A. Santos, Compilation by Transformation in the Glasgow Haskell Compiler. In Glasgow Workshop on Functional Programming, Ayr, September 1994. Springer Verlag Workshops in Computing Series.

[Rob65] J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle. Journal of the Association for Computing Machinery, 12(1), January 1965.

[Sch85] D. A. Schmidt, Detecting global variables in denotational specifications. ACM Trans. on Programming Languages and Systems, 7:299–310, 1985.

[SP95] P. Sansom and S. L. Peyton Jones, Time and space profiling for non-strict higherorder functional languages. In 22’nd ACM Symposium on Principles of Programming Languages, San Francisco, January 1995.

[Wad90a] P. Wadler, Deforestation: Transforming programs to eliminate trees, Theoretical Computer Science, 73, 1990.

[Wad90b] P. Wadler, Linear types can change the world! In M. Broy and C. Jones, editors, Programming Concepts and Methods, Sea of Galilee, Israel, April 1990. North Holland, 1990.

[Wad91] P. Wadler, Is there a use for linear logic? In Conference on Partial Evaluation and Semantics-Based Program Manipulation (PEPM), ACM Press, New Haven, Connecticut, June 1991.

[WB93] D. A. Wright and C. A. Baker-Finch, Usage analysis with natural reduction types. In Workshop on Semantic Analysis, 1993.

Comb \frac{Γ_{1} ⊢_{Θ} e_{1} : τ_{1}  ⋯  Γ_{n} ⊢_{Θ} e_{n} : τ_{n}}{Γ_{1}, …, Γ_{n} ⊢_{Θ} e_{1}, …, e_{n} : τ_{1}, …, τ_{n}}
Cont \frac{Γ, x : τ′, y : τ′ ⊢_{Θ} \overline{e} : \overline{τ}  |τ| = ω}{Γ, z : τ′ ⊢_{Θ} [z/x, z/y]\overline{e} : \overline{τ}}
Weak \frac{Γ ⊢_{Θ} \overline{e} : \overline{τ}}{Γ, x : τ′ ⊢_{Θ} \overline{e} : \overline{τ}}  Exch \frac{Γ, x : τ_{1}, y : τ_{2}, Δ ⊢_{Θ} \overline{e} : \overline{τ}}{Γ, y : τ_{2}, x : τ_{1}, Δ ⊢_{Θ} \overline{e} : \overline{τ}}
Var \overline{x : τ ⊢_{Θ} x : τ}  Abs \frac{Γ, x : τ ⊢_{Θ} e : τ′ κ ≤_{Θ} |Γ|}{Γ ⊢_{Θ} λx. e : τ →^{κ} τ′}
App \frac{Γ ⊢_{Θ} e : τ →^{κ} τ′ Δ ⊢_{Θ} x : τ}{Γ, Δ ⊢_{Θ} e x : τ′}
Int \overline{⊢_{Θ} n : Int^{κ}}  Plus \frac{Γ ⊢_{Θ} e_{1} : Int^{κ_{1}}  Δ ⊢_{Θ} e_{2} : Int^{κ_{2}}}{Γ, Δ ⊢_{Θ} e_{1} + e_{2} : Int^{κ}}
Nil \overline{⊢_{Θ} nil : [τ]^{κ}}  Cons \frac{Γ ⊢_{Θ} x : τ  Δ ⊢_{Θ} y : [τ]^{κ}}{Γ, Δ ⊢_{Θ} cons x y : [τ]^{κ}}
Case \frac{Γ ⊢_{Θ} e_{1} : [τ]^{κ} Δ ⊢_{Θ} e_{2} : τ′ Δ, x : τ, y : [τ]^{κ} ⊢_{Θ} e_{3} : τ′}{Γ, Δ ⊢_{Θ} case e_{1} of \{nil → e_{2}; cons x y → e_{3}\} : τ′}
Let \frac{Γ, x_{1} : τ_{1}, …, x_{n} : τ_{n} ⊢_{Θ} e_{1}, …, e_{n}, e : τ_{1}, …, τ_{n}, τ}{Γ ⊢_{Θ} let x_{1} = e_{1}, …, x_{n} = e_{n} in e : τ}

Figure 1: Type rules

Var \overline{x : τ ▷_{Θ} x : τ}
Abs \frac{Γ ▷_{Θ} e : τ′ κ ≤_{Θ} |Γ − x : τ|}{Γ − x : τ ▷_{Θ} λx. e : τ →^{κ} τ′}  App \frac{Γ ▷_{Θ} e : τ →^{κ} τ′}{Γ × x : τ ▷_{Θ} e x : τ′}
Int \overline{▷_{Θ} n : Int^{κ}} Plus \frac{Γ_{1} ▷_{Θ} e_{1} : Int^{κ_{1}} Γ_{2} ▷_{Θ} e_{2} : Int^{κ_{2}}}{Γ_{1} × Γ_{2} ▷_{Θ} e_{1} + e_{2} : Int^{κ}}
Nil \overline{▷_{Θ} nil : [τ]^{κ}}  Cons \overline{x : τ, y : [τ]^{κ} ▷_{Θ} cons x y : [τ]^{κ}}
Case \frac{Γ_{1} ▷_{Θ} e_{1} : [τ]^{κ} Γ_{2} ▷_{Θ} e_{2} : τ′ Γ_{3} ▷_{Θ} e_{3} : τ′}{Γ_{1} × (Γ_{2} + (Γ_{3} − (x : τ, y : [τ]^{κ}))) ▷_{Θ} case e_{1} of \{nil → e_{2}; cons x y → e_{3}\} : τ′}
Let \frac{Γ_{1} ▷_{Θ} e_{1} : τ_{1} ⋯ Γ_{n} ▷_{Θ} e_{n} : τ_{n} Δ ▷_{Θ} e : τ}{(Γ_{1} × ⋯ × Γ_{n} × Δ) − (x_{1} : τ_{1}, …, x_{n} : τ_{n}) ▷_{Θ} let x_{1} = e_{1}, …, x_{n} = e_{n} in e : τ}

Figure 2: Syntax-directed type rules

Let \frac{Γ ⊢_{(Σ; Θ)} e_{0} : σ Δ, x : σ ⊢_{(Σ; Θ)} e_{1} : τ}{Γ, Δ ⊢_{(Σ; Θ)} let x = e_{0} in e_{1} : τ}
Gen \frac{Γ ⊢_{(Σ, a^{κ}; Θ)} e : σ}{Γ ⊢_{(Σ; Θ)} e : ∀a^{κ}. σ}  Spec \frac{Γ, x : [τ/a^{κ}]σ ⊢_{(Σ; Θ)} e : τ′ κ ≤_{Θ} |τ|}{Γ, x : ∀a^{κ}. σ ⊢_{(Σ; Θ)} e : τ′}
Gen-Use \frac{Γ ⊢_{(Σ; Θ, j≤\{k_{1},...,k_{n}\})} e : σ}{Γ ⊢_{(Σ; Θ)} e : ∀j ≤ \{k_{1}, …, k_{n}\}. σ}
Spec-Use \frac{Γ, x : [ι/i]σ ⊢_{(Σ; Θ)} e : τ′ ι ≤_{Θ} k_{1} ⋯ ι ≤_{Θ} k_{n}}{Γ, x : ∀i ≤ \{k_{1}, …, k_{n}\}. σ ⊢_{(Σ; Θ)} e : τ′}

Figure 3: Type rules (polymorphic)

n_{1} + n_{2}  ⟹ \underline{n_{1} + n_{2}}
(λx. e) y  ⟹ [y/x]e
case nil of {nil → e_{1}; cons x y → e_{2}}  ⟹ e_{1}
case (cons y_{0} y_{1}) of {nil → e_{1}; cons x_{0} x_{1} → e_{2}} ⟹ [y_{0}/x_{0}, y_{1}/x_{1}]e_{2}
L[let \overline{x} = \overline{e} in e′] ⟹ let \overline{x} = \overline{e} in L[e′]
letrec x = v in C[x] ⟹ letrec x = v in C[v]
let x = v in C[x]  ⟹ let x = v in C[v]  if |x| = ω
let x = v in C[x]  ⟹ C[v]  if |x| = 1

Figure 4: Call-by-need reductions