Compiling Laziness using Projections

Ross Paterson

School of Computing, University of North London, Eden Grove, London N7 8DB, UK

Abstract. Projection-based strictness analysis is a powerful technique, able to cope with non-flat domains and latent demand. By analysing the projections as embedding-projection pairs, we develop an algorithm to translate lazy functions into a strict functional language with explicit closures. The translated functions typically operate on simpler types than the originals, in particular types containing fewer liftings, which correspond to the operational notion of closures. Like the analysis on which it is based, our algorithm is restricted to first-order functions.

1 Introduction

A lazy functional language provides great expressive power, but this comes at a cost in both space and time, for delayed computations must be stored as closures on the heap. The management of these closures also adds to execution time, and the frequent context switches frustrate both compile-time optimization and efficient exploitation of hardware.

Strictness analysis [17,3,20,14] aims to ameliorate this situation by identifying strict functions, which can be implemented using call-by-value. The arguments of such functions may be evaluated early and passed unboxed. This has contributed to compiler performance, but the changes to the code generator are seldom formally verified.

There have been some efforts to verify these alterations. Modifications of the CPS translation [2] to use simple strictness information have been described by Danvy and Hatcliffe [6] and by Burn and Le Métayer [4]. Amtoft [1] describes a modification of a type-based strictness analysis to generate code that creates fewer thunks.

Peyton Jones and Launchbury [19,18] introduce flat domains to their source language, interpreting them operationally as unboxed values. They are thus able to verify unboxing transformations in the source language.

The above systems are based on information about active demand, i.e. statements that a certain amount of a data structure will be required. In the presence of lazy data structures, e.g. streams, one is also interested in latent demand, i.e. statements that though a value may not be required, if it is then so much of it must be evaluated. This sort of strictness information can be obtained by projection-based strictness analysis [20].

This paper extends the projection technique to obtain a new algorithm translating lazy functional programs to more efficient strict forms.

1.1 Projection-based Strictness Analysis

In order to capture strictness over simple domains as well as non-flat domains, Wadler and Hughes [20] introduced projections over extended domains to describe evaluation contexts. An equivalent formulation [15] defines a projection over a type t as a partial function α : t ∘→ t satisfying α ≤ id and α ∘ α = α. For example, the projection Str : ∀ a. a_{⊥} ∘→ a_{⊥} is defined only if its argument is not ⊥. (A type t_{⊥} consists of the elements of t, which may or may not contain a bottom element, plus a new bottom element.) The projection Both : ∀ a, b. a_{⊥}×b_{⊥} → a_{⊥} × b_{⊥} is defined only if neither of its arguments are ⊥.

The analysis of a total function f : t_{α} → t_{β} for a given context projection β : t_{β} ∘→ t_{β} yields an equation

β ∘ f = β ∘ f ∘ α  (1)

This equation implies that for an application of f in the context β, the context of the argument of f is given by the projection α : t_{α} ∘→ t_{α}. For example, the iterative factorial function fact : Num_{⊥} × Num_{⊥} → Num_{⊥} (where Num is the set of numbers, without ⊥) is seen to satisfy

Str ∘ fact = Str ∘ fact ∘ Both  (2)

indicating that it is strict in both arguments. Moreover, such projection equations can also capture latent strictness properties such as head strictness, which says that if a list is ever evaluated to weak head normal form, its head will also be evaluated. This analysis has been implemented by Kubiak, Hughes and Launchbury [13]. The present formulation is based on theirs.

1.2 This Paper

The point of departure of this paper is Launchbury’s observation [15] that the images of these partial projections correspond to unboxed types. These images may be described using embedding-projection pairs. A partial projection α is factored as α^{E} ∘ α^{P}, for a total function α^{E} : t′_{α} → t_{α} and a partial function α^{P} : t_{α} ∘→ t′_{α} such that α^{P} ∘ α^{E} = id and α^{E} ∘ α^{P} ≤ id. The type t′_{α} will be a simpler variant of the type t_{α}. For example, the projection Str factors as an embedding of a type a in the type a_{⊥}. The latter lifted type might be implemented using closures, the former using unboxed values. Here the embedding component merely boxes the number; the projection component demands the value of a closure, and is therefore partial. Similarly, the projection Both corresponds to an embedding of the type a × b in the type a_{⊥} × b_{⊥}.

Now (2) expands to

Str^{E} ∘ Str^{P} ∘ fact = Str^{E} ∘ Str^{P} ∘ fact ∘ Both^{E} ∘ Both^{P}

Composing Str^{P} on the left to cancel the Str^{E}’s, this is equivalent to

Str^{P} ∘ fact = Str^{P} ∘ fact ∘ Both^{E} ∘ Both^{P}  (3)

Now we can fuse the composition Str^{P} ∘ fact ∘ Both^{E}, yielding a variant fact′ : Num×Num ∘→ Num. This function, which operates on unboxed numbers instead of closures, can then be used in place of fact. The projection component Both^{P} goes on to provide a context for the arguments of fact.

General fusion is difficult, so we shall alter projection analysis to generate equations of the form

β^{P} ∘ f = f_{β} ∘ α^{P}  (4)

for some partial function f_{β} : t′_{α} ∘→ t′_{β}. The rules of our algorithm thus correspond to those of projection-based strictness analysis; the novelty here is the translated version f_{β}.

The source language of our translation is a small first-order lazy functional language, defined in Sect. 2. The main unusual feature of this language is that lifting is treated as a separate type constructor. This allows us to treat the issues raised by each type constructor separately, and also to deal with unlifted types, which are avoided in most accounts of strictness analysis.

The translation sketched above produces partial functions. The projection components of e-p pairs are also partial functions. To express these, we introduce in Sect. 3 a small first-order strict functional language, with explicit delay and force constructs, as in Scheme [5].

The usual next step would be to give denotational descriptions of these two languages in a semantic meta-language. However, this meta-language would be essentially equivalent to our source language. Instead, we give an axiomatic description of the lazy language, and define the strict language by a translation to the lazy language. Then the rules of our algorithm expand to formulas over the lazy language.

Since everything is translated back to the lazy language for proof purposes, we could have described our algorithm as a source-to-source transformation on the lazy language. Indeed this was done in an early version of this work, but the transformation rules were far more complex than those presented here. Also, in the strict language closures are exactly the elements of lifted types; in the lazy language the correspondence is not as precise. The strict language is also well suited to the description of sequential computations; failure of any evaluation causes failure of the whole machine. This language may also be used as an interface to existing compilers.

A translation to a strict language driven by strictness analysis is also used by Faxén [9], but there only simple strictness is used. Thunk elimination and unboxing are performed at a later stage using a type-based flow inference [8].

In Sect. 4, we show how the contexts of conventional projection analysis may be factored as embedding-projection pairs. The embedding components, being total functions, are described by the lazy language, while the projection components, being partial, are described in the strict language.

The rules of our translation algorithm are given in Sect. 5, with some examples. Section 6 concludes.

Types  t = ∅ | 1l | t × t | t + t | t_{⊥} | a | μ a. t
Definitions def = f_{d} =^{△} λ x. e
Expressions e = x | ⊥ | () | (e_{1}, e_{2}) | f e
| case e of inl x_{1} ⇒ e_{1} [] inr x_{2} ⇒ e_{2}
| case e of lift x ⇒ e′
Functions  f = f_{d}
| λ x. e
| fst | snd | inl | inr | lift | id | empty

Fig. 1. First-order lazy functional language

products : Num_{⊥} × List Num_{⊥} → List Num_{⊥}

products (x, ys) =^{△} case ys of lift n ⇒ case n of inl () ⇒ lift (inl ()) [] inr (y, ys′) ⇒ let x′ =^{△} x ∗ y in lift (inr (x′, products (x′, ys′)))

append : ∀ a. List a × List a → List a

append (xs, ys) =^{△} case xs of lift n ⇒ case n of inl () ⇒ ys [] inr (x, xs′) ⇒ lift (inr (x, append (xs′, ys)))

Fig. 2. Example lazy functions

2 A First-order Lazy Language

The source language of our translation algorithm is a simple first-order lazy functional language, whose grammar is given in Fig. 1. This language is the first-order fragment of the language of [16]. The most unusual feature is that not all types have a least element ⊥. For example, we shall see below that sums are disjoint unions, and we shall later introduce flat types of numbers and so on.

A type is said to be pointed if it has a least element ⊥. The type 1l is pointed; t_{1} × t_{2} is pointed if both t_{1} and t_{2} are; t_{⊥} is always pointed; μ a. t is pointed if t is pointed for any a. Note that t_{1} +t_{2} is never pointed; nor is ∅. The result types of recursive functions, of case e of lift x ⇒ e′, and of ⊥ itself, are required be pointed.

Recursive types are considered to be equivalent to their unfoldings. Recursive forms whose initial solution is empty, like μ c. a × c, are forbidden. For example, the list type constructor is defined by

List a =^{△} μ c. (1l + a × c)_{⊥}

Figure 2 contains some example of functions written in this language. (We have used a little syntactic sugar to render the pattern matching more readable.) The function products is a typical stream processor, mapping a list of numbers to a list of partial products.

Instead of giving a denotational semantics for the language, we shall give a series of axioms that it satisfies. Firstly, the empty type ∅ has no elements:

∀ x : ∅. false

There is however a function empty : ∀ a. ∅ → a.

Next, the unit type 1l has a single element ():

∀ x : 1l. x = ()

The product type constructor describes a true product:

fst (x, y) = x  snd (x, y) = y  ∀ p : a × b. p = (fst p, snd p)

The sum type constructor makes disjoint unions:

(case inl x of inl x′ ⇒ e_{1} [] inr y′ ⇒ e_{2}) = e_{1}[x′ ↦ x]
(case inr y of inl x′ ⇒ e_{1} [] inr y′ ⇒ e_{2}) = e_{2}[y′ ↦ y]
∀ z : a + b. (∃ x : a. z = inl x) ∨ (∃ y : b. z = inr y)

Lifted types have constructors ⊥ and lift : ∀ a. a → a_{⊥}:

(case ⊥ of lift y ⇒ e) = ⊥

(case lift x of lift y ⇒ e) = e[y ↦ x] ∀ z : a_{⊥}. (z = ⊥) ∨ (∃ x : a. z = lift x)

Finally, we assume β- and η-equivalence for functions, and that recursive definitions support unfolding and Scott induction.

Some abbreviations will be convenient. We write let x =^{△} e in e′ for (λ x. e′) e, and f ∘g for λ x. f (g x). There are operators on functions corresponding to type constructors:

f_{1} × f_{2} = λ z. (f_{1} (fst z), f_{2} (snd z))
f_{1} + f_{2} = λ z. case z of inl x_{1} ⇒ inl (f_{1} x_{1}) [] inr x_{2} ⇒ inr (f_{2} x_{2})
f_{⊥} = λ z. case z of lift x ⇒ lift (f x)

These operators preserve id and composition, i.e. they are functors.

3 A First-order Strict Language

The target language of the strictness translation is a first-order strict functional language, given in Fig. 3. The domain types of this language are identical to those of the lazy language, but there are no pointedness restrictions. Lifted types t_{⊥}

Definitions def = p_{d} =^{△} λ x. v
Expressions v = x | ⊥ | () | (v_{1}, v_{2}) | p v
| case v of inl x_{1} ⇒ v_{1} [] inr x_{2} ⇒ v_{2}
| delay v
Partial  p = p_{d}
functions  | λ x. v
| fst | snd | inl | inr | id | force

Fig. 3. First-order strict functional language

\begin{aligned}[ \\ [ & p_{d} =^{△} λ x. v & ] \\ & ] \end{aligned} = p_{d} =^{△} \begin{aligned}[ \\ [ & λ x. v & ] \\ & ] \end{aligned}
\begin{aligned}[ \\ [ & p_{d} & ] \\ & ] \end{aligned} = p_{d}
\begin{aligned}[ \\ [ & λ x. v & ] \\ & ] \end{aligned} = λ x. \begin{aligned}[ \\ [ & v & ] \\ & ] \end{aligned}
[ [fst] ] = lift ∘ fst
[ [snd] ] = lift ∘ snd
[ [inl] ] = lift ∘ inl
[ [inr] ] = lift ∘ inr
[ [force] ] = id
[ [id] ] = lift

\begin{matrix}[ \\ [ & x & ] \\ ] \end{matrix} = lift x
\begin{matrix}[ \\ [ & ⊥ & ] \\ ] \end{matrix} = ⊥
[ [()] ] = lift ()

\begin{matrix}[ \\ [ & (v_{1}, v_{2}) & ] \\ ] \end{matrix} = case \begin{aligned}[ \\ [ & v_{1} & ] \\ & ] \end{aligned} of lift x_{1} ⇒

case \begin{aligned}[ \\ [ & v_{2} & ] \\ & ] \end{aligned} of lift x_{2} ⇒
lift (x_{1}, x_{2})
\begin{aligned}[ \\ [ & p v & ] \\ & ] \end{aligned} = case \begin{aligned}[ \\ [ & v & ] \\ & ] \end{aligned} of lift x ⇒ \begin{matrix}[ \\ [ & p & ] \\ ] \end{matrix} x

[

[case v of inl x_{1} ⇒ v_{1} [] inr x_{2} ⇒ v_{2}]

]

= case \begin{aligned}[ \\ [ & v & ] \\ & ] \end{aligned} of lift y ⇒

case y of \begin{matrix}inl x_{1} ⇒ \begin{aligned}[ \\ [ & v_{1} & ] \\ & ] \end{aligned} [] \\ inr x_{2} ⇒ \begin{aligned}[ \\ [ & v_{2} & ] \\ & ] \end{aligned} \end{matrix}

\begin{aligned}[ \\ [ & delay v & ] \\ & ] \end{aligned} = lift (\begin{matrix}[ \\ [ & v & ] \\ & ] \end{matrix})

Fig. 4. Semantics of the strict language

have a special role in this language, representing the types of closures. These are built by the delay construct, and their values demanded by the function force : ∀ a. a_{⊥} → a, as in Scheme [5].

The semantics of this language is given in Fig. 4 via a translation into the lazy language, corresponding to the standard denotational semantics of strict languages. Strict computations of type t are modelled by lazy expressions of type t_{⊥}. Thus partial functions, whose types we write as t ∘→ t′, are translated to lazy functions of type t → t′_{⊥}.

In the strict language we use abbreviations like those for the lazy language. We write let x =^{△} v in v′ for (λ x. v′) v, and p ∘ q for λ x. p (q x). The strict language also has operators (functors) preserving id and composition:

p_{1} × p_{2} = λ z. (p_{1} (fst z), p_{2} (snd z))
p_{1} + p_{2} = λ z. case z of inl x_{1} ⇒ inl (p_{1} x_{1}) [] inr x_{2} ⇒ inr (p_{2} x_{2})
p_{⊥} = λ z. delay (p (force z))

Ide = ⟨id  , id  ⟩ :  a ⊴ a
Abs = ⟨λ (). ⊥ , λ x. () ⟩ :  1l ⊴ a
Fail = ⟨empty , λ x. ⊥ ⟩ :  ∅ ⊴ a
α × β = ⟨α^{E} × β^{E}, α^{P} × β^{P} ⟩ : t′_{α} × t′_{β} ⊴ t_{α} × t_{β}
α + β = ⟨α^{E} + β^{E}, α^{P} + β^{P} ⟩ : t′_{α} + t′_{β} ⊴ t_{α} + t_{β}
α_{⊥} = ⟨α^{E}_{⊥} , α^{P}_{⊥} ⟩ : t′_{α}_{⊥} ⊴ t_{α}_{⊥}
α\begin{matrix}⊥ \\ ◯ \end{matrix} = ⟨lift ∘ α^{E} , α^{P} ∘ force⟩ :  t′_{α} ⊴ t_{α}_{⊥}
Fig. 5. Embedding-projection pairs (given α : t′_{α} ⊴ t_{α} and β : t′_{β} ⊴ t_{β})

4 Embedding-projection Pairs

We need to analyse each projection α : t ∘→ t used in strictness analysis [13] as an e-p pair ⟨α^{E} : t′ → t, α^{P} : t ∘→ t′⟩ such that α = α^{E}_{⊥} ∘ [[α^{P}]]. That is, the embedding component is a total function, described in the language of lazy functions, while the projection component is a partial function, described in the language of strict functions. We shall identify α with this pair relating a type t with a reduced representation t′. We write α : t′ ⊴ t for this factorization.

The primitive e-p pairs and constructors are listed in Fig. 5.

The trivial e-p pair is the identity Ide, which embeds any type in itself.

The context Abs (absent) is used to indicate that a value is unused, so any value will do, and we may as well implement it using the unit type 1l (a form of dead code elimination). Note that Abs^{E} is only defined for pointed types, while Abs^{P} is defined for all types.

The context Fail is used to indicate that no value is acceptable. Such a value may be represented using the empty type.

We define the composition of e-p pairs α : t′ ⊴ t and β : t′′ ⊴ t′ as

α ∘ β = ⟨α^{E} ∘ β^{E}, β^{P} ∘ α^{P}⟩ : t′′ ⊴ t

The above e-p pairs satisfy the following equations:

α = α ∘ Ide = Ide ∘ α  (5)
Abs = α ∘ Abs if [[α^{P}]] is total (6)
Fail = α ∘ Fail  (7)

Next are the operators corresponding to the type constructors ×, + (unlifted sum) and ·_{⊥}. By construction, these operations on e-p pairs preserve Ide and composition.

Liftings are eliminated (performing unboxing) by the variant ·_{⊥ ◯} of ·_{⊥}. This operator is not functorial; its action on Ide is the strictness projection:

Str = Ide_{⊥ ◯} = ⟨lift, force⟩

The e-p pair corresponding to the projection Both is Str × Str.

The interaction of the ·_{⊥ ◯} operator with composition is given by the following equations:

(α ∘ β)_{⊥ ◯} = α_{⊥ ◯} ∘ β  (8)
(α ∘ β)_{⊥ ◯} = α_{⊥} ∘ β_{⊥ ◯}  (9)

For example, the operation on e-p pairs corresponding to List is

List α =^{△} (1l + α × List α)_{⊥}

Often we will want to talk about lists in a strict context, so we use the active variant

List! α =^{△} (1l + α × List α)_{⊥ ◯}

It would also be possible to eliminate the liftings in the recursive types, giving a context describing tail (or spine) strictness:

Tail α =^{△} (1l + α × Tail α)_{⊥ ◯}

However, this kind of unboxing is not always a good idea, as the early evaluation of the whole list may use a great deal of space.

In order to be able to use the fixpoint methods developed for strictness analysis, we need to limit ourselves to a finite set of contexts. In the rest of this paper, we shall use contexts built from Abs, Fail and variables ranging over contexts using ×, +, ·_{⊥} and ·_{⊥ ◯}. We shall only unfold recursive contexts to one level, as we did with List above. We shall also introduce flat data types, like Num, whose associated contexts are instances of Ide.

4.1 Upper Bounds of Projections

There is a natural ordering on contexts, extending the ordering on simple projections: we write η : α ⊑ β for α = β ∘ η. When we do not need to refer to η, we simply write α ⊑ β. A smaller e-p pair in this ordering represents less boxing, and is therefore more desirable.

In some of the rules of projection analysis, we require a context β greater than each of a pair of argument contexts α_{1} and α_{2}. The actions on projections are the usual approximate answers [13] built from the primitive contexts and operators of Fig. 5. However, we also require e-p pairs η_{i} : α_{i} ⊑ β to act as witnesses to the orderings, and to mediate between the representations. Since the approximations are defined by syntactic matching of the context terms, the necessary e-p pairs follow from various equations above, as in Fig. 6.

5 Translation from the Lazy Language

The translation of a lazy function f in a context β will be defined by a theorem of the form

[[β^{P}]] ∘ f = [[p ∘ α^{P}]]

Ide : α ⊑ α α : α ⊑ Ide

[[α^{P}]] is total ⇒ Abs : Abs ⊑ α

Fail : Fail ⊑ α

η_{1} : α_{1} ⊑ β_{1} ∧ η_{2} : α_{2} ⊑ β_{2} ⇒ η_{1} × η_{2} : α_{1} × α_{2} ⊑ β_{1} × β_{2}
η_{1} : α_{1} ⊑ β_{1} ∧ η_{2} : α_{2} ⊑ β_{2} ⇒ η_{1} + η_{2} : α_{1} + α_{2} ⊑ β_{1} + β_{2}
η : α ⊑ β ⇒ η_{⊥} : α_{⊥} ⊑ β_{⊥}
η : α ⊑ β ⇒ η : α\begin{matrix}⊥ \\ ◯ \end{matrix} ⊑ β\begin{matrix}⊥ \\ ◯ \end{matrix}
η : α ⊑ β ⇒ η\begin{matrix}⊥ \\ ◯ \end{matrix} : α\begin{matrix}⊥ \\ ◯ \end{matrix} ⊑ β_{⊥}

Fig. 6. Rules for context orderings

where p is a partial function in the strict language and α is an e-p pair.

The simplest case, corresponding to the transformation discussed by Peyton Jones and Launchbury [19], is where β is Str. This corresponds to the common observation that “an expression is never evaluated unless its value is required in WHNF”. Since [[Str^{P}]] = id, the left side of the above equation reduces to f. In their terminology, the function f is defined as a wrapper performing unboxing of the arguments (via the projection α^{P}) for a worker function p. For example, we assume that the multiplication function is supplied with a translation

[[Num_{⊥ ◯}^{P}]] ∘ (∗) = \begin{aligned}[ \\ [ & (∗) ∘ (Num_{⊥ ◯} × Num_{⊥ ◯})^{P} & ] \\ & ] \end{aligned}

stating that it is strict.

Often the context will be more interesting—in the above example the argument of f will be evaluated in the context α. The environment of the program may also imply a more informative context. For example, in a stream-producing computation the outer context will be both strict and head-strict.

The lazy functions of Fig. 2 interact in interesting ways with latent demand. In different contexts, products translates to different partial functions, both defined in Fig. 7:

[ [(List! Num_{⊥})^{P}] ] ∘ products

= [

[products_{1} ∘ (Num_{⊥} × List! Num_{⊥})^{P}]

]
[ [(List! Num_{⊥ ◯})^{P}] ] ∘ products

= [

[products_{2} ∘ (Num_{⊥ ◯} × List! Num_{⊥ ◯})^{P}]

]

In the first case, products is used in a completely lazy context, and the resulting program must build closures for both x′ and the tail of the list, just like the original. In a head-strict context, products is compiled to a different version that performs the multiplication immediately, but still builds a closure for the tail. Further, products_{2} expects as arguments an unboxed number and a list of unboxed numbers.

In contrast, a single translation of append suffices for all contexts List! α:

\begin{aligned}[ \\ [ & (List! α)^{P} & ] \\ & ] \end{aligned} ∘ append

= [

[append_{1} ∘ (List! α × List α)^{P}]

]

type List! a =^{△} 1l + a × List a

products_{1} : Num_{⊥} × List! Num_{⊥} ∘→ List! Num_{⊥} products_{1} (x, n) =^{△} case n of inl () ⇒ inl () [] inr (y, ys) ⇒ let x′ =^{△} delay (force x ∗ force y) in inr (x′, delay (products_{1} (x′, force ys)))

products_{2} : Num × List! Num ∘→ List! Num products_{2} (x, n) =^{△} case n of inl () ⇒ inl () [] inr (y, ys) ⇒ let x′ =^{△} x ∗ y in inr (x′, delay (products_{2} (x′, force ys)))

append_{1} : ∀ a. List! a × List a ∘→ List! a append_{1} (n, ys) =^{△} case n of inl () ⇒ force ys [] inr (x, xs) ⇒ inr (x, delay (append_{1} (force xs, ys)))

Fig. 7. Partial functions generated by the translation

Note that append_{1} is essentially the same as append—the unboxing projections are pushed straight through it onto its arguments.

Similar translations were achieved by the informally verified algorithm of Hall and Wise [10]. They use a single data type, which would be written in the notation of this paper as

Structure =^{△} μ c. (Atom + c × c)_{⊥}

where Atom is an unpointed set (including nil and numbers). Strictness is described by strictness patterns, which are equivalent (though with the inverse ordering) to certain contexts over Structure. Their outer strictness pattern corresponds to

Printer! =^{△} (Atom + Printer! × Printer)_{⊥ ◯}
Printer =^{△} (Atom + Printer! × Printer)_{⊥}

They use an infinite domain of contexts, requiring the user to limit the number of versions of a function that may be generated.

5.1 Translation Rules

The rules of the backward analysis correspond to the rules of the conventional analysis [20,13]; what is new here is the translations.

The translations of the primitive functions are given in Fig. 8. These theorems follow from the axioms of Sect. 2, but the proofs are omitted here. Note that lift may also occur in a context of the form α_{⊥}; this case is covered by rule (20), to be discussed later.

[[α^{P}]] ∘ fst = \begin{aligned}[ \\ [ & fst ∘ (α × Abs)^{P} & ] \\ & ] \end{aligned}
[[α^{P}]] ∘ snd = \begin{aligned}[ \\ [ & snd ∘ (Abs × α)^{P} & ] \\ & ] \end{aligned}
\begin{aligned}[ \\ [ & (α + β)^{P} & ] \\ & ] \end{aligned} ∘ inl = [[inl ∘ α^{P}]]
\begin{aligned}[ \\ [ & (α + β)^{P} & ] \\ & ] \end{aligned} ∘ inr = [[inr ∘ β^{P}]]

[[α\begin{matrix}⊥ \\ ◯ \end{matrix}^{P}]] ∘ lift = [[id ∘ α^{P}]]
[[α^{P}]] ∘ id = [[id ∘ α^{P}]]
[[α^{P}]] ∘ empty = [[id ∘ Fail^{P}]]

Fig. 8. Translations of pre-defined functions

The translation of an expression e in a context β is described by a theorem of the form

[[β^{P}]] e = [[v ⊲ ρ^{P}]]

for some translated expression v and environment ρ. The ⊲ operator, applied to an environment π mapping variables x : t to call-by-value functions π_{x} : t′ ∘→ t, is the following abbreviation:

v ⊲ π = let x_{1} =^{△} π_{x_{1}} x_{1} in … let x_{n} =^{△} π_{x_{n}} x_{n} in v

We write \overline{α} for the context environment mapping each variable to the context α.

Figure 9 contains inference rules for every combination of context and expression permitted by the type constraints of our language. The soundness of these follows from the axioms of Sect. 2, but the rules may also be read as a directed logic program.

The first two rules should be given precedence over the others, as they may produce superior results. First, a context of Abs indicates that any value will do, so we use the unit type instead. A context of Fail indicates that no value will do, so the empty type is a suitable representation.

The environment of variable values may be viewed as a product, and variables as projections. Hence their translation (12) is similar to fst and snd in Fig. 8.

If ⊥ occurs in a strict context, no value for the free variables will do.

To compile a pair, we must combine the demands of the two components. On each variable, we will have a pair of e-p pairs α : t_{α} ⊴ t and β : t_{β} ⊴ t. We require an e-p pair γ : t_{γ} ⊴ t and call-by-value functions θ^{L} : t_{γ} ∘→ t_{α} and θ^{R} : t_{γ} ∘→ t_{β} such that

(α^{P} x, β^{P} x) = let x′ =^{△} γ^{P} x in (θ^{L} x′, θ^{R} x′)

When this equation holds, we write ⟨γ, θ^{L}, θ^{R}⟩ ∈ α & β. As with the upper bound calculations, we can use the approximations for γ supplied by conventional projection analysis, but we also need the θ’s. In Fig. 10, we go through all the rules for & [13] and calculate the θ’s. Note the fall-back rule; the other rules give better answers where they apply, but this covers cases like α_{⊥} & β_{⊥}. Recursive types can be handled in the same way as for ordinary projections [13].

Applications of primitive or user-defined functions are translated using (16). Applications of λ-expressions, i.e. let definitions, are translated using (17). The latter uses & because a let definition makes non-linear use of its environment, like the pairing construct.

[[Abs^{P}]] e = \begin{aligned}[ \\ [ & () ⊲ \overline{Abs}^{P} & ] \\ & ] \end{aligned}  (10)
[[Fail^{P}]] e = \begin{aligned}[ \\ [ & ⊥ ⊲ \overline{Fail}^{P} & ] \\ & ] \end{aligned}  (11)
[[β^{P}]] x = \begin{aligned}[ \\ [ & x ⊲ (\overline{Abs}[x ↦ β])^{P} & ] \\ & ] \end{aligned}  (12)
[[β^{P}]] ⊥ = \begin{aligned}[ \\ [ & ⊥ ⊲ \overline{Fail}^{P} & ] \\ & ] \end{aligned}  [[β^{P}]] strict  (13)
[[β^{P}]] () = \begin{aligned}[ \\ [ & () ⊲ \overline{Abs}^{P} & ] \\ & ] \end{aligned}  (14)
\frac{[[β_{i}^{P}]] e_{i} = [[v_{i} ⊲ ρ_{i}^{P}]]  ⟨ρ, θ^{L}, θ^{R}⟩ ∈ ρ_{1} & ρ_{2}}{[[β_{1} × β_{2}^{P}]] (e_{1}, e_{2}) = [[(v_{1} ⊲ θ^{L}, v_{2} ⊲ θ^{R}) ⊲ ρ^{P}]]}  (15)

\frac{[[β^{P}]] ∘ f = [[p ∘ α^{P}]]  [[α^{P}]] e = [[v ⊲ ρ^{P}]]}{[[β^{P}]] (f e) = [[(p v) ⊲ ρ^{P}]]}  (16)

\frac{[[β^{P}]] e_{2} = [[v_{2} ⊲ ρ_{2}^{P}]]  [[ρ_{2}_{x}^{P}]] e_{1} = [[v_{1} ⊲ ρ_{1}^{P}]]  ⟨ρ, θ^{L}, θ^{R}⟩ ∈ ρ_{1} &(ρ_{2}\x)}{[[β^{P}]] (let x =^{△} e_{1} in e_{2}) = [ [(let x =^{△} v_{1} ⊲ θ^{L} in v_{2} ⊲ θ^{R}) ⊲ ρ^{P}] ]} (17)

\frac{[[β^{P}]] e_{i} = [[v_{i} ⊲ ρ_{i}^{P}]]  α_{i} = ρ_{i}_{y_{i}}  η_{i} : ρ_{i}\y_{i} ⊑ ρ}{[[β^{P}]] (\begin{matrix}case x of \\ inl y_{1} ⇒ e_{1} [] \\ inr y_{2} ⇒ e_{2} \end{matrix}) = [ [(\begin{matrix}case x of \\ inl y_{1} ⇒ v_{1} ⊲ η_{1}^{P} [] \\ inr y_{2} ⇒ v_{2} ⊲ η_{2}^{P} \end{matrix}) ⊲ (ρ[x ↦ α_{1} + α_{2}])^{P} ] ]}

x not free in e_{1}, e_{2}

(18)

\frac{[[β^{P}]] e = [[v ⊲ ρ^{P}]]  α = ρ_{y}}{[[β^{P}]] (case x of lift y ⇒ e) = \begin{aligned}[ \\ [ & v ⊲ ((ρ\y)[x ↦ α\begin{matrix}⊥ \\ ◯ \end{matrix}])^{P} & ] \\ & ] \end{aligned}}  [[β^{P}]] strict x not free in e (19)

\frac{[[β\begin{matrix}⊥ \\ ◯ \end{matrix}^{P}]] e = [[v ⊲ ρ^{P}]]  η : ρ ⊑ ρ′  \overline{Abs} ⊑ ρ′}{[[β_{⊥}^{P}]] e = \begin{aligned}[ \\ [ & delay (v ⊲ η^{P}) ⊲ ρ′^{P} & ] \\ & ] \end{aligned}}  (20)

Fig. 9. Translation rules for expressions

⟨α, id, id⟩ ∈ α & α  ⟨α, id, λ x. ()⟩ ∈ α & Abs  ⟨Fail, λ x. ⊥, λ x. ⊥⟩ ∈ α & Fail

\frac{⟨γ_{1}, θ1^{L}, θ1^{R}⟩ ∈ α_{1} & β_{1} ⟨γ_{2}, θ2^{L}, θ2^{R}⟩ ∈ α_{2} & β_{2}}{⟨γ_{1} × γ_{2}, θ1^{L} × θ2^{L}, θ1^{R} × θ2^{R}⟩ ∈ (α_{1} × α_{2}) &(β_{1} × β_{2})}

\frac{⟨γ_{1}, θ1^{L}, θ1^{R}⟩ ∈ α_{1} & β_{1} ⟨γ_{2}, θ2^{L}, θ2^{R}⟩ ∈ α_{2} & β_{2}}{⟨γ_{1} + γ_{2}, θ1^{L} + θ2^{L}, θ1^{R} + θ2^{R}⟩ ∈ (α_{1} + α_{2}) &(β_{1} + β_{2})}

\frac{⟨γ, θ^{L}, θ^{R}⟩ ∈ α & β}{⟨γ\begin{matrix}⊥ \\ ◯ \end{matrix}, θ^{L}, θ^{R}⟩ ∈ α\begin{matrix}⊥ \\ ◯ \end{matrix} & β\begin{matrix}⊥ \\ ◯ \end{matrix}}  \frac{α ⊑ γ  η : β ⊑ γ  ⟨δ, θ^{L}, θ^{R}⟩ ∈ α & γ}{⟨δ\begin{matrix}⊥ \\ ◯ \end{matrix}, θ^{L}, (λ z. delay (η^{P} z)) ∘ θ^{R}⟩ ∈ α\begin{matrix}⊥ \\ ◯ \end{matrix} & β_{⊥}}

\frac{η_{1} : α ⊑ γ  η_{2} : β ⊑ γ}{⟨γ, η_{1}^{P}, η_{2}^{P}⟩ ∈ α & β}  (used if no other rule applies)

Fig. 10. Rules for the & operation

Equations (18) and (19) cover only restricted forms, where the expression being analysed is a variable that does not occur free in the body of the case. In this way we avoid aliasing, giving simpler rules. However, no generality is lost, as any case expression may be re-written in this form using a let.

5.2 Active and Latent Contexts

Equations (13) and (19) have an extra side condition: the function [[β^{P}]] must be strict, corresponding to a context in which the value is demanded.

A similar restriction arises in the translation of recursive functions. A function f =^{△} λ x. e will be translated to a different partial function p for each context β. Since our contexts correspond to those of ordinary projection analysis [20,13], we can use standard fixed point methods to compute the input context α for the required contexts β, and then read off the associated translation p for a particular β. Now the equations [[β^{P}]] ∘ f = [[p ∘ α^{P}]] are inductive, so they will hold for the fixed point functions if [[β^{P}]] is strict.

For example, γ_{⊥ ◯} has a strict projection component, while γ_{⊥} does not. Recall that the translation of lift in Fig. 8 also requires the strict form.

Wadler and Hughes [20] made all contexts strict by introducing a guard rule. We shall only do this where required by the above rules. They may be extended to contexts of the form β_{⊥} using (20). That is, create a boxed closure, whose code evaluates v in an active context.

In most accounts of strictness analysis, all values are assumed to be of lifted type, so (20) covers all cases. In our lazy language, we require of the result type of the evaluation only that it be pointed. Hence it cannot be a sum, but it may be a product of pointed types. Now the context γ × δ has a strict projection component if either of γ or δ have. Otherwise, in a context γ × δ we can rewrite an evaluation using the equation

case x of lift y ⇒ e = let z =^{△} (case x of lift y ⇒ lift e) in (\begin{matrix}case z of lift p ⇒ fst p, \\ case z of lift p ⇒ snd p) \end{matrix}

(21)

In the expression on the right-hand side, the first case is of lifted type, and thus will have a tractable context. The other two case have contexts γ and δ, which we treat inductively. The generated code for such fully latent pairs will not be efficient, but the programmer has left us little choice.

A similar device may be applied to recursively defined functions.

5.3 Polymorphism

Since our language allows expressions of pointed types in these positions, the other possibility is that the result type of an evaluation or recursive function is a type variable, constrained to pointed types. Such a case must be treated by instantiation of the type variable, creating a context more specific than the type of the expression.

Instantiation is also required in the calculation of certain upper bounds of contexts. This is because Fig. 6 gives no general rule for an upper bound of α and Abs.

However, if we constrain the language so that the types of these expressions must be products of lifted types, then our translation procedure will be polymorphic. Even this restriction is less stringent than the situation in languages like Haskell [11], where all expressions are of lifted type.

6 Conclusion

We have developed an algorithm to compile lazy functions to call-by-value forms. By basing the algorithm on projection-based strictness analysis, we were able to make use of latent demand information in the translation. Moreover, the rules of our algorithm are formulas over a simple functional language, and are hence easily verified.

The key step was factoring of the projections as embedding-projection pairs. In the present paper, we used only the projection components in a backwards analysis to expose strictness and perform unboxing. It is also possible (indeed simpler) to define a forwards analysis using the embeddings, delaying creation of closures, possibly permanently. It is also possible that other analyses using projections may benefit from factorization.

The principal shortcoming of our algorithm is inherited from the analysis on which it is based: it is limited to first-order functions. This is an obvious area for future work, perhaps using one of the higher-order extensions of projection analysis [7,12].

Acknowledgements

John Launchbury suggested that an explicit treatment of lifting might enable the exploitation of projection-based strictness analysis. John Hughes, David Sands and anonymous referees gave suggestions for the presentation of this work. Nurith Goldblatt found some technical errors.

References

1. Torben Amtoft. Minimal thunkification. In Patrick Cousot et al., editors, Static Analysis: 3rd International Workshop, WSA ’93, Padova, Italy, volume 724 of Lecture Notes in Computer Science, pages 218–229. Springer, 1993.

2. Andrew A. Appel. Compiling with Continuations. Cambridge University Press, 1992.

3. Geoffrey L. Burn, Chris Hankin, and Samson Abramsky. Strictness analysis of higher order functions. Science of Computer Programming, 7:249–278, 1986.

4. Geoffrey L. Burn and Daniel Le Métayer. Proving the correctness of compiler optimisations based on a global program analysis. In Fifth International Symposium on Programming Language Implementation and Logic Programming, volume 714 of Lecture Notes in Computer Science, pages 346–364, Tallinn, Estonia, August 1993. Springer.

5. W. Clinger and J. Rees. Revised^{4} report on the algorithmic language Scheme. ACM Lisp Pointers, IV, July–September 1991.

6. Olivier Danvy and John Hatcliff. CPS-transformation after strictness analysis. ACM Letters on Programming Languages and Systems, 1(3):195–212, 1992.

7. Kei Davis and Philip Wadler. Strictness analysis in 4D. In 1990 Glasgow Workshop on Functional Programming, Workshops in Computing, pages 23–43. Springer, 1991.

8. Karl-Filip Faxén. Optimizing lazy functional programs using flow inference. In Static Analysis, Second International Symposium, volume 983 of Lecture Notes in Computer Science, pages 136–153. Springer, 1995.

9. Karl-Filip Faxén. Flow inference, code generation and garbage collection for lazy functional languages. Licentiate thesis, Kungl Tekniska Högskolan, January 1996.

10. Cordelia V. Hall and David S. Wise. Compiling strictness into streams. In 14th ACM Symposium on Principles of Programming Languages, pages 132–143, Munich, January 1987.

11. Paul Hudak, Simon Peyton Jones, Philip Wadler, et al. Report on the programming language Haskell, a non-strict purely functional language (Version 1.2). SIGPLAN Notices, 27(5), March 1992.

12. Sebastian Hunt. Abstract Interpretation of Functional Languages: From Theory to Practice. PhD thesis, Imperial College of Science, Technology and Medicine, 1991.

13. Ryszard Kubiak, John Hughes, and John Launchbury. Implementing projectionbased strictness analysis. In 1991 Glasgow Workshop on Functional Programming, Workshops in Computing, pages 207–224. Springer, 1992.

14. T-M. Kuo and P. Mishra. Strictness analysis: A new perspective based on type inference. In FPCA’89, London, England, pages 260–272. ACM Press, September 1989.

15. John Launchbury and Gebreselassie Baraki. Representing demand by partial projections. Journal of Functional Programming, 6(4), 1996.

16. John Launchbury and Ross Paterson. Parametricity and unboxing with unpointed types. In European Symposium on Programming, volume 1058 of Lecture Notes in Computer Science, pages 204–218, Linköping, Sweden, April 1996.

17. Alan Mycroft. The theory and practice of transforming call-by-need into call-by-value. In B. Robinet, editor, International Symposium on Programming, volume 83 of Lecture Notes in Computer Science. Springer, 1980.

18. Simon L. Peyton Jones. Implementing lazy functional languages on stock hardware: the spineless tagless G-machine. Journal of Functional Programming, 2(2):127–202, July 1992.

19. Simon L. Peyton Jones and John Launchbury. Unboxed values as first class citizens in a non-strict functional language. In Conference on Functional Programming Languages and Computer Architecture, pages 636–666, Cambridge, MA, 1991.

20. Philip Wadler and John Hughes. Projections for strictness analysis. In Conference on Functional Programming Languages and Computer Architecture, volume 274 of Lecture Notes in Computer Science, Portland, OR, 1987.