Projections for Strictness Analysis^{∗}

Philip Wadler

Programming Research Group, Oxford University and Programming Methodology Group, Chalmers University, Göteborg

R.J.M. Hughes

Department of Computer Science, University of Glasgow

May 1987

Abstract

Contexts have been proposed as a means of performing strictness analysis on non-flat domains. Roughly speaking, a context describes how much a sub-expression will be evaluated by the surrounding program. This paper shows how contexts can be represented using the notion of projection from domain theory. This is clearer than the previous explanation of contexts in terms of continuations. In addition, this paper describes finite domains of contexts over the non-flat list domain. This means that recursive context equations can be solved using standard fixpoint techniques, instead of the algebraic manipulation previously used.

Praises of lazy functional languages have been widely sung, and so have some curses. One reason for praise is that laziness supports programming styles that are inconvenient or impossible otherwise [Joh87, Hug84, Wad85a]. One reason for cursing is that laziness hinders efficient implementation.

Still, acceptable efficiency for lazy languages is at last being achieved. This is done by means of graph reduction [Pey87], as found in the G-machine [Aug84, Joh84] and the Ponder implementation [FW86], among others. The essential trick is to evaluate an expression immediately, when this is safe, rather than to construct a graph. Strictness analysis can reveal more places where this optimisation is safe. In the Ponder implementation, strictness analysis speeds up some programs by a factor of two or more. In addition, strictness analysis may enable other optimisations, such as destructive updating of arrays [HB85].

Accordingly, strictness analysis has received much attention; see [AH87] for a collection of some recent work. An elegant approach to strictness analysis is abstract interpretation. This approach was first applied by Mycroft [Myc81], and later extended to higher-order languages [BHA85, HY85] and polymorphism [Abr85]. For an excellent introduction, see [CP85].

∗Presented at the Third International Conference on Functional Programming Languages and Computer Architecture, Portland, Oregon, September 1987.

A remaining question of great interest was how to perform strictness analysis for data types over non-flat domains, such as lazy lists. An early proposal in this direction was made by Hughes, based on analysis of the context in which an expression may be evaluated [Hug85, Hug87a]. The method could determine useful information about strictness in programs using lazy lists. But it had three drawbacks.

First, it was not clear exactly what a context was. The first paper was somewhat informal, and concluded “a proper treatment would be welcome”. This was provided by the second paper, which modeled contexts as abstractions of sets of continuations. The model was less than completely intuitive, and the proofs involved were lengthy.

Second, context analysis yielded equations that were difficult to solve. The equations had to be solved by algebraic manipulation, and the descriptions of the manipulations required ran to many pages. Further, exact simplifications were not always possible, and heuristics were required to decide what approximations to introduce. An example in [Hug85] shows how an apparently reasonable heuristic can lead to an unreasonably bad approximation.

Third, the method applied only to first-order, untyped languages. Extensions to higher-order, polymorphic languages would need to be developed.

Meanwhile, Wadler, in part inspired by Hughes’ work, discovered a different method of analysing strictness on non-flat domains, with none of the above drawbacks [Wad87]. First, the method was a straightforward extension of abstract interpretation, and so built on existing mathematical foundations and intuitions. Second, like other work on abstract interpretation, it used finite domains. Fixpoints could be found by straightforward techniques [CP85], and methods for finding fixpoints efficiently could be directly applied [PC87, YH86]. No algebraic manipulation was required. Third, since abstract interpretation had already been extended to include higher-order languages and polymorphism, so did this method.

An open and shut case? Not quite. As it turns out, context analysis reaches the places abstract interpretation cannot reach. As we shall see in the next section, there are primarily two kinds of strictness of interest for lazy lists, head strictness and tail strictness. Context analysis can find both. Abstract interpretation can find tail strictness, and it can find head strictness when it is combined with tail strictness. But it cannot find head strictness alone. That’s a shame. A major paradigm in lazy functional programming involves functions that read a bit of the input list and then produce a bit of the output list, acting like a coroutine. Such functions are often head strict, but cannot be tail strict. So the additional power of context analysis is important.

This paper provides a new description of contexts that addresses previous shortcomings.

First, a simple, and we believe intuitive, explanation of contexts is given. The notion of context is identified with the notion of projection from domain theory. The proofs involved are simpler than those in [Hug87a].

Second, finite domains are given for contexts over lists. This means that the standard fixpoint methods can be used, and algebraic manipulation is no longer required.

Third … well, two out of three isn’t bad. The method is still limited to a firstorder, monomorphic language. However, there are reasons to believe that context analysis will follow in the footsteps of abstract interpretation, and be extended to higher-order functions and polymorphism; one way of doing so is outlined in [Hug87b]. It is hoped that the new explanation of contexts given here will aid in this task.

The history of this paper is as follows. Wadler discovered how to represent contexts by projections (Sections 2–4, 6–8) after studying the work of Hughes [Hug87a]. Hughes discovered how to define finite domains for contexts over lists (Sections 5, 6.6) after studying the work of Wadler [Wad87]. The paper itself was written by Wadler.

Contexts have close relations to other work on strictness analysis, including that of Burn [Bur87], Dybjer [Dyb87], Hall [HW87], and Wray [Wra86, FW86]. Contexts may also be applied to Bjerner’s work on analysing time and space complexity [Bje87], and to analysing pre-order traversal [Wad85b]. These issues are discussed in Section 8.

This paper assumes the reader knows some domain theory; for an introduction, see one of [Sco82, Sto77, Sch86]. The domains used are consistently complete, algebraic cpos. Familiarity with abstract interpretation or the authors’ previous work is helpful but not required.

This paper is organized as follows. Section 1 introduces head strictness and tail strictness. Section 2 formalizes these with projections. Section 3 extends the method to deal with ordinary strictness. Section 4 discusses finite domains of contexts over flat domains. Section 5 discusses finite domains of contexts over lists. Section 6 develops the fundamentals of context analysis. Section 7 presents examples. Section 8 compares related work. Section 9 concludes.

1 Head strictness and tail strictness

As usual, let : be the list construction operator, cons, so that 1 : 2 : [ ] denotes the list [1, 2]. Let :_{H} be a function identical to :, but strict in the head field, and let H be the computable function on lists that replaces each : by :_{H}. For example,

H (1 : 2 : ⊥ : 3 : [ ]) = 1 :_{H} 2 :_{H} ⊥ :_{H} 3 :_{H} [ ] = 1 : 2 : ⊥

Similarly, let :_{T} be a function identical to : but strict in the tail field, and let T be the computable function that replaces each : by :_{T}.

We say a function f is head strict if it is safe to replace each : by :_{H} in the argument to f . In other words, f is head strict if f = f ∘ H . Similarly, we say f is tail strict if f = f ∘ T .

An example of a head strict function is before, which returns the segment of a list before the first zero (see Figure 1). Any cons cell examined by before will have its head examined to see if it is zero, hence before is head strict. If a bottom occurs before the first zero, we have, say,

before (1 : ⊥ : 0 : [ ]) = before (1 : ⊥) = 1 : ⊥

before xs

=

case xs of
[ ]  ⇒ [ ]
y : ys ⇒ if y = 0
then [ ]
else y : before ys
length xs

=

