The worker/wrapper transformation

Andy Gill and Graham Hutton. The worker/wrapper transformation.

The worker/wrapper transformation is a technique for changing the type of a computation, usually with the aim of improving its performance. It has been used by compiler writers for many years, but the technique is little-known in the wider functional programming community, and has never been formalised. In this article we explain, formalise, and explore the generality of the worker/wrapper transformation. We also provide a systematic recipe for its use, and illustrate the power of this recipe using a range of examples.

While the basic idea behind the worker/wrapper transformation should be trivial to any programmer, this paper shows the added value that comes from formal analysis and the usefulness of the algebraic approach.

The paper may be slightly too long for those used to reading work of this type, but since all the examples are presented in detail it should be more accessible to newcomers than many other similar papers.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Not for redistribution?

Hmmm. The article says "DRAFT of 21st Dec 2007 — Not for Redistribution". What does that mean in general? Is it "this is private and I only sent the link to my friends and you have no business reading it", or is it "this is work in progress, so check again and expect updates"?

Status

The version currently on the web is work in progress, and will be revised again before submission. In particular, a number of the calculations and proofs will be omitted in the submitted version for brevity, but will be included in an extended version on the web for those readers who want to see all the details. As always, comments are most welcome!

Terminological question

Is there any intended difference between the notion of "computation" and "function" in the article e.g. in the following paragraph:

Consider the problem of changing the type of a recursive computation. More precisely, suppose that we are given a computation comp ::A, defined as the least fixed point comp = fix body of some function body :: A → A, and that we wish to change the underlying type from A to some other type B. For example, it may be that B supports a more efficient implementation of the computation.

Or is the word "computation" just used to make the text more interesting?

We say "computation" rather

We say "computation" rather than "function" because the technique isn't specific to functions, but can be applied to values of any type, including non-function types such as Int, [Int], etc. For example, one of the examples in the paper shows how to transform a function of type Nat -> Nat into a computation of type Stream Nat, which isn't a function type. In practice, however, the most common application of the technique will indeed be with functions.

Rolling loops?

I wonder if the same idea of rolling has been applied to transform loops instead of (overt) recursion?

Modulo Scheduling

Modulo scheduling is an instance where this type of rolling happens, I believe. One iteration might be doing some work, setting up the next iteration, and completing the previous one, in parallel.

http://en.wikipedia.org/wiki/Software_pipelining

CPS and paremetricity

The CPS example was very interesting. It seems like you might be able to do a whole-program cps transformation using just worker/wrapper and beta-expansion.

The paper doesn't point it out so I took a while to notice the fusion rule

unwrap (wrap work) = work

can be applied with work other than the one you are simplifying. This is the key to deriving mutually recursive workers from mutually recursive functions. In particular this implies

k (fun args) = k (worker args id) = worker args k

whenever worker was derived from fun with a worker/wrapper cps transformation of the right arity.

You can also get that rule as a free theorem, if functions are parametric in the continuation return type. The Free theorem calculator says

k (f k2) = f (k . k2)

for f of type (T0-> r) -> r, when k is strict and total.

Requiring the continuation to be strict at least is not so bad. That justifies the rewrite

k (case e of pat -> alt) = case e of pat -> k alt

which gets the continuation through cases to functions in the first place. In the paper unwrap for the continuation example uses a case expression, so the corresponding simplification is just case/case.

Revised version - November 2008

A revised version of the paper is now available.