Transforming Lazy Functions using Comportment Properties

Ross Paterson

University of North London

Abstract. This paper develops a source-to-source transformation that seeks to delay the creation of thunks as much as possible, often eliminating them altogether. The generated programs make use of simpler representations, including types in which all expressions terminate. The transformation is guided by an abstract interpretation, with the abstract values of basic comportment analysis concretized as representation types related by injections. The transformation of functions is polyvariant, with functions mapped to natural transformations. This leads to a clean treatment of higher order functions. Keywords: static analysis, abstract interpretation, automatic program transformation

1 Introduction

If a function is lazy, its argument must be passed as a suspended computation, or thunk. This object is typically created on the heap, or boxed, and the function using it must inspect the thunk to determine whether it has been evaluated. It has long been recognized that these thunks are a major obstacle to the application of conventional compiler technology to lazy functional languages. They have been attacked using strictness analysis [9], which determines that certain sub-expressions must be evaluated in order to produce the final output. Instead of being suspended, such expressions may be safely evaluated early, and their values passed in an unboxed form on the stack.

There is also a dual approach, known as termination analysis, which determines that certain sub-expressions will have been evaluated by a certain point. If we know that an argument of a function will have been evaluated by the time the function is called, we can pass the argument in unboxed form to a call-by-value variant of the function (even if the function is not strict).

A typical functional language incorporates lazy data structures, and strictness analysis techniques have been developed that produce information about latent demand [14]. Similarly termination analysis may be extended to produce statements about latent termination: though an expression might not terminate, it may be that if it does then its components will also have been evaluated.

The information supplied by these analyses has been used to improve compiler performance, but the changes to the code generator are seldom formally verified. Exceptions include the work of Danvy and Hatcliffe [3] and of Burn and Le Métayer [1], who describe modifications of the continuation-passing transform to incorporate simple strictness information. Paterson [11] defines a transformation based on projection-based strictness analysis. The transformation moves backwards to perform evaluation as early as possible, and as a side-benefit discovers unused components of data structures. The transformation of this paper is dual to that one; it moves forward, delaying boxing as much as possible, and as a side-benefit discovers unused alternatives.

We shall confine our attention to forwards analyses, which may infer that the value of an expression lies within a subset of values, called a comportment property [2]. It is customary to render the analysis tractable by using a finite set of properties, indexed by an abstract domain. For the purposes of simple strictness analysis, it suffices to use properties that are ideals, but in order to encompass other properties, including termination, totality and constancy, this restriction must be dropped.

This paper is concerned with exploiting the results of comportment analysis to transform programs into forms operating on reduced types. For this we require a source language whose type system allows us to express such distinctions as whether or not a type includes the bottom element ⊥. This is routine in denotational semantics; we need only model our source language on the denotational meta-language [8]. An appropriately modified typed λ-calculus is discussed in Sect. 2.

Next we develop concrete representations of basic comportment properties over each type as subtypes, each with an embedding into the original type. As defined by Cousot and Cousot [2], the qualification “basic” indicates that the properties we use are not closed under disjunction (union). Thus we use an approximation of union in the analysis of conditionals, losing some information in comparison with the full-flown comportment analysis. Section 3 presents the easy case of non-functional types. The principal difficulty is with function types, discussed in Sect. 4. Since a function will be specialized in different ways for different input subtypes, we can represent it as a family of related functions, i.e. a natural transformation. The class of natural transformations is sufficiently constrained that it may be embedded in the original function type.

In Sect. 5 we define an abstract interpretation and accompanying source-to-source transformation, which transforms an expression to one of the reduced type. The abstract interpretation is a fairly standard comportment analysis (except for the treatment of fixed points). The novelty is the translation into forms exploiting the subtype representations to achieve greater efficiency. In particular, the creation of closures is delayed as long as possible, and often eliminated.

Our transformation exploits termination properties directly, producing improved representations of values known to terminate, and permitting eager evaluation where it does not harm termination. Strictness properties may be used indirectly, as sketched in Ex. 2 in the next section.

There are some similarities between our work and binding time analysis, which identifies subexpressions whose values will be statically known, given that part of the input will be static. Our abstract interpretation is particularly close to that of Hunt and Sands [7]. However, the transformations we consider are much less ambitious than those performed by specializers using binding time information. On the other hand we use an extended definition of staticness, using static values within dynamic structures. We are also able to transform the program without knowing the values of the static inputs.

2 A Source Language with Explicit Lifting