case xs of
[ ]  ⇒ 0
y : ys ⇒ 1 + length ys
doubles xs

=

case xs of
[ ]  ⇒ [ ]
y : ys ⇒ (2 × y) : doubles ys

Figure 1: Example programs

which is as required, since H (1 : ⊥ : 0 : [ ]) = 1 : ⊥. If a bottom occurs after the first zero, we have, say

before (1 : 2 : 0 : ⊥ : 3 : [ ]) = before (1 : 2 : 0 : ⊥) = 1 : 2 : [ ]

which is again as required, since H (1 : 2 : 0 : ⊥ : 3 : [ ]) = 1 : 2 : 0 : ⊥.

An example of a tail strict function is length, which finds the length of a list. Any cons cell examined by length will also have its tail examined, hence length is tail strict. If any tail field contains bottom, then length is undefined; for instance

length (1 : 2 : 3 : ⊥) = length ⊥ = ⊥

which is as required, since T (1 : 2 : 3 : ⊥) = ⊥. If no tail field contains bottom, the length is defined even if some head is bottom; for instance

length (1 : ⊥ : 3 : [ ]) = 3

which is again as required, since T (1 : ⊥ : 3 : [ ]) = 1 : ⊥ : 3 : [ ].

This characterization of strictness is useful because it can enable important optimizations. Say we have a program containing a fragment of the form f ∘ g, and we know that f is head strict. Then the fragment is equivalent to f ∘ H ∘ g. So we may replace this call of g by a call to a new version g_{H} of g, in which every : operation that produces part of the result is replaced by :_{H}. The head arguments of these cons operations may be evaluated immediately, instead of constructing a graph to be evaluated later. This can lead to significant improvements in efficiency.

Thus, our goal is to label every sub-expression of the program with a context function like H or T that indicates what components of a structure can be evaluated immediately.

We will see later that contexts can also be used to indicate simple strictness information, such as what arguments in a function call need to be evaluated.

Contexts themselves provide useful information for propagating contexts further. Consider the function doubles, which doubles every element in a list. Clearly, doubles is not head strict. For instance

doubles (1 : ⊥ : 3 : [ ]) = 2 : ⊥ : 6 : [ ] ≠ 2 : ⊥ = doubles (1 : ⊥)

even though H (1 : ⊥ : 3 : [ ]) = 1 : ⊥. So doubles ≠ doubles ∘ H . However, it is not hard to see that H ∘ doubles = H ∘ doubles ∘ H , that is, doubles is head strict in a head strict context. Since before is head strict we have

before ∘ doubles = before ∘ H ∘ doubles = before ∘ H ∘ doubles ∘ H

showing that it is safe to replace : by :_{H} in the argument to doubles when the result is examined by a head strict function like before.

One reason that head strictness is of particular importance is that printing may induce a head strict context. Say that e is an expression that returns a list of characters to be printed on a terminal. Then e and H e will both print exactly the same results, but the same cannot be said of e and T e. Thus, a character printer is head strict but not tail strict.

Traditionally, a function f is said to be strict if f ⊥ = ⊥. Tail strictness can be characterized similarly: a strict function f is tail strict iff f u = ⊥ whenever any tail of u is ⊥. This holds because if any tail of u is ⊥ then T u = ⊥, so f u = f (T u) = f ⊥ = ⊥. Similarly, a strict function f is both head strict and tail strict iff f u = ⊥ whenever any head or tail of u is ⊥. This “f u = ⊥” approach was used in [Wad87].

However, it is not true that f is head strict only if f u = ⊥ whenever some head of u is ⊥. Two counter-examples appear above, where before u ≠ ⊥ although some head of u is ⊥. A main advantage of the context approach is that it can describe head strictness, whereas the “f u = ⊥” approach cannot.

2 Projections

A continuous function α is a projection [Sco81] if for every object u,

\begin{matrix}α u & ⊑ & u \\ α (α u) & = & α u \end{matrix}

The first line says that projections only remove information from an object. The second line says that all the information is removed at once, so applying the projection a second time has no effect. These two properties can also be written

\begin{matrix}α & ⊑ & ID \\ α ∘ α & = & α \end{matrix}

where ID is the identity function, defined by ID u = u for all u. In this paper, α, β, γ, etc., will always denote projections.

As we have seen, projections such as H and T characterize the context in which a value is needed, and so are useful for this style of strictness analysis. We will use the words “projection” and “context” interchangably.

Projections form a complete lattice under the ⊑ ordering, with ID at the top and BOT at the bottom, where BOT is the function defined by BOT u = ⊥ for all u. For example, the projections we have seen so far form the following lattice,

ID •
H •  • T
H ⊓ T •
BOT •

The projection H ⊓ T corresponds to being both head and tail strict.

We say that a function f is β-strict in context α if α ∘ f = α ∘ f ∘ β, and write f : α ⇒ β. For example, we have seen that before : ID ⇒ H and doubles : H ⇒ H .

An alternate characterization of f : α ⇒ β is given by the following result.

Proposition: f : α ⇒ β iff α ∘ f ⊑ f ∘ β.

Proof: In the forward direction, since α ∘ f = α ∘ f ∘ β and α ⊑ ID, we may conclude α ∘ f ⊑ f ∘ β. In the reverse direction, composing α with each side gives α ∘ α ∘ f ⊑ α ∘ f ∘ β, and since α ∘ α = α, we have α ∘ f ⊑ α ∘ f ∘ β. Since β ⊑ ID, we also have α ∘ f ⊒ α ∘ f ∘ β, which gives the desired equality. □

The strictness relation satisfies a useful composition result.

Proposition: If f : α ⇒ β and g : β ⇒ γ then f ∘ g : α ⇒ γ.

Proof: Immediate, since α ∘ f ∘ g ⊑ f ∘ β ∘ g ⊑ f ∘ g ∘ γ. □

For example, from before : ID ⇒ H and doubles : H ⇒ H we may conclude, as noted in the previous section, that before ∘ doubles : ID ⇒ H .

A similar argument shows that if α ⊑ β and f : β ⇒ γ and γ ⊑ δ then f : α ⇒ δ. In particular, f : α ⇒ ID for every f and α.

We now verify the assertion made above, that projections form a complete lattice. We first take care of the least upper bound.

Proposition: If A is a set of projections, then ⨆ A exists and is a projection.

Proof: For every α ∈ A we have α ⊑ ID, so clearly ⨆ A exists and ⨆ A ⊑ ID. Further, from this it follows that ⨆ A ∘ ⨆ A ⊑ ⨆ A, so it remains to show that ⨆ A ∘ ⨆ A ⊒ ⨆ A.

Then for every object u we have

⨆ A (⨆ A u)
= ⨆ A (⨆{α u | α ∈ A})
⊒ ⨆{⨆ A (α u) | α ∈ A}
⊒ ⨆{α (α u) | α ∈ A}
= ⨆{α u | α ∈ A}
= ⨆ A u

as required. □

Now, a difficulty arises. If we let α ⊓ β denote the largest continuous function f such that f ⊑ α and f ⊑ β, then f may not be a projection. (Counter-example: Consider the domain {a, b, c} with a ⊏ b ⊏ c. Let α = {a ↦ a, b ↦ a, c ↦ c} and β = {a ↦ a, b ↦ b, c ↦ b}. Then f = {a ↦ a, b ↦ a, c ↦ b}, which is not a projection since f c = b but f (f c) = a.)

