PLT Redex & SEwPR








































    

Semantics Engineering with PLT Redex, by
Matthias Felleisen, Robby Findler, and Matthew Flatt.

Preface

Working programmers engineer software systems. The typical engineering process consists of a number of phases, including the collection of requirements, the creation of a specification, the design of the architecture, the design of the modules, the maintenance of the system, and so on. In many cases, the engineering process involves iterative approaches, with repetitions across various phases in the process.

Working semanticists engineer models of programming languages. Such models almost always include at least one semantics, often several. Like the engineering of a software system, the creation of a semantics requires many different steps, including the formulation of a model, its exploration with test cases, example-based validation of invariants, theorem-proving, typesetting, and more. Also like the engineering of software systems, the engineering of a semantics is an iterative process, not a linear one.

This text is addressed to the working semantics engineer who needs a lightweight modeling tool. Typically these are graduate students and working programmers who find themselves engineering the semantics of a programming language or, more likely, an extension of a programming language. An ideal reader knows the functional programming language Scheme and has significant experience with representing information via S-expressions. A regular reader has a working knowledge of some functional language (Erlang, Haskell, ML) or has extensive experience programming functionally in a conventional language. In our experience, the key is a familiarity with programming over algebraic data types.

Organization: We have organized the text into three parts. Part I presents a framework for the formulation of language models, focusing on equational calculi and abstract machines. Roughly speaking, a minimal model of a language requires the specification of the core of the syntax and its meaning. This book uses a syntactic approach to the formulation of meaning. Put differently, the meaning of the core syntax is mostly formulated through binary relations on itself. We illustrate the approach and its major ideas with several small programming languages inspired by Church's λ-calculus.

Part II introduces software tools for expressing the models from part I as PLT Redex programs. In principle, Redex is just a small domain-specific programming language, hosted in PLT Scheme. A typical Redex model consists of two parts: a grammar for the language syntax and a binary relation on the syntax. Put differently, formulating a language model in Redex requires as little effort as writing it down with paper and pencil. One immediate advantage of Redex programs is that these models are executable. It is thus possible to explore the models with examples; to create and run test suites that are also useful for an eventual implementation; to check whether examples satisfy some invariant; to typeset the model. Because Redex is an embedded programming language, semantics engineers may also use plain Scheme functions for the model and may even import their own tools. Part II explains how to do all this with examples from part I and more.

Part III collects seven contributions on a wide range of models, all formulated in Redex. In the first contribution, Carl Eastlund explains an intermediate point in the design of a variant of ACL2 with modules; the Redex model is used to explore how to map modules to ACL2's evaluator and, separately, to the theorem prover. Martin Gasblicher, in the second contributed article, presents the first rewriting model of macro expansion for the R5RS version of Scheme; the Redex model allows programmers to step through the expansion of macro expressions. For the third article, Kathryn Gray extends her work on interoperability between untyped programming languages and typed ones; her Redex model combines the semantics of two distinct languages in one in order to investigate soundness issues. Joe Hallet, Eric Allen, and Sukyoung Ryu use a Redex model to explain one intricate part of Fortress's type system. The fifth article continues George Kuan's series of articles on type checking as a reduction system; thus, his Redex model uses reductions for modeling both the type checking process and for the evaluation process. With the penultimate contribution, Jacob Matthews describes his development of a web-based interview specification language. Last but not least, Mike Rainey demonstrates how Redex models are helpful for developing scheduling algorithms for a multi-core world.

To the Instructor: We have used the first two parts in graduate courses on topics in programming languages. A typical course covers the first two parts in four to eight weeks, depending on the familiarity of students with Scheme and/or functional programming. While we assign weekly homework projects for this period, we also ask students to work out Redex models for papers we pick. Students present the results of these projects in class. Equipped with this background, the course tackles additional topics. Sometimes students develop Redex models for papers of their choice; at other times, we jointly investigate historical developments of ideas.

To the Student: In addition, we have used the notes to train individual PhD students with a self-study plan. These students typically work through parts I and II in parallel so that they can immediately use the theoretical lessons to build practical models. Since most of our students end up extending a programming language, and since most of these designs are long-term efforts with many iterations, we consider it critical that students become intimately familiar with Redex (and other lightweight modeling tools).

Many times, our students iterate the model development to the point where we can reuse the test suites from the model for an actual implementation of a language extension. Our paper at the 2007 International Conference on Functional Programming on engineering functional and delimited continuations for a realistic programming system is a particularly good example of this kind of language development. We conjecture that all students of programming languages will benefit from such work flows.

Software: PLT Redex comes with the PLT Scheme implementation, which is available for free at http://www.plt-scheme.org/

Redex program is just a Scheme module that imports the Redex language. We urge you to download the software before you start reading so that you can experiment with Redex as you work your way through the book.

Programmers do not have to know much about Scheme to use Redex. Programmers who do know Scheme, especially PLT Scheme, can easily escape into the host language and build their own extensions. Jacob Matthew's contribution, for example, is the specification of a domain-specific web programming language; his model's reduction relations open a web browser to interact with the user.

Like all software, Redex isn't perfect. For that reason, DrScheme comes with a Help Desk facility and an error reporting interface. The former explains our intent and contains details that are beyond the scope of a text like this one. We intend to continue the development of Redex, and you will be able to find the documentation for these extensions and revisions in Help Desk. The error reporting interface is useful both for contacting us concerning failures and for requesting additional features.

In addition to Redex, our web site also hosts the models in this book, additional examples, and future contributions. Visit http://redex.plt-scheme.org/ and also use it to share your favorite Redex models with others.

Acknowledgments: We thank Daniel P. Friedman for inspiring the exploration of reduction semantics and for pushing us to implement our ideas. Lambda, lambda, and once more, lambda.

Robert Hieb (1953--1992) and Matthias jointly worked out the style of reduction semantics used in part I in 1989 and 1990. Their collaboration was tragically shortened by a traffic accident; Bob is dearly missed.

Thanks to Robby's Tutu for the use of her lanai, where he built the first version of Redex. And thanks to Jacob Matthews and Casey Klein for numerous hours of work on Redex.

Over the past decade, many people have read drafts of part I and have used early versions of Redex. Three stand out for their use of our work and their feedback: Olivier Danvy, Johnathan Edwards, and Bill Richter. In addition, the book has benefited from the feedback of several generations of students who took our courses. They are too numerous to enumerate here, but we certainly owe them a big “thank you.”

Finally, we wish to thank our editors at the Press. Bob Prior encouraged us for years to turn these notes into a book, and Ada Brunstein took us over the final hurdles to make it happen. Mel Goldsipe helped us polish our writing and that of our contributors.

Of course, the remaining errors are all ours.