Årets bedste speciale 1997

Implicit and Explicit Aspects Of Scope and Block Structure

af Ulrik Pagh Schultz

Background
Block structure is a fundamental mechanism for expressing the scope of variables in a computation. Scope can be expressed either explicitly with formal parameters or implicitly with free variables. Making scope explicit is current practice in functional programming: it is called "lambda-lifting". Lambda-lifting transforms a block-structured and lexically scoped functional program into recursive equations. It has been used pervasively in the implemen-tation of functional programming languages - be they statically typed and lazy (Haskell), statically typed and eager (ML), or dynamically typed and eager (Scheme). For several years I had been toying with the idea of a program trans-formation that would be an inverse to lambda-lifting, i.e., that would restore block structure and lexical scope from recursive equations. This general theme caught Ulrik Schultz's interest, and he decided to dedicate his Speciale to it.

Contribution
Ulrik Schultz's thesis addresses the transformations between implicit and explicit scope and their application. Ulrik starts by reviewing the usual possible representations of "closures" (i.e., the run-time values of higher-order func-tions), and of block structure, and proposes an abstract model to describe the relative costs of lambda-lifted vs. lambda-dropped programs (Chapters 1 and 2). He then describes lambda-lifting and lambda-dropping algorithmically and in a symmetric way (Chapters 3 and 5). As a transition from lambda-lifting to lambda-dropping, each step of lambda-lifting is carefully reversed (Chapter 4). Chapter 6 compares and contrasts the two transformations, addressing their formal correctness (which was still an open problem, in spite of the wide use of lambda-lifting in compilers), evaluating the abstract model of Chapter 2, and reporting an array of tests over a number of block-structured procedural programming languages (i.e., not just functional, and including Pascal, Gnu C¹, and Java²). These tests show lambda-dropping to be a useful transformation that can be applied to clarify the structure of programs and to increase the efficiency of recursive functions. Chapter 7 reports Ulrik's main application of lambda-dropping: as the back-end of a partial evaluator for Scheme.

Analysis
I am impressed by Ulrik Schultz's thesis: it is a well-organized and well-presented piece of work, that he brought far beyond what I had envisioned when I first proposed him the project of investigating lambda-dropping, in the fall of '96. Let me structure my analysis in three directions.

Fundamental advances
The concepts of block structure and lexical scope are central to programming languages at large but aside from Landin's Correspondence Principle, they have been tackled either empirically (how to represent closures efficiently) or avoided altogether (by lambda-lifting source programs into recursive equa-tions). Ulrik's thesis provides a linguisting attempt at addressing them both.

Theoretical advances
Ulrik introduces an abstract cost model for block structure and lexical scope, and he provides the complexity of each transformation step in lambda-lifting and lambda-dropping. Time (one semester) proved too short to elaborate on the formal correctness of lambda-lifting and lambda-dropping, but this correctness was the topic of Ulrik's oral exam, in June '97, and he solved it satisfactorily during the standard few days of preparation.

Practical advances
Ulrik went out of his way to put lambda-lifting and lambda-dropping to the test, and this is to me where his work really stands out: we presented lambda-dropping at the joint conference ICFP (International Conference on Functional Programming) and PEPM (Partial Evaluation and Semantics-Based Program Manipulation), in June 1997, and we were given to meet the two most major implementors of functional programming languages today: Andrew Appel, from Princeton (Standard ML of New Jersey) and Simon Peyton Jones, from Glasgow (the Glasgow Haskell Compiler). They gave Ulrik a considerably harder time than we did in his oral exam, but he listened to their criticisms and he understood them, despite no particular expertise on implementing higher-order functional programming languages and no specific knowledge about the implementation of their compiler. Then, (overnight during the conference), he re-did all his tests on the latest version of SML/NJ, demonstrating to Andrew Appel that lambda-dropping yields a substantial speedup for more than single recursive functions - which is the only such optimization carried out in SML/NJ; and he did the same on the latest version of GHC, surprising Simon Peyton Jones who thought that the problem had been solved in a PhD thesis he directed last year (André Santos's thesis on "let floating", the crux of the matter is explained at the end of Section 5.5.2 of Ulrik's thesis). Let floating actually does not solve the problem, and lambda-dropped source programs are substantially more efficient in GHC.

Both of these veteran implementers went home with a copy of Ulrik's thesis under their arm, and they are now integrating his points in the next release of their compilers.

Conclusion
Ulrik Schultz's Speciale addresses a topic which is fundamental in programming languages - so fundamental that it actually has been overlooked. Through rare inventiveness and persistency, Ulrik has been able to shed a new light on it, in a way that he has formalized (both semantically and algorithmically, including complexity), and that he has demonstrated to be practical enough to influence the two major implementations of typed functional programming languages today: ML and Haskell.

For all these reasons I am submitting this Speciale to your judgement.

Vejleder: Lektor Olivier Danvy, DAIMI