Therefore, we adopt the convention that α ⊓ β denotes the largest projection γ such that γ ⊑ α and γ ⊑ β. (In the counter-example above, we would have γ = {a ↦ a, b ↦ a, c ↦ a}.) With this convention, the greatest lower bound of a set of projections is given by

⊓A = ⨆{β | for all α ∈ A, β ⊑ α}

where β ranges over projections. It follows from the above proposition that ⊓A exists and is a projection.

3 Strictness and absence

We have used projections to characterize such exotic concepts as head strictness and tail strictness, but we have not yet tackled ordinary strictness, defined by f ⊥ = ⊥. Using projections to characterize strictness is possible, but requires some extensions to the framework described so far.

Roughly speaking, the problem is that projections, as described so far, let us specify what information is sufficient but not what information is necessary. For example, say that f is head strict, that is, f = f ∘ H . Then we know that if the argument of f is, say, 1 : ⊥ : [ ] then it is sufficient to use the value H (1 : ⊥ : [ ]) = 1 : ⊥ instead. But to characterize strictness, we must say something about what information is necessary. In particular, we must use projections to say that it is necessary that a value be more defined than ⊥.

In order to specify information about necessity with projections, we extend our domains with a new element , pronounced “abort” (the symbol is intended to resemble a lightning bolt). The interpretation of α u = will be that α requires a value more defined than u. In order for this interpretation to work, we require that all functions be strict in , that is, f = for all functions f . Intuitively, if a value is not acceptable it is mapped into , which causes all computation to abort immediately. To define strictness, we will use a projection STR that does not accept ⊥, so we must have STR ⊥ = . Since any projection must satisfy α u ⊑ u, we must have beneath ⊥ in the domain ordering.

Therefore we extend each domain D to a new domain D _{}, derived by lifting D and adding a new bottom element, , beneath the existing bottom, ⊥. So ⊏ ⊥ ⊑ u, for every u ∈ D. Every function f : D_{1} → D_{2} is extended to a function f : D_{1} _{}→ D_{2} _{}by making f strict in . All functions are strict in , but may or may not be strict in ⊥. In particular, cons is strict in , so (u : ) = = ( : v) for all u and v.

(A technical point: since everything, even the conditional, is strict in , the least fixpoint of any recursive function definition is the constant function. This is not what we want. For recursive functions definitions in our language, we take the least fixpoint above the function BOT defined by BOT u = ⊥ if ⊏ u, and BOT = .)

The extended domains allow contexts to specify information about necessity. A value u is unacceptable to a context α if α u = .

Proposition: If f : α ⇒ β and u is unacceptable to β, then f u is unacceptable to α.

Proof: Assuming α ∘ f = α ∘ f ∘ β and β u = gives

α (f u) = α (f (β u)) = α (f ) =

as required. □

The projection STR is defined by setting

[figure: STR; =]
STR ⊥ =
STR u = u if ⊥ ⊏ u

We can now capture the notion of strictness precisely.

Proposition: f : STR ⇒ STR iff f is strict.

Proof: In the forward direction, the only value unacceptable to STR is ⊥, so it follows from the preceding result that u = ⊥ implies f u = ⊥, so f is strict. In the backward direction, we must show that if f is strict then STR (f u) ⊑ f (STR u) for all u. If u ≠ ⊥ this follows since STR u = u. If u = ⊥ this follows since both sides of the inequality reduce to : on the left STR (f ⊥) = STR ⊥ = and on the right f (STR ⊥) = f = . □

Although ID is still the top element of the domain of projections, BOT is no longer the bottom. The new bottom element is the projection FAIL, defined by FAIL u = for all u. Say that a function f : D_{1} → D_{2} is divergent if f u = ⊥ for every u ∈ D_{1}. The following two results are of interest.

Proposition: f : STR ⇒ FAIL iff f is divergent.

Proposition: g : FAIL ⇒ FAIL for every function g.

Both proofs are simple exercises. As a corollary, the composition rule implies that if f is divergent, then so is f ∘ g for any g.

The old projection BOT is rechristened ABS, for “absent”, and defined by

[figure: ABS; =]
ABS ⊥ = ⊥
ABS u = ⊥ if ⊥ ⊏ u

Say that a function f : D_{1} → D_{2} ignores its argument if f u = f ⊥ for every u ∈ D_{1}. Again, there are two results of interest.

Proposition: f : STR ⇒ ABS iff f ignores its argument.

Proposition: g : ABS ⇒ ABS for every function g.

And again, both proofs are simple exercises. As a corollary, the composition rule implies that if f ignores its argument, then so does f ∘ g for any g.

The four projections we have been discussing have the following domain ordering:

ID •
ABS •  • STR
FAIL •

This is just a subdomain of the domain of projections over D. This is discussed more fully in the next section.

Context analysis can yield useful information for a compiler. If analysis succeeds in labelling a sub-expression e with one of these contexts, then the following interpretations apply:

• FAIL. No value that could be returned by e is acceptable. The compiler may safely implement e by code that aborts the program immediately.

• ABS. The value of e is ignored. The compiler may safely implement e by code that returns a dummy value.

• STR. The value of e is required. The compiler may safely implement e by code that evaluates e immediately; no graph for e need be constructed.

• ID. The value of e may be required or may be ignored. The compiler can safely implement e only by constructing a graph.

Strictness annotations having exactly these four meanings are used in Wray’s strictness analyzer [Wra86, FW86]. Most strictness analysers only distinguish between strict and non-strict arguments, corresponding to the distinction between STR and ID above. The compilation possibilities afforded by FAIL and ABS are extra optimisations, not available to most compilers.

We will call α : D _{}→ D _{}a projection over D. Strictly speaking, we should write ID_{D}, STR_{D}, ABS_{D}, and FAIL_{D} to indicate the domain D that these projections are over. Usually we will omit the domain subscript since it can be derived, as the phrase goes, from context.

The strict part of a projection α is α′ = α ⊓ STR. For example, ID′ = STR and ABS′ = FAIL. A context α is strict if it is equal to its strict part, or equivalently, if α ⊑ STR. Ironically, this implies that α is called strict iff α ⊥ = , and non-strict iff α ⊥ = ⊥.

The problem of analysing strictness in context α can be reduced to analysing strictness in context α′:

Proposition: If α is non-strict and f : α′ ⇒ β then f : α ⇒ ABS ⊔ β.

Proof: Since α is non-strict, α = ABS ⊔ α′ and we have

(ABS ⊔ α′) ∘ f = (ABS ∘ f ) ⊔ (α′ ∘ f ) ⊑ (f ∘ ABS) ⊔ (f ∘ β) ⊑ f ∘ (ABS ⊔ β)

as required. □

For instance, say f is a strict function, so f : STR ⇒ STR. That is, if the result of f is needed, then the argument of f will be needed. Then since ID′ = STR and ABS ⊔ STR = ID, from the above we have f : ID ⇒ ID. That is, if the result of f may or may not be needed, then the argument of f may or may not be needed.

4 Finite domains

Let INT be the flat domain of integers. Clearly, there are an infinite number of projections α over INT . Using these we can specify quite precise information about functions. For example, for any integer m let EQUAL_{m} be the projection defined by

EQUAL_{m} m = m
EQUAL_{m} u =  if u ≠ m

Then if f : EQUAL_{m} ⇒ EQUAL_{n} it follows that f n = m.

For some applications this expressiveness may be useful, but it is more precise than required for strictness analysis in a compiler. Fortunately, we need not maintain such precise information. The purpose of context analysis is to label each sub-expression e in a program with a context α such that α e and e return the same result (within the larger context in which the sub-expression appears). Clearly, if it is safe to label e with α then it is also safe to label e with any β such that α ⊑ β. For example, we can safely approximate EQUAL_{m} by STR, for any m.

This gives a notion of “approximation” inverted from the usual one. The inequality α ⊑ β is traditionally read “α approximates β”, meaning α u is less defined than β u for every u. However, we may also read it as “α is approximated by β”, meaning α conveys more precise information than β about the values acceptable in some context.

Thus for purposes of strictness analysis in a compiler, we may choose to use any subset of projections, so long as it is closed under the operations of interest (e.g., ⊔ and ⊓) and so long as it contains the largest projection, ID. For analyzing flat domains, such as the integers, a good choice is the four point subdomain of projections, {ID, STR, ABS, FAIL}, discussed in the preceding section.

The subset of projections that we choose need not even include FAIL. For example, the two point domain {ID, STR} can provide quite useful analyses. When using this two point domain, ABS is approximated by ID, and FAIL is approximated by STR. This is indeed safe: ID safely approximates everything, since it is always safe to construct a graph; and STR safely approximates FAIL, since if the function is going to diverge anyway (as for FAIL) it is safe to evaluate the argument in advance (as for STR).

5 Finite domains for lists

Let LIST D be the non-flat domain of lists whose elements are in domain D. For example, LIST INT is the domain of lists of integers, and LIST (LIST INT ) is the domain of lists of lists of integers. We have already discussed two projections over LIST D, namely H and T . This section presents finite domains of projections over LIST D, analogous to the finite domains of projections over INT presented in the previous section.

It is convenient to define the projection NIL and the projection generator CONS. The projection NIL over LIST D is defined by

[figure: NIL; =]
NIL ⊥  =
NIL [ ]  = [ ]
NIL (u : v) =

If α is a projection over D, and β is a projection over LIST D, the projection CONS α β on LIST D is defined by

CONS α β  =
CONS α β ⊥  =
CONS α β [ ]  =
CONS α β (u : v) = α u : β v

These projections can be used to describe lists precisely. For example,

CONS ID (CONS EQUAL_{0} NIL)

specifies the context that only accepts lists of length two whose second element is zero.

Of special interest are projections which treat all elements of a list in the same way. If α is a projection over D, then the projections FIN α and INF α over LIST D are defined by

FIN α = NIL ⊔ CONS α (FIN α)

INF α = NIL ⊔ CONS α (ABS ⊔ INF α)

Roughly speaking, FIN α accepts only finite lists, each element of which is accepted by α, and INF α accepts finite or infinite lists, each element of which is accepted by α. Neither accepts ⊥, so FIN α and INF α are strict for every α, even if α is non-strict.

These projections are related to the ones discussed previously by the following equations:

STR = INF ID  ID = ABS ⊔ INF ID
H′ = INF STR  H = ABS ⊔ INF STR
T′ = FIN ID  T = ABS ⊔ FIN ID
H′ ⊓ T′ = FIN STR  H ⊓ T = ABS ⊔ FIN STR

(∗)

The projections H and T were defined before was introduced, so H ⊥ = ⊥ and T ⊥ = ⊥, and therefore H and T are non-strict. The corresponding strict versions are, of course, H′ and T′.

As another example, we have length : STR ⇒ FIN ABS. That is, length is defined only for finite lists, but the elements of the list are ignored.

Let D_{C} be a finite domain of projections over D. For example, if D is INT then D_{C} might be {STR, ID}. The finite domain LIST_{C} D_{C} of projections over LIST D consists of the projections

INF α  ABS ⊔ INF α
FIN α  ABS ⊔ FIN α

for each α ∈ D_{C} , plus FAIL and ABS. Note that STR and ID are implicitly included in LIST_{C} D_{C} , since from above we have STR = INF ID and ID = ABS ⊔ INF ID, and ID must be in D_{C} .

For example, if D_{C} is the two point domain {ID, STR}, then LIST_{C} D_{C} is the ten point domain consisting of the eight projections in (∗) plus ABS and FAIL. A diagram of this domain appears in Figure 2.

As a second example, if D_{C} is the four point domain {ID, STR, ABS, FAIL}, then LIST_{C} D_{C} is a domain with sixteen points. One would expect eighteen points (4 × 4 + 2), but

FIN FAIL = INF FAIL
ABS ⊔ FIN FAIL = ABS ⊔ INF FAIL

and so four of the points collapse to two. The identifications arise because CONS FAIL α = FAIL for any projection α, and so FIN FAIL = INF FAIL = NIL.

6 Context analysis

The problem of context analysis is this: given a program defining f and a projection α, we wish to find a projection β such that f : α ⇒ β. Of course, we could just always take β to be ID, but if possible we would like to find a smaller projection.

ID •
• T
STR •  H •
• T′  • H ⊓ T
H′ •  • ABS
• H′ ⊓ T′
• FAIL

Figure 2: A finite domain of projections for lists

Ideally, given f and α we would like to find the smallest β such that f : α ⇒ β. There are two difficulties with this. First, it is not clear that a smallest β always exists. Second, even if it did exist, it would not be computable. As we have already observed, f : STR ⇒ FAIL holds iff f diverges for every argument; so if we could always find the smallest β then we could solve the halting problem. Therefore we will have to settle for finding some β, not necessarily the smallest one.

6.1 Language

To analyse a function f we will need to examine the program that defines it. We will use a small first-order language, with the following grammar:

e ::= x  variables
| k  constants
| f e_{1} … e_{n}  function applications
| if e_{0} then e_{1} else e_{2}  conditionals
| case e_{0} of [ ] ⇒ e_{1} | y : ys ⇒ e_{2} case expressions

Each function f has a fixed arity n. Function definitions have the form

f x_{1} … x_{n} = e

Infixes are allowed as usual; e_{1} + e_{2} is equivalent to (+) e_{1} e_{2}, where (+) is a function name. Some programs in this language are shown in Figure 1 of Section 1 and Figure 5 of Section 7.

6.2 Projection transformers

For each function f of n arguments, and each i from 1 to n, we will define f^{i} to be a transformer that takes a projection applied to the result of f into a projection that may safely be applied to the i’th argument. That is, f^{i} must satisfy the following safety requirement: if β_{i} = f^{i} α then

α (f u_{1} … u_{i} … u_{n}) ⊑ f u_{1} … (β_{i} u_{i}) … u_{n}

for all u_{1}, …, u_{n}. In particular, if f is a function of one argument, and β = f^{1} α, then the safety requirement ensures that f : α ⇒ β.

It is easy to show that the safety requirements for f^{1}, …, f^{n} are satisfied iff

α (f u_{1} … u_{n}) ⊑ f (β_{1} u_{1}) … (β_{n} u_{n})

for all u_{1}, …, u_{n}, where β_{i} = f^{i} α for each i from 1 to n.

Similar to f^{i}, for each expression e and each variable x, we will define e^{x} to be a transformer that takes a projection applied to e into a projection that may safely be applied to each instance of x in e. That is, e^{x} must satisfy the safety requirement: if β = e^{x} α then

α e ⊑ e[(β x)/x]

for all values of the variables in e (including x). Here, as usual, e_{0}[e_{1}/x] denotes the result of substituting e_{1} for each instance of x in e_{0}.

(To make this definition more formal, we should give a semantics of the language, defining E[[e]]ρ for each expression e and environment ρ. The safety requirement becomes that if β = e^{x} α then

α (E[[e]]ρ) ⊑ E[[e]](ρ[(β (ρ[[x]]))/[[x]]])

for each environment ρ. To be more formal still, for e^{x} α we should write something like M [[e]][[x]]α.)

Having specified the safety conditions, we must now give definitions of f^{i} and e^{x} satisfying these conditions. Definitions of f^{i} for primitive f appear in Section 6.7. Otherwise, if the program defining f is

f x_{1} … x_{n} = e

then f^{i} is defined by

f^{i} α = e^{x_{i}} α

for each i from 1 to n. The definition of e^{x} may in turn refer to the f^{i}, so the definitions are mutually recursive. The full definition of e^{x} is given in Figure 3. If it looks forbidding, don’t worry: all will be explained as we go along.

It is clear that the rule defining f^{i} is safe (that is, satisfies the safety condition) if the rules defining e^{x} are safe. In what follows, we will show that the rules defining e^{x} are safe if the f^{i} are safe; and that the f^{i} are safe for primitive f . It follows by recursion induction that the definitions of f^{i} and e^{x} are indeed safe.

e^{x} α = α ⊳ e^{x} α′

If α is strict and α ≠ FAIL then:

x^{x} α = α
y^{x} α = ABS  if x ≠ y
k^{x} α = ABS  if k is a constant

(f e_{1} … e_{n})^{x} α

= e_{1}^{x} (f^{1} α) & ⋯ & e_{n}^{x} (f^{n} α)

(if e_{0} then e_{1} else e_{2})^{x} α

= e_{0}^{x} STR & (e_{1}^{x} α ⊔ e_{2}^{x} α)

(case e_{0} of [ ] ⇒ e_{1} | y : ys ⇒ e_{2})^{x} α

= (e_{0}^{x} NIL & e_{1}^{x} α) ⊔ (e_{0}^{x} (CONS (e_{2}^{y} α) (e_{2}^{ys} α)) & e_{2}^{x} α)

Figure 3: Definition of e^{x} α

Three rules in the definition of e^{x} are obvious:

x^{x} α = α
y^{x} α = ABS if x ≠ y
k^{x} α = ABS if k is a constant

More generally, it is safe to set e^{x} α = ABS whenever x does not appear in e. As an example, say that the constant function K is defined by

K x y = x

Then we have K^{1} α = x^{x} α = α and K^{2} α = x^{y} α = ABS. In other words, evaluating K in context α causes its first argument to be evaluated in context α and its second argument to be ignored.

6.3 The ⊳ operation

Results from Section 3 guarantee that it is safe to set e^{x} FAIL = FAIL and e^{x} ABS = ABS, and that if α is non-strict we may set e^{x} α = ABS ⊔ e^{x} α′. Therefore, in defining e^{x} α, we can restrict our attention to the case that α is strict and not FAIL.

To aid in doing so, we introduce the ⊳ operator, pronounced “guard”, and defined by

FAIL ⊳ β  = FAIL
ABS ⊳ β  = ABS
α ⊳ β = β if α is strict and α ≠ FAIL
(ABS ⊔ α) ⊳ β = ABS ⊔ β if α is strict and α ≠ FAIL

It follows from the above that we may safely set

e^{x} α = α ⊳ e^{x} α′

This rule holds for all α, but has no effect unless α is non-strict or FAIL. We assume in all other rules that α is strict and not FAIL.

6.4 Application and the & operation

Say we wish to determine (f e_{1} e_{2})^{x} α. Then we need to find a δ such that

α (f e_{1} e_{2}) ⊑ (f e_{1} e_{2})[δ x/x]

We go about doing so in three stages.

First, we know from the definition of f^{i} that

α (f e_{1} e_{2}) ⊑ f (β_{1} e_{1}) (β_{2} e_{2})

where β_{i} = f^{i} α, for i = 1, 2. Second, we know from the definition of e_{i}^{x} that

f (β_{1} e_{1}) (β_{2} e_{2}) ⊑ f (e_{1}[γ_{1} x/x]) (e_{2}[γ_{2} x/x])

where γ_{i} = e_{i}^{x} β_{i}, for i = 1, 2. Third, we need to find a δ such that

f (e_{1}[γ_{1} x/x]) (e_{2}[γ_{2} x/x]) ⊑ (f e_{1} e_{2})[δ x/x]

Clearly, we could take δ = γ_{1} ⊔ γ_{2}. But we can do a little better than this. Since all functions are strict in , assuming x appears in both e_{1} and e_{2} then if either γ_{1} x = or γ_{2} x = the left hand side evaluates to , so we may safely set δ x = . Therefore we define

(γ_{1} & γ_{2}) u = \{ \begin{matrix} & if γ_{1} u = or γ_{2} u = \\ γ_{1} u ⊔ γ_{2} u & otherwise \end{matrix}

Taking δ = γ_{1} & γ_{2}, we have shown that the rule

(f e_{1} e_{2})^{x} α = e_{1}^{x} (f^{1} α) & e_{2}^{x} (f^{2} α)

is safe. For a function of n arguments, we get the rule show in Figure 3.

What if x does not appear in e_{1} or e_{2}? No problem. If x does not appear in e_{i}, then γ_{i} = e_{i}^{x} β_{i} = ABS, so we won’t have γ_{i} x = anyhow (unless x is , of course).

As an example, we have

(K x y)^{y} STR = x^{y} (K^{1} STR) & y^{y} (K^{2} STR)
= x^{y} STR & y^{y} ABS = ABS & ABS = ABS

so the expression K x y ignores the value of y, as we would expect.

The & operation satisfies many laws, some of which are shown in Figure 4: it is commutative, associative, idempotent, has ABS as a unit, FAIL as a zero, distributes over ⊔, and satisfies various properties with NIL and CONS.

Many people at first expect the role of & to be played by ⊓. It is worth noting, therefore, that & is certainly different from ⊓; for instance, ABS & STR = STR whereas ABS ⊓ STR = FAIL. As we shall see in Section 8, Dybjer’s inverse image analysis [Dyb87] might be considered a restriction to the class of projections for which & and ⊓ are identical.

& is commutative and associative

α & α = α
ABS & α = α
FAIL & α = FAIL
α & (β ⊔ γ) = (α & β) ⊔ (α & γ)
CONS α β & NIL = FAIL
CONS α β & CONS γ δ = CONS (α & γ) (β & δ)

Figure 4: Laws of &

6.5 Conditional expressions

To derive the rule for conditional expressions, we need to find a δ such that

α (if e_{0} then e_{1} else e_{2}) ⊑ (if e_{0} then e_{1} else e_{2})[δ x/x]

Again, the derivation proceeds by a sequence of steps.

We begin by pointing out an incorrect derivation. An obvious first step would be

α (if e_{0} then e_{1} else e_{2}) = (if STR e_{0} then α e_{1} else α e_{2})

where α is strict and STR is over booleans. But in a domain containing this law is invalid. For example, if α is STR over integers, e_{0} is true, e_{1} is 1, and e_{2} is ⊥, then the left-hand side of the above equation yields 1, while the right-hand side yields (because if true then 1 else evaluates to and not 1).

Instead, as a first step we use the rule

α (if e_{0} then e_{1} else e_{2})
= (if STR e_{0} then α e_{1} else ⊥) ⊔ (if STR e_{0} then ⊥ else α e_{2})

where, again, α is strict and STR is over booleans. It is easy to verify that this rule is valid by considering the four possibilities , ⊥, true, and false for the value of e_{0}.

We then have

α (if e_{0} then e_{1} else e_{2})

= (if STR e_{0} then α e_{1} else ⊥) ⊔
(if STR e_{0} then ⊥ else α e_{2})
⊑ (if e_{0}[β_{0} x/x] then e_{1}[β_{1} x/x] else ⊥) ⊔
(if e_{0}[β_{0} x/x] then ⊥ else e_{2}[β_{2} x/x])
⊑ (if e_{0} then e_{1} else ⊥)[((β_{0} & β_{1}) x)/x] ⊔
(if e_{0} then ⊥ else e_{2})[((β_{0} & β_{2}) x)/x]
⊑ ((if e_{0} then e_{1} else ⊥) ⊔ (if e_{0} then ⊥ else e_{2}))
[(((β_{0} & β_{1}) ⊔ (β_{0} & β_{2})) x)/x]
= (if e_{0} then e_{1} else e_{2}) [(((β_{0} & β_{1}) ⊔ (β_{0} & β_{2})) x)/x]
= (if e_{0} then e_{1} else e_{2}) [((β_{0} & (β_{1} ⊔ β_{2})) x)/x]

where β_{0} = e_{0}^{x} STR, β_{1} = e_{1}^{x} α, and β_{2} = e_{2}^{x} α. The last step uses the distributive law from Figure 4.

This establishes the rule

(if e_{0} then e_{1} else e_{2})^{x} α = e_{0}^{x} STR & (e_{1}^{x} α ⊔ e_{2}^{x} α)

when α is strict. An intuitive reading of this rule is as follows. If the conditional expression is evaluated under strict α then x will be evaluated in e_{0} under STR and either x will be evaluated in e_{1} under α or x will be evaluated in e_{2} under α.

Readers familiar with strictness analysis by abstract interpretation will note a resemblance between the rule given above and the rule

(if e_{0} then e_{1} else e_{2})^{#} = e_{0}^{#} ⊓ (e_{1}^{#} ⊔ e_{2}^{#})

used in abstract interpretation.

6.6 Case expressions

The rule for case expressions is

(case e_{0} of [ ] ⇒ e_{1} | y : ys ⇒ e_{2})^{x} α
= (e_{0}^{x} NIL & e_{1}^{x} α) ⊔ (e_{0}^{x} (CONS (e_{2}^{y} α) (e_{2}^{ys} α)) & e_{2}^{x} α)

when α is strict. An intuitive reading of this rule is as follows. If the case expression is evaluated under strict α, then e_{0} must evaluate to nil or to a cons cell. If e_{0} evaluates to nil, then x will be evaluated in e_{0} under NIL, and in e_{1} under α. If e_{0} evaluates to a cons cell, then the head of this cons cell will be evaluated as much as y is evaluated in e_{2} under α, that is, the head will be evaluated under e_{2}^{y} α. Similarly, the tail will be evaluated under e_{2}^{ys} α. So x will be evaluated in e_{0} under (CONS (e_{2}^{y} α) (e_{2}^{ys} α)), and in e_{2} under α.

Using the concepts developed in the preceding sections, the proof of safety of this rule is straightforward, although lengthy. We outline only some key points here. To start, translate the case expression

case e_{0} of [ ] ⇒ e_{1} | y : ys ⇒ e_{2}

to the equivalent form

if null e_{0} then e_{1} else e_{2}[head zs/y, tail zs/ys][e_{0}/zs]

where zs is a new variable and null, head, and tail are defined in the usual way. The proof uses the facts

α (head e) = head ((CONS α ABS) e)
α (tail e) = tail ((CONS ABS α) e)

and the last two laws in Figure 4.

As pointed out in [Wad87], including case expressions in the language is essential when the analysis uses finite domains for lists. If the case expressions were rewritten in terms of head and tail, as above, then context analysis would yield less precise results. Case expressions are essential because they gather in one place information about how both the head and tail of the list are evaluated.

6.7 Primitive functions

Finally, we need to define f^{i} where f is a primitive function.

If f is strict in all its arguments, then we may set

f^{i} α = α ⊳ STR

This definition is suitable for all primitives functions on flat domains, such as (+) and (=) over integers.

Most functions on non-flat domains, such as (=) over lists, need not be given as primitives, since they can be defined in the language. The exception is the constructor function, (:). Writing HEAD for (:)^{1} and TAIL for (:)^{2} (do not confuse these with H and T ), we must have

α (u : v) ⊑ ((HEAD α) u) : ((TAIL α) v)

for all u, v, and α. It is not hard to verify that the following definitions fit the bill:

(HEAD α) u = ⨆_{v∈LIST D} head (α (u : v))
(TAIL α) v = ⨆_{u∈D} tail (α (u : v))

where α is over LIST D, and, as usual, head (u : v) = u and tail (u : v) = v. It follows that

HEAD (CONS α β) = α if β ≠ FAIL
TAIL (CONS α β) = β if α ≠ FAIL

and so HEAD and TAIL take after their smaller brethren.

7 Examples

Applying the analysis method of the previous section to the definitions in Figures 1 and 5 gives the following results:

length^{1} α = NIL ⊔ CONS ABS (length^{1} α)
before^{1} α = NIL ⊔ CONS (STR & HEAD α) (ABS ⊔ before^{1} (TAIL α))
doubles^{1} α = NIL ⊔ CONS (HEAD α) (doubles^{1} (TAIL α))
append^{1} α = NIL ⊔ CONS (HEAD α) (append^{1} (TAIL α))
append^{2} α = α ⊔ append^{2} (TAIL α)
reverse^{1} α = NIL ⊔ CONS (HEAD (append^{2} α)) (rev^{1} (append^{1} α))

append xs zs

=

case xs of
[ ]  ⇒ zs
y : ys ⇒ y : append ys zs
reverse xs

=

case xs of
[ ]  ⇒ [ ]
y : ys ⇒ append (revese ys) [y]

Figure 5: More example programs

append^{1} α = (xs^{xs} NIL & zs^{xs} α)

⊔(\begin{matrix}xs^{xs} (CONS ((y : append ys zs)^{y} α) ((y : append ys zs)^{ys} α)) \\ &(y : append ys zs)^{xs} α)) \end{matrix}

= (NIL & ABS)

⊔(\begin{matrix}(CONS (y^{y} (HEAD α) & (append ys zs)^{y} (TAIL α)) (y^{ys} (HEAD α) & (append ys zs)^{ys} (TAIL α))) \\ &ABS) \end{matrix}

= NIL & (CONS (HEAD α) (append^{1} (TAIL α)))
append^{2} α = (xs^{zs} NIL & zs^{zs} α)

⊔(\begin{matrix}xs^{zs} (CONS ((y : append ys zs)^{y} α) ((y : append ys zs)^{ys} α)) \\ &(y : append ys zs)^{zs} α)) \end{matrix}

= (ABS & α)

⊔(\begin{matrix}ABS \\ &(y^{zs} (HEAD α) & (append ys zs)^{zs} (TAIL α))) \end{matrix}

= α ⊔ append^{2} (TAIL α)

Figure 6: Context analysis of append

As usual, this assumes α is strict and not FAIL; otherwise, we use the rule f^{i} α = α ⊳ f^{i} α′. For the interested reader, details of the derivation for append are shown in Figure 6. The results have been simplified to improve readability, by reducing terms of the form ABS & β to β.

Not surprisingly, recursive function definitions yield recursive definitions of projection transformers. Using the finite domains of Sections 4 and 5, we can solve these in the usual way by taking the limits of ascending Kleene chains [CP85]. For instance, for length we define:

length^{1(0)} α = FAIL
length^{1(i+1)} α = NIL ⊔ CONS ABS (length^{1(i)} α)

We then have

length^{1(0)} STR = FAIL
length^{1(1)} STR = NIL ⊔ CONS ABS FAIL
= FIN FAIL
length^{1(2)} STR = NIL ⊔ CONS ABS (FIN FAIL)
= FIN ABS
length^{1(3)} STR = NIL ⊔ CONS ABS (FIN ABS)
= FIN ABS

and so length^{1} STR = FIN ABS, just as we expected: length must be given a finite list, but ignores the lists elements.

Because the domains are finite, the ascending chains are guaranteed to reach a fixpoint after a finite number of iterations. Further, no algebraic simplification methods are required. For any given list domain, we may construct finite tables for calculating the relevant functions (⊔, &, CONS, HEAD, TAIL) and then compute the limits as above in a completely mechanical fashion.

Applying the above techniques we can derive, among other results, the following:

(1) before^{1} ID  = ABS ⊔ INF STR
(2) before^{1} STR  = INF STR
(3) doubles^{1} STR  = STR
(4) doubles^{1} (INF STR) = INF STR
(5) append^{1} (FIN STR) = FIN STR
(6) append^{2} (FIN STR) = FIN STR
(7) append^{1} (INF STR) = INF STR
(8) append^{2} (INF STR) = ABS ⊔ INF STR
(9) reverse^{1} STR  = FIN ID
(10) reverse^{1} (FIN STR) = FIN STR

Line (1) shows that before is head strict (recalling that H = ABS ⊔ INF STR), and line (2) shows in addition that it is strict. (In fact, line (1) follows immediately from line (2), by an application of the guard rule.) Line (3) shows that doubles is strict, but says nothing else, while line (4) shows that doubles is head strict in a head strict context. Lines (5–6) show that in a context requiring a completely evaluated list, append must completely evaluate both its arguments. Lines (7–8) show that in a head strict context append is head strict in both arguments, but it is only strict in the first argument. Line (9) shows that the argument to reverse must be a finite list, and line (10) shows that if reverse is evaluated in a head and tail strict context, then so is its argument.

The results for reverse are particularly significant, since in the original work on contexts [Hug85] the analysis of reverse was more problematic. The analysis method has also been applied to a few other functions (the other common definition of reverse, insertion sort) with equally good results.

What are the method’s limitations? The major one is that conditional and case expressions have a special role. For instance, if we define a function cond by

cond x y z = if x then y else z

and then replace an arbitrary conditional by an equivalent call on cond, then analysis of the transformed function may give a much worse result. This is worrying, although more research is needed to discover whether this will be a significant problem in practice.

8 Relation to other work

Burn’s evaluation transformers. Geoffrey Burn has suggested evaluation transformers as a way of controlling parallelism in a functional language implementation [Bur87]. There are some close relationships between his work and ours, but also some important differences.

Burn introduces four evaluators, E_{0}, E_{1}, E_{2}, E_{3}, which correspond to the four projections ID, STR, T′, H′ ⊓ T′. His main result can be re-phrased in our terms as follows: it is safe to use an evaluator E_{i} (in the sense that this will waste no work) whenever it is safe to apply the corresponding projection (in the sense that this will not change the result).

For example, writing f (E_{2} e) means that the spine of e can be evaluated in parallel with the application of f . This is rather different than writing f (T′ e), which insists that the entire spine of e is evaluated before it is passed to f . However, f (E_{2} e) wastes no work (evaluates no unneeded portion of the spine) only when f (T′ e) = f e (that is, only when f is tail-strict). The key to Burn’s work is this link between an operational notion of safety (“wastes no work”) and a denotational one (“doesn’t change the result”).

Burn’s analysis is based on Wadler’s previous work [Wad87]. Whether evaluation transformers can take advantage of the extra information revealed by projection analysis (such as absence or head strictness) is one of many remaining open questions.

Dybjer’s inverse image analysis. Inspired by earlier work on context analysis, Peter Dybjer has devised a method of analysis based on inverse images of open sets [Dyb87]. The method has a simple and elegant mathematical foundation. Like earlier work on contexts, it uses algebraic manipulation to solve equations.

Interestingly, the open sets used by Dybjer correspond exactly to a restricted class of projections. Namely, open sets correspond to projections α with the additional restriction that for each u, either α u = or α u = u. It is easy to see that with this restriction, the & operation defined in Section 6.4 is exactly equivalent to ⊓. The projections STR and T′ satisfy this restriction, while ABS and H′ do not. Thus open sets can describe strictness and tail strictness, but appear ill-suited for describing absence and head strictness.

Hall’s strictness patterns. Cordelia Hall’s strictness analyser is based on strictness patterns [HW87]. There are striking similarities between strictness patterns and projections; compare the strictness pattern laws, $$π = $π and $π ⊒ π, to the projection laws, α α u = α u, and α u ⊑ u (note that strictness patterns reverse the ordering). However, there appear to be no strictness pattern corresponding to ABS.

Unlike us, Hall can extract useful strictness from a list in which, say, every other element is strict. Also unlike us, Hall has examined the question of how to generate different versions of a procedure depending on the context in which it is called. Overall, the two works appear to be complementary. Whereas our work has stressed simple foundations, Hall’s has stressed practical issues in building a prototype.

Wray’s strictness analyser. The relation between the four point domain {ID, STR, ABS, FAIL} and the work of Stuart Wray [Wra86, FW86] has already been mentioned. Wray’s analyser also handles higher-order functions and a flexible type system; this inspired the similar extensions for backwards analysis outlined in [Hug87b].

Finally, here are two applications of projections outside of strictness analysis.

Bjerner’s complexity analysis. An important open problem is analysis of the time and space complexity of lazy functional programs. Bror Bjerner has devised an elegant solution to this problem for the programming language of Martin-Löf’s type theory [Bje87]. The solution makes use of evaluation notes to describe how much of the result of a program is required. It appears straightforward to adapt projections for use as evaluation notes, and to adapt Bjerner’s method to lazy functional languages.

Pre-order traversal. In connection with Wadler’s work on the listless transformer, it was necessary to describe the notion of pre-order traversal of a data structure [Wad85b]. This was done by introducing a function PRE, satisfying PRE ⊑ ID and PRE ∘ PRE = PRE. A function f was pre-order if PRE ∘ f = PRE ∘ f ∘ PRE. In other words, pre-order traversal was characterized by a projection. (Thus, this paper can be applied directly to solving the problem, posed by that paper, of how to analyse pre-order traveral.)

It was exactly at this time that the two authors were pursuing the work on strictness analysis described in the introduction. But it was not until a year later that Wadler realized that this approach could describe the work of Hughes!

9 Conclusion

This work has provided a simpler explanation of contexts than available previously. The finite domains for lists presented here make it possible to solve recursive equations in a straightforward way, using standard fixpoint techniques, which has advantages over the previous method of algebraic manipulation.

An important next step is to extend backwards analysis to languages with higher-order functions and polymorphic typing; a way of doing this is outlined in [Hug87b]. Some applications of projections outside strictness analysis were suggested in the last section. We hope the approach presented here will provide fertile soil for future developments.

Our projection for strictness analysis is a rosy future.

Acknowledgements. This work owes a debt to the Programming Methodology Group at Chalmers University of Technology, Göteborg. The first paper on context analysis was written while Hughes was a visitor at Chalmers, and this paper was written while Wadler was a visitor there. We are grateful to the members and staff of the PMG for the enjoyable, stimulating, and supportive environment they provided.

We thank Richard Bird, Geoffrey Burn, Peter Dybjer, Cordelia Hall, Thomas Johnsson, Kent Karlsson, Jon Fairbairn, Simon Peyton-Jones, Staffan Truvè, and Stuart Wray for fruitful discussions and for comments on an earlier draft of this paper. Wadler is particularly grateful to Peter Dybjer for comments on the mathematical rigour (or lack of it) in an earlier version of this work.

Part of this work was performed while Wadler was on a research fellowship supported by ICL.

References

[Abr85] S. Abramsky. Strictness analysis and polymorphic invariance. In N. Jones and H. Ganzinger, editors, Workshop on Programs as Data Objects, Springer-Verlag, Copenhagen, October 1985. LNCS 217.

[AH87] S. Abramsky and C. Hankin. Abstract Interpretation of Declarative Languages. Ellis Horwood, 1987.

[Aug84] L. Augustsson. A compiler for lazy ML. In ACM Symposium on Lisp and Functional Programming, pages 218–227, Austin, 1984.

[BHA85] G. L. Burn, C. L. Hankin, and S. Abramsky. The theory of strictness analysis for higher-order functions. In N. Jones and H. Ganzinger, editors, Workshop on Programs as Data Objects, Springer-Verlag, Copenhagen, October 1985. LNCS 217.

[Bje87] B. Bjerner. Complexity analysis of programs in type theory. Programming Methodology Group, Chalmers University of Technology, Göteborg, Sweden, 1987.

[Bur87] G. L. Burn. Evaluation transformers—a model for the parallel evaluation of functional languages. In Conference on Functional Programming Languages and Computer Architecture, Portland, Oregon, September 1987.

[CP85] C. Clack and S. L. Peyton-Jones. Strictness analysis—a practical approach. In Conference on Functional Programming Languages and Computer Architecture, Nancy, France, 1985.

[Dyb87] P. Dybjer. Computing inverse images. In International Conference on Automata, Languages, and Programming, 1987.

[FW86] J. Fairbairn and S. C. Wray. Code generation techniques for functional languages. In ACM Symposium on Lisp and Functional Programming, pages 94– 104, Boston, 1986.

[HB85] P. Hudak and A. Bloss. The aggregate update problem in functional programming systems. In 12’th ACM Symposium on Principles of Programming Languages, pages 300–314, January 1985.

[Hug84] R. J. M. Hughes. Why functional programming matters. Technical Report, Programming Methodology Group, Chalmers University of Technology, Göteborg, Sweden, 1984.

[Hug85] R. J. M. Hughes. Strictness detection in non-flat domains. In N. Jones and H. Ganzinger, editors, Workshop on Programs as Data Objects, Springer-Verlag, Copenhagen, October 1985. LNCS 217.

[Hug87a] R. J. M. Hughes. Analysing strictness by abstract interpretation of continuations. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, Ellis Horwood, 1987, to appear.

[Hug87b] R. J. M. Hughes. Backwards analysis of functional programs. University of Glasgow research report CSC/87/R3, March 1987.

[HW87] C. V. Hall and D. S. Wise. Compiling strictness into streams. In 14’th ACM Symposium on Principles of Programming Languages, pages 132–143, Munich, January 1987.

[HY85] P. Hudak and J. Young. Higher order strictness analysis in untyped lambda calculus. In 12’th ACM Symposium on Principles of Programming Languages, pages 97–109, January 1985.

[Joh84] T. Johnsson. Efficient compilation of lazy evaluation. In ACM Symposium on Compiler Construction, 1984.

[Joh87] T. Johnsson. Attribute grammars as a paradigm for functional programming. Programming Methodology Group, Chalmers University of Technology, Göteborg, Sweden, 1987.

[Myc81] A. Mycroft. Abstract interpretation and optimising transformations for applicative programs. PhD thesis, University of Edinburgh, 1981.

[PC87] S. L. Peyton-Jones and C. Clack. Finding fixpoints in abstract interpretation. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, Ellis Horwood, 1987.

[Pey87] S. L. Peyton-Jones. Implementing Functional Languages using Graph Reduction. Prentice-Hall, 1987.

[Sch86] D. A. Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Newton, Massachusetts, 1986.

[Sco81] D. S. Scott. Lectures on a mathematical theory of computation. Technical Report PRG-19, Oxford University Programming Reseach Group, May 1981.

[Sco82] D. S. Scott. Domains for denotational semantics. In Conference on Automata, Languages and Programming, pages 577–613, Springer-Verlag, July 1982. LNCS 140.

[Sto77] J. E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, Massachusetts, 1977.

[Wad85a] P. L. Wadler. How to replace failure by a list of successes. In Conference on Functional Programming Languages and Computer Architecture, Nancy, France, 1985.

[Wad85b] P. L. Wadler. Listlessness is better than laziness II: composing listless functions. In N. Jones and H. Ganzinger, editors, Workshop on Programs as Data Objects, Springer-Verlag, Copenhagen, October 1985. LNCS 217.

[Wad87] P. L. Wadler. Strictness analysis on non-flat domains (by abstract interpretation over finite domains). In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, Ellis Horwood, 1987, to appear.

[Wra86] S. C. Wray. Implementation and Programming Techniques for Functional Languages. PhD thesis, University of Cambridge, January 1986.

[YH86] J. Young and P. Hudak. Finding fixpoints on function spaces. Technical Report YALEU/DCS/RR-505, Yale University Dept. of Computer Science, December 1986.