The denotational semantics of lazy functional programs often refers to a lifting domain constructor A_{⊥}, which adds an additional bottom element to the domain A. For example, a numeric type might be modelled as N_{⊥} for some set N, and a sum type as (A + B)_{⊥}, where + denotes disjoint union. The addition of the bottom element is required to model the possibility of nontermination. The key to thunk removal is a source language modelled on the meta-language, in which this lifting is explicit, and therefore susceptible to transformation [8]. Such a language might serve as a core language, to which a more comfortable source language is translated as a first step in compilation.

We assume a collection of base types A, B, etc, which correspond to flat sets, without a bottom element. Then the types of our language are described by the following grammar:

t ::= B | ∅ | t × t | t + t | t_{⊥} | t → t

Here ∅ represents the empty type, and ×, + and → are unlifted. Note that many types, including base types and sum types, have no bottom element. Any expression of such a type must terminate, and can thus be safely evaluated early instead of being suspended in a thunk. The aim then becomes to transform programs to equivalent programs using types with fewer liftings.

On the other hand, we may not define values by general recursion unless the type concerned is known to have a least element ⊥ and thus support the Kleene definition of fixed points. We define a class of pointed types by stating that t_{⊥} is always pointed, s × t is pointed if both s and t are, and s → t is pointed if t is.^{1}

Our source language is a simply typed λ-calculus, similar to those of [6,8]. We assume the families of constants c^{t} listed in Fig. 1. We also assume a fixed set of constants c^{B_{1}→···B_{n}→B} for base types B_{1}, …, B_{n} and B. Variables x^{t} are also typed, but we will routinely omit the type superscripts on variables and constants where they are irrelevant or may be deduced from the context.

Most of these constants are familiar, as long as one remembers that sums are unlifted. The main novelty lies in the constants lift, fail and ext, which manipulate lifted types, and satisfy the axioms

ext f fail = ⊥  (1)
ext f (lift x) = f x  (2)

1 If t is pointed, then t + ∅ and ∅ + t also have least elements, but we will not be using them here.

empty^{∅→t}  fix^{(t→t)→t} for pointed t
fst^{s×t→s}
snd^{s×t→t}
pair^{s→t→s×t}

inl^{s→s+t}
inr^{t→s+t}
choose^{(s→u)→(t→u)→s+t→u}

fail^{t_{⊥}}
lift^{t→t_{⊥}}
ext^{(s→t)→s_{⊥}→t} for pointed t

Fig. 1. Constants

Operationally, ext f x forces the evaluation of x to weak head normal form, and if this terminates then (tail-) calls f with the result as argument.

We aim to delay the application of lift as long as possible, hoping to cancel it with a subsequent ext. There is some similarity to deforestation [4,13], but here we preserve the structure of the source program.

As the standard interpretation of our language is trivial, we shall proceed by proving equalities in the logic associated with our language. This logic comprises axioms including those above (see [6,8] for details), β- and η-equivalence and Scott induction.

Example 1. Suppose the familiar type Int is expanded as ℤ_{⊥}, for the primitive flat type ℤ representing the integers or some finite approximation. The familiar constants 1, 2, etc. are similarly expanded as lift(1), lift(2) etc. for 1, 2, …: ℤ. Similarly, functions like ∗ : Int → Int → Int are expanded as

x ∗ y =^{△} ext (λ u. ext (λ v. lift (u ⋆ v)) y) x

using a primitive function ⋆ : ℤ → ℤ → ℤ, corresponding to a machine instruction. Similarly, the function λ x. 2 ∗ x might be transformed to

λ x.2 ∗ x = λ x. ext (λ u. ext (λ v. lift (u ⋆ v)) x) (lift 2)
= ext (λ v. lift (2 ⋆ v))

Example 2. Suppose a function f : s_{⊥} → t is discovered to be strict by the analysis discussed here or any other. Then any occurrence of f may be replaced by the term ext (f ∘ lift). Then the transformation of Sect. 5 will promote the lift through f, producing an improved translation. In this way we achieve similar effects to previous approaches in which strictness information had been used to enable local optimizations to remove thunks [5,12].

3 Embeddings of Non-functional Types

In this section and the next we define for each type t a lattice of subtypes of t. In the analysis, this lattice is represented by an abstract domain Dt^{#}, which is a finite lattice under the ordering ⊆^{#}. A concretion mapping C_{t}[·] relates the two lattices. Types that do not contain → are easier to handle, and will be treated first.

Example 3. For the type ℤ_{⊥}, the relevant subtypes are

∅_{⊥}, which can be used for expressions that are known not to terminate, ℤ, which can be used for expressions that are known to terminate, and ℤ_{⊥}, which can be used for any expression.

To complete the lattice, we add the type ∅. These types may be arranged in a lattice, with the inclusions made explicit as embedding functions between subtypes, as on the right side of Fig. 2. The figure also shows the corresponding abstract domain Dℤ_{⊥}^{#} and the concretion map.

[figure: Dℤ_{⊥}^{#}:; ∅^{#}_{□}; ∅^{#}_{□^{⊥}}; ℧^{#}_{□}; ℧^{#}_{□^{⊥}}; C_{ℤ_{⊥}}; ∅; ∅_{⊥}; ℤ; ℤ_{⊥}; empty; empty; empty_{⊥}; lift]

Fig. 2. Abstract domain Dℤ_{⊥}^{#} and lattice of subtypes of ℤ_{⊥}

The rather curious names of the abstract values on the left are explained by the definition of the abstract domains Dt^{#} by induction over t:

– For a base type B (for example ℤ), DB^{#} consists of the two values ∅B^{#} and

℧B^{#}, with ∅^{#} ⊆^{#} ℧^{#}.

– The domain D∅^{#} consists of a single value ∅∅^{#}.

– For any type t, the abstract domain Dt_{⊥}^{#} consists of values α_{□^{⊥}} and α_{□}, for α ∈ Dt^{#}. (The significance of the notation is that the subtype denoted by α_{□^{⊥}} includes the bottom element of t_{⊥}, while the subtype denoted by α_{□} does not.) The constructors ·_{□^{⊥}} and ·_{□} are monotonic, and α_{□} ⊆^{#} α_{□^{⊥}} for each α.

– For types s and t, the abstract domain Ds×t^{#} consists of pairs α ⊠ β for α ∈ Ds^{#} and β ∈ Dt^{#}, such that either both α and β are the least elements of their respective lattices, or neither is (i.e. a smash product). The pairs are ordered pointwise.

– For types s and t, the abstract domain Ds+t^{#} consists of pairs α ⊞ β for α ∈ Ds^{#} and β ∈ Dt^{#}, ordered pointwise.

The concretion maps are also defined by induction on the structure of t, as follows:

C_{B}[℧B^{#}] = B  C_{t_{⊥}}[α_{□^{⊥}}] = (C_{t}[α])_{⊥}
C_{B}[∅B^{#}] = ∅  C_{t_{⊥}}[α_{□}] = C_{t}[α]
C_{∅}[∅∅^{#}] = ∅  C_{s×t}[(α ⊠ β)] = C_{s}[α] × C_{t}[β]
C_{s+t}[(α ⊞ β)] = C_{s}[α] + C_{t}[β]

Each abstract domain Dt^{#} has a least element ∅t^{#}, indicating no values, whose concrete value is a type that is equivalent to ∅. At first glance that this might seem useless, since the abstract interpretation can hardly assign this value to any expression. However ∅t^{#} is useful in compound abstract values. For example, inl produces only values in the left part of a sum type, so the type of its result could be simplified to s + ∅. Similarly, fail produces only the bottom element of a lifted type; the type of its result could be simplified to ∅_{⊥}, and the type being lifted could be simplified to ∅. The abstract version of the product domain is formed using the smash product because we do not wish to have distinct points representing ∅ × ∅ and ∅ × t.

Each abstract domain Dt^{#} also has a greatest element ℧t^{#}. It is easy to establish that if t does not include →, then C_{t}[℧t^{#}] = t, though this will not hold for types including →. For each type t, the concretion map C_{t} maps the abstract domain Dt^{#} to a lattice of subtypes of this type C_{t}[℧t^{#}]. To make this lattice explicit, we define for each α ⊆^{#} α′ in Dt^{#}, a function C_{t}[α ⊆^{#} α′] : C_{t}[α] → C_{t}[α′]. These functions are also defined by induction over t, as in Fig. 3.

C_{t}[α ⊆^{#} α′] : C_{t}[α] → C_{t}[α′]
C_{B}[∅B^{#} ⊆^{#} ∅B^{#}] = empty
C_{B}[℧B^{#} ⊆^{#} ℧B^{#}] = id
C_{B}[∅B^{#} ⊆^{#} ℧B^{#}] = empty
C_{∅}[∅∅^{#} ⊆^{#} ∅∅^{#}] = empty
C_{s×t}[α ⊠ β ⊆^{#} α′ ⊠ β′] = C_{s}[α ⊆^{#} α′] × C_{t}[β ⊆^{#} β′]
C_{s+t}[α ⊞ β ⊆^{#} α′ ⊞ β′] = C_{s}[α ⊆^{#} α′] + C_{t}[β ⊆^{#} β′]
C_{t_{⊥}}[α_{□^{⊥}} ⊆^{#} α′_{□^{⊥}}] = (C_{t}[α ⊆^{#} α′])_{⊥}
C_{t_{⊥}}[α_{□} ⊆^{#} α′_{□^{⊥}}] = lift ∘ C_{t}[α ⊆^{#} α′]
C_{t_{⊥}}[α_{□} ⊆^{#} α′_{□}] = C_{t}[α ⊆^{#} α′]

Fig. 3. Injections between types C_{t}[α]

Proposition 4. For each type t and α ⊆^{#} β ∈ Dt^{#}, the function C_{t}[α ⊆^{#} β] is bimonotone.^{2}

That is, these functions are subspace injections.

Proposition 5. For each type t and α ⊆^{#} β ⊆^{#} γ ∈ Dt^{#},

C_{t}[α ⊆^{#} α] = id_{C_{t}[α]}  (3)
C_{t}[β ⊆^{#} γ] ∘ C_{t}[α ⊆^{#} β] = C_{t}[α ⊆^{#} γ]  (4)

That is, C_{t} is a functor from Dt^{#} to the category of our source language.

3.1 A Note on the Computational Pre-order

In addition to the set-based inclusion ordering (our ⊆^{#}), previous accounts of comportment analysis [2,10] make use of the computational or Egli-Milner ordering for the calculation of fixed points. The requirement that functions also preserve this ordering has the additional benefit of reducing the size of the abstract function domains, making the analysis more tractable.

There is a complication, however: the computational relation between properties is not anti-symmetric. To turn it into an ordering, one must deal with equivalence classes of properties, eliminating the distinction between a property and its convex closure. However we require this distinction for the description of the latent termination properties mentioned in Sect. 1. For example, it may be that we are not sure whether a list-valued expression will terminate, but we know that if it does then the head will not be ⊥. The use of the computational ordering would identify this property with the set of all lists. Hence we require a different definition of fixed points; we shall use the inclusion ordering.

We can however define a computational pre-order ⊑^{#}, using it to restrict the size of the abstract function domains. Since this pre-order has such a minor role, we only sketch it here. In each abstract domain Dt^{#}, the point ∅^{#} is isolated in the ⊑^{#} pre-order. The domains Ds×t^{#} and Ds+t^{#} inherit the pre-order pointwise. The pre-order ⊑^{#} on Dt_{⊥}^{#} is defined by the following rules:

α ≠ ∅^{#} ⇒ α_{□^{⊥}} ⊑^{#} α_{□}
α ⊑^{#} β ⇒ α_{□} ⊑^{#} β_{□}
α ⊑^{#} β ⇒ α_{□^{⊥}} ⊑^{#} β_{□^{⊥}}
α ⊆^{#} β ⇒ α_{□^{⊥}} ⊑^{#} β_{□^{⊥}}

4 Embeddings of Higher Types

So far, our abstract values describe the sets of values that an expression might produce. This cannot be directly extended to functions: while strict functions

2 A function f is bimonotone if x ≤ y ⇔ f x ≤ f y.

ℤ_{⊥} → ℤ_{⊥} are in one-to-one correspondence with elements of the type ℤ → ℤ_{⊥}, and strict total functions may be represented by ℤ → ℤ, no simple representation is available for functions that are merely known to be total.

In analysing a function, we want to know what set of outputs can be produced from a given set of inputs. In all cases the empty set of inputs should produce the empty set of outputs. We also expect that larger sets of inputs will produce larger sets of outputs, and that more defined inputs will produce more defined outputs. Hence we define Ds→t^{#} as the set of functions Ds^{#} → Dt^{#} that preserve ∅^{#} and are monotonic with respect to both ⊆^{#} and ⊑^{#}. Both the order ⊆^{#} and the pre-order ⊑^{#} are extended pointwise to functions.

Example 6. The domain Dℤ_{⊥}→ℤ_{⊥}^{#} has 7 elements, exactly those listed as basic comportments by Cousot and Cousot [2]. We define the abstract functions by their actions on non-∅^{#} elements:

λ α. ℧^{#}_{□^{⊥}}  representing all functions
λ α. ℧^{#}_{□}  constant, total functions
λ α. ∅^{#}_{□^{⊥}}  divergent functions
λ α. α  strict, total functions
λ α. α ∪^{#} ℧^{#}_{□}  total functions
λ α. α ∪^{#} ∅^{#}_{□^{⊥}}  strict functions
λ α. ∅^{#}_{□}  empty

The orderings are exactly as in [2].

Suppose that the abstract interpretation of a function f : s → t yields a function φ ∈ Ds^{#} → Dt^{#}. For each abstract input α, there will be a version f_{α} : C_{s}[α] → C_{t}[φ α]. That is, the transformation is polyvariant.

Example 7. Abstract interpretation of ext (λ u. lift (2 ⋆ u)) : ℤ_{⊥} → ℤ_{⊥} yields the identity function on Dℤ_{⊥}^{#}, indicating that the function is both strict and total. Transformation yields four versions mapping between corresponding subtypes, as shown in Fig. 4. In this case, the transformed functions connect corresponding types in the two lattices because the abstract function was the identity. Other abstract functions will produce different patterns.

The commuting diagram of Fig. 4 is typical of the general situation, for the families of versions will be natural transformations:

C_{s→t}[φ] = C_{s} →^{.} C_{t} ∘ φ

That is, the type C_{s→t}[φ] consists of families of functions f_{α} : C_{s}[α] → C_{t}[φ α] for each α ∈ Ds^{#}, satisfying

f_{α′} ∘ C_{s}[α ⊆^{#} α′] = C_{t}[φ α ⊆^{#} φ α′] ∘ f_{α}  (5)

However, we stipulate that C_{s→t}[∅s→t^{#}] is empty.

[figure: ∅; id; ∅_{⊥}; id; ∅_{⊥}; ℤ; λ u. 2 ⋆ u; ℤ_{⊥}; ext (λ u. lift (2 ⋆ u)); empty; empty; empty_{⊥}; lift]

[figure: ∅; ∅_{⊥}; ℤ; ℤ_{⊥}; empty; empty; empty_{⊥}; lift]
Fig. 4. Transformed versions of ext (λ u. lift (2 ⋆ u)) : ℤ_{⊥} → ℤ_{⊥}

When such a natural transformation f exists, the instance f_{℧^{#}} determines all the others, because each function C_{t}[φ α ⊆^{#} φ α′] is injective. However the existence of f_{℧^{#}} does not guarantee the existence of the natural transformation; our algorithm will construct the whole transformation.

These families will be implemented by iterated products of function types. It is important to note that the abstract domains Dt^{#} will not appear in the transformed program. Selection of a component f_{α} will be represented by extraction of a known position in the tuple of functions. Unless f is a variable, this extraction can be done statically.

If φ ⊆^{#} φ′ in the pointwise ordering, then there is a corresponding injection C_{s→t}[φ ⊆^{#} φ′] between the natural transformations, defined by:

(C_{s→t}[φ ⊆^{#} φ′] f)_{α} = C_{t}[φ α ⊆^{#} φ′ α] ∘ f_{α}

It is straightforward to verify that

– C_{s→t}[φ ⊆^{#} φ′] f is natural,

– C_{s→t}[φ ⊆^{#} φ′] is bimonotone, and

– C_{s→t} is a functor.

With the introduction of function types, the type C_{t}[℧t^{#}] is no longer identical to t. However, it is isomorphic to t.

Proposition 8. For each type t, there is an isomorphism i_{t} : C_{t}[℧t^{#}] ≅ t.

Proof. The required isomorphism is defined by induction over t. This is straightforward except for the case s → t, for which we define

i_{s→t} g = i_{t} ∘ g_{℧^{#}} ∘ i_{s}^{−1}

(i_{s→t}^{−1} f)_{α} = \{ \begin{matrix}empty_{s→t} & if α = ∅s^{#} \\ i_{t}^{−1} ∘ f ∘ i_{s} ∘ C_{s}[α ⊆^{#} ℧s^{#}] & otherwise \end{matrix}

where empty_{s→t} is the unique element of C_{s}[∅s^{#}] → C_{t}[∅t^{#}].

Then for g : C_{s→t}[℧s→t^{#}] and α ≠ ∅^{#} (the empty case is trivial),

(i_{s→t}^{−1} (i_{s→t} g))_{α} = i_{t}^{−1} ∘ i_{t} ∘ g_{℧^{#}} ∘ C_{s}[α ⊆^{#} ℧s^{#}] ∘ i_{s}^{−1} ∘ i_{s}
= g_{℧^{#}} ∘ C_{s}[α ⊆^{#} ℧s^{#}]  by assumption
= C_{t}[℧s→t^{#} α ⊆^{#} ℧s→t^{#} ℧s^{#}] ∘ g_{α}  by (5)
= C_{t}[℧t^{#} ⊆^{#} ℧t^{#}] ∘ g_{α}
= g_{α}

The reverse equality is demonstrated by instantiation. ⊓ ⊔

Thus for each abstract value α ∈ Dt^{#} there is an embedding α^{E} : C_{t}[α] → t defined by α^{E} = i_{t} ∘ C_{t}[α ⊆^{#} ℧t^{#}]. The image of this function α^{E} is the property used in the conventional interpretation.

5 Abstract Interpretation and Transformation

Abstract interpretation of a closed expression e : t will yield a value e^{#} ∈ Dt^{#}, representing the type of the transformed expression. Transformation of e will yield an expression e^{⋆} : C_{t}[e^{#}]. The transformation will be considered correct if

e = (e^{#})^{E} (e^{⋆})  (6)

so that the behaviour of the original expression e can be recovered from the transformed version. The correctness condition is extended to expressions with free variables in Sect. 5.2.

The following lemma is used frequently in the proofs.

Lemma 9. The condition f = φ^{E} f′ is equivalent to

∀ α ∈ Ds^{#}. f ∘ α^{E} = (φ α)^{E} ∘ f′_{α}

The forward implication is established by expanding the definitions and simplifying. The reverse direction follows by instantiating α to ℧s^{#}.

We consider first the abstract interpretation and transformation of the constants.

5.1 Translation of Constants

For each constant c : t, we shall define an abstract constant c^{#} ∈ Dt^{#} and a translated constant c^{⋆} : C_{t}[c^{#}] satisfying

c = (c^{#})^{E} (c^{⋆})  (7)

In most cases this property is easily verified.

The definitions of the abstract constants c^{#} ∈ Dt^{#} are mostly standard (e.g. in [7]). The constant empty is new, but its transformation is straightforward:

empty^{#} α = ∅t^{#}
empty_{α}^{⋆} = empty

The product constants are translated to themselves:

fst^{#}(α ⊠ β) = α snd^{#}(α ⊠ β) = β  pair^{#} α β = α ⊠ β
fst_{α⊠β}^{⋆} = fst  snd_{α⊠β}^{⋆} = snd (pair_{α}^{⋆} x)_{β} y = pair x y

Injections into sums can only produce values in one arm of the sum:

inl^{#} α = α ⊞ ∅^{#}  inr^{#} β = ∅^{#} ⊞ β
inl_{α}^{⋆} = inl  inr_{β}^{⋆} = inr

We must combine the results of the two arms of a choose:

choose^{#} φ ψ (α ⊞ β) = φ α ∪^{#} ψ β
((choose_{φ}^{⋆} f)_{ψ} g)_{α⊞β} = choose (C_{t}[φ α ⊆^{#} γ] ∘ f_{α}) (C_{t}[ψ β ⊆^{#} γ] ∘ g_{β})
where γ = φ α ∪^{#} ψ β

Note that if α is ∅^{#}, then since φ is strict γ = ψ β and the left branch is transformed to λ x^{∅}. e = empty. The program will then contain types ∅ + t. We assume that a subsequent pass will reduce these, eliminating associated injections and chooses.

Failure can only produce the bottom element of lifting:

fail^{#} α = ∅^{#}_{□^{⊥}}
fail_{α}^{⋆} = empty_{⊥}

Applications of lift are delayed:

lift^{#} α = α_{□}
lift_{α}^{⋆} = id

For evaluation, there are two possibilities. If the expression to be evaluated is already unboxed, no evaluation is required:

ext^{#} φ α_{□} = φ α
(ext_{φ}^{⋆} f)_{α_{□}} = f_{α}

If the argument is boxed, the evaluation remains, and we must ensure that its result type is pointed:

ext^{#} φ α_{□^{⊥}} = φ α ∪^{#} ⊥^{#}
(ext_{φ}^{⋆} f)_{α□^{⊥}} = ext (C_{t}[φ α ⊆^{#} γ] ∘ f_{α}) where γ = φ α ∪^{#} ⊥^{#}

where for each pointed type t, ⊥t^{#} is the least element of Dt^{#} such that the image of ⊥t^{#}^{E} contains the bottom element of t. We can define ⊥t^{#} by the following rules:

⊥s×t^{#} = ⊥s^{#} ⊠ ⊥t^{#}
⊥t_{⊥}^{#} = ∅^{#}_{□^{⊥}}
⊥s→t^{#} α = ⊥t^{#} for α ≠ ∅s^{#}

For example, ⊥ℤ_{⊥}^{#} = ∅^{#}_{□^{⊥}}, whose concretion is the one point type ∅_{⊥}. In general, for any pointed type t, ⊥t^{#} ∈ Dt^{#} abstracts a one point type, that point being mapped by ⊥t^{#}^{E} to the bottom element of t.

Recursion also requires a pointed type:

fix^{#} φ = ⋃_{n∈ω}^{#} φ′^{n}(∅^{#}) where φ′ α = φ α ∪^{#} ⊥^{#}
fix_{φ}^{⋆} f = fix (C_{t}[φ γ ⊆^{#} γ] ∘ f_{γ}) where γ = fix^{#}φ

By Lemma 9, the instance of (7) for fix is equivalent to

∀ φ ∈ Dt→t^{#}. ∀ f : C_{t→t}[φ]. fix (φ^{E} f) \begin{matrix}= (fix^{#} φ)^{E} (fix_{φ}^{⋆} f) \\ = γ^{E} (fix (C_{t}[φ γ ⊆^{#} γ] ∘ f_{γ})) \end{matrix} (8)

Since ⊥^{#} ⊆^{#} γ, we know that γ^{E} is strict, and hence (8) follows from

f ∘ γ^{E} = (φ γ)^{E} ∘ f′_{γ} = γ^{E} ∘ C_{t}[φ γ ⊆^{#} γ] ∘ f′_{γ}

As noted in Sect. 3.1, our definition of fix^{#} differs from that of the Cousots [2], who use the sequence φ^{n}(⊥^{#}), which is a chain under the computational ordering. In contrast, we seek the smallest strict property for recursive functions.

The translation of a base constant c^{B_{1}→···B_{n}→B} is

(c^{B_{1}→···B_{n}→B})^{#} α_{1} … α_{n} = ℧B_{1}→···B_{n}→B^{#}
(… ((c^{B_{1}→···B_{n}→B})_{α_{1}}^{⋆} x_{1}) …)_{α_{n}} x_{n} = c^{B_{1}→···B_{n}→B} (α_{1}^{E} x_{1}) … (α_{n}^{E} x_{n})

Here each α_{i} is either ℧B_{i}^{#}, representing B_{i}, or ∅B_{i}^{#}, representing ∅. Hence each α_{i}^{E} is either id or empty. The application of the constant will only produce a result if all of its arguments exist.

5.2 Transformation of Expressions

An expression e : t with free variables x^{t_{1}}, …, x^{t_{n}} may be considered as a function of type t_{1} × ⋯ × t_{n} → t. Hence we define the set Env^{#} of abstract environments as the domain of mappings of variables x^{t} to abstract values from Dt^{#}, such that if any variable is mapped to ∅^{#}, they all are.

For any variable x^{t}, let x^{⋆} denote a family of variables indexed by Env^{#}, such that for each η ∈ Env^{#}, x^{⋆} has type C_{t}[η x^{t}].

Definition 10. If e : t, we write e ⟹^{e^{#}} e^{⋆} to mean

1. e^{#} : Env^{#} → Dt^{#} maps the empty environment to ∅^{#} and is monotonic with respect to both ⊆^{#} and ⊑^{#}. (That is, e^{#} is an abstract interpretation of e.)

2. e^{⋆} is a family of expressions e_{η}^{⋆} : C_{t}[e^{#} η] indexed by environments η ∈ Env^{#}, such that if η ⊆^{#} η′ ∈ Env^{#}, then

⋀_{x^{s}} (x_{η′}^{⋆} = C_{s}[η_{x} ⊆^{#} η′_{x}](x_{η}^{⋆})) ⇒ e_{η′}^{⋆} = C_{t}[e^{#}η ⊆^{#} e^{#}η′] (e_{η}^{⋆})

(That is, e^{⋆} is a natural transformation.)

3. For each η ∈ Env^{#},

⋀_{x^{s}} (x = η_{x}^{E} (x_{η}^{⋆})) ⇒ e = (e^{#} η)^{E} (e_{η}^{⋆})

(That is, the combination of abstract interpretation and transformation is correct.)

From these definitions it is easy to prove the following result, which enables us to transform any λ-expression.

Theorem 11.

1. If a constant c satisfies c = (c^{#})^{E} (c^{⋆}), then c ⟹^{\overline{c^{#}}} \overline{c^{⋆}} where \overline{c^{#}} η = c^{#} and \overline{c^{⋆}}_{η} = c^{⋆}.

2. x ⟹^{x^{#}} x^{⋆} where x^{#} η = η_{x}

3. If e ⟹^{e^{#}} e^{⋆}, then λ x. e ⟹^{f^{#}} f^{⋆}, where

f^{#} η α = e^{#} η[x ↦ α]
(f_{η}^{⋆})_{α} = λ x_{η}^{⋆}. e_{η[x↦α]}^{⋆}

4. If e_{1} : s → t, e_{2} : s, e_{1} ⟹^{e_{1}^{#}} e_{1}^{⋆} and e_{2} ⟹^{e_{2}^{#}} e_{2}^{⋆}, then e_{1} e_{2} ⟹^{e^{#}} e^{⋆}, where

e^{#} η = (e1^{#} η) (e2^{#} η)
e_{η}^{⋆} = (e_{1}^{⋆}_{η})_{e_{1}^{#}η} (e_{2}^{⋆}_{η})

Example 12. For the function

thrice : (t → t) → t → t

thrice f x =^{△} f (f (f x))

the transformed version is

thrice^{#} φ α = φ (φ (φ α))
(thrice_{φ}^{⋆} f)_{α} x =^{△} f_{φ(φ α)} (f_{φ α} (f_{α} x))

Note the use of three (possibly) different transformations of f.

Sometimes we will prefer weaker translations than those defined above. For example, if the above translation is applied to the term (λ x. (x, x)) ∘ lift, the lift will be duplicated. If these lifts are not subsequently consumed by the transformation, the resulting program might generate two thunks where formerly there was one. The detection of such situations requires a linearity analysis (as with deforestation in similar situations [13]). Such an analysis is beyond the scope of this paper, but we can offer the following result, which guarantees the correctness of such weakenings.

Proposition 13. If e : t, e ⟹^{e^{#}} e^{⋆} and e^{#} ⊆^{#} e^{#}′ ∈ Env^{#} → Dt^{#}, then e ⟹^{e^{#}′} e^{⋆}′, where

(e^{⋆}′)_{η} = C_{t}[e^{#} η ⊆^{#} e^{#}′ η] (e_{η}^{⋆})

Example 14. Suppose e : s_{⊥} × t and we wish to force the transformed version to use a lifted type for the first component. Then we can use this proposition with

e^{#}′ η = e^{#} η ∪^{#} ⊥^{#} ⊠ ℧^{#}

6 Conclusion

We have proved the correctness of a source-to-source transformation intended to remove thunks from the source program. The transformation of functions is polyvariant, with functions mapped to natural transformations, and is able to deal with higher order functions in a clean way. Such transformations are made possible by a source language in which lifting is explicit, and not all types need have a bottom element [8].

There are several areas in which this work could be extended.

Polymorphism. Our transformation assumed a monotyped language. It appears that many polymorphic functions, such as thrice above, could be handled by applying our rules to symbolic expressions representing abstract values.

Efficiency of the analysis. The abstract domains of even basic comportment analysis are rather large, but many of the points they contain contribute little to the quality of the transformation. It would be useful to identify useful subdomains. Similarly, one might like to cut down the sizes of the families of function variants used.

Quality of the generated program. We have said nothing about pragmatic issues, not even a guarantee that the transformation will improve the program. However we have given a framework (Prop. 13) within which such choices may be made while maintaining the correctness of the resulting transformation.

Recursive types. It is relatively straightforward to extend this work to (purely positive) retractive types, like the type of finite, partial and infinite lists. Adding initial types, like finite lists, would provide opportunities for further optimizations. However some care would be required: sometimes evaluating the large data structure early (rather than on demand) may be wasteful of space.

References

1. 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.

2. Patrick Cousot and Radhia Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). In International Conference on Computer Languages, pages 95–112. IEEE Computer Society Press, 1994.

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

4. G.W. Hamilton. Higher order deforestation. In Programming Languages: Implementations, Logics and Programs, volume 1140 of Lecture Notes in Computer Science, pages 213–227. Springer, 1996.

5. A. Reza Haydarlou and Pieter H. Hartel. Thunk lifting: Reducing heap usage in an implementation of a lazy functional language. Journal of Functional and Logic Programming, 1995.

6. Brian T. Howard. Inductive, projective, and pointed types. In ACM International Conference on Functional Programming, pages 102–109, Philadelphia, May 1996.

7. Sebastian Hunt and David Sands. Binding time analysis: A new PERspective. In ACM Symposium on Partial Evaluation and Semantics-based Program Manipulation, pages 154–165. ACM SIGPLAN Notices 26(9), September 1991.

8. 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. Springer.

9. 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, pages 270–281. Springer, 1980.

10. Alan Mycroft and Kirsten Lackner Solberg. Uniform pers and comportment analysis. In Programming Languages: Implementations, Logics and Programs, volume 982 of Lecture Notes in Computer Science, pages 169–187. Springer, 1995.

11. Ross Paterson. Compiling laziness using projections. In Static Analysis Symposium, volume 1145 of Lecture Notes in Computer Science, pages 255–269, Aachen, Germany, September 1996. Springer.

12. 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.

13. Philip Wadler. Deforestation: Transforming programs to eliminate trees. Theoretical Computer Science, 73:231–248, 1990.

14. 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, pages 385–407, Portland, OR, 1987. Springer.