Jewels of the lambda calculus: scope

If abstraction is the grand prize-winning jewel of the lambda calculus, then scope is the first runner-up. Mitch Wand teaches his graduate students that the scoping properties of a language are one of the Four Questions we ask in order to understand its semantics ("why is this language different from all other languages?").

Scope is the first static property of any programming language. Lexical scope gives us a static context in which to understand a fragment of a program. Within the following program:

λy.λx.y

we can look at the inner portion, λx.y, and in order to understand what portion of the program gives meaning to its body, we must understand that y is bound to--i.e., will receive its runtime meaning from--the static context of the fragment that binds it, i.e., the outer binding.

The static aspects of a program are what communicate its properties to the reader, allowing the reader to understand its behavior logically, as opposed to experimentally. Scope is the property that communicates the relationships between fragments of a program, whether through arguments, module imports, or class hierarchies. Scope is the static assignment of responsibility to these units of the program for communicating dynamic information.

Jewels of the lambda calculus: abstraction as generalization

Since there are few things as likely to inspire in me a sense of religious reverence as the lambda calculus, I've decided to start a new series on some of the deep principles of computer science lurking in the lambda calculus.

Let's start with the crown jewel, abstraction:

λx.e

This simple form represents the first rule of programming. Ruby hackers call it the "don't repeat yourself" rule. Perl hackers call it laziness: good programmers avoid repetitive, manual tasks. No matter the size, shape, or form, any time you write a program, you create an abstraction, a piece of code that automates a common task that otherwise would have to be repeated by a human.

Lambda abstractions represent the generalization of repeated patterns by parameterizing over their differences. If you perform several computations that are similar but not identical:

(9/5 × 23 + 32)
(9/5 × 40 + 32)
(9/5 × 13 + 32)

then each one of these computations is a special case of a more generalized procedure. The abstraction of the three is represented by parameterizing over the portion where they differ:

λc.(9/5 × c + 32)

From functions to abstract classes to Microsoft Office macros to parametric polymorphism, every form of abstraction is at its heart this same phenomenon.

Stratego is cool

I've been meaning to talk about this for a while. Stratego is a very cool language. Their raison d'être seems to be performing program transformations, such as compilers and program optimizations. But because it's a term rewriting system, it's also perfectly reasonable to use it as a framework for specifying operational semantics of programming languages.

Here's an example rewrite rule, specifying the evaluation of variable references in a CEKS machine:

EvalVar :
  |[
     Expr:  $e,
     Env:   $r,
     Cont:  $k,
     Store: $s
  ]|
→
  |[
     Value: $v,
     Cont:  $k,
     Store: $s
  ]|
where <is-var> e
    ; x := <var-name> e
    ; v := <resolve>(x,r)

Unless you know Stratego, you won't realize the most remarkable thing about this code: it's using a custom syntax for the representation of the configurations in the CEKS machine! That is, I've extended the syntax of Stratego with a concrete syntax for configurations, bracketed between |[ and ]| tokens. I've also added unquotation to that concrete syntax in the form of $ tokens followed by Stratego terms. This allows me to bind meta-variables within the left-hand side of the rewrite rule and the where clauses and refer to bound meta-variables within the right-hand side of the rewrite rule and again in the where clauses.

Stratego is based in part on SDF, the Syntax Definition Formalism, which is a lovely system for defining modular grammars. SDF is based on Tomita's Generalized LR (GLR) parsing algorithm, which recognizes the full class of context-free grammars, even ambiguous ones. If you want extensible grammars, you have to work with a class of grammars that's closed under composition, so they've chosen the most permissive, the full CFG class. Unfortunately this means you can end up with ambiguities, but as far as I know I haven't run into any sneaky ambiguities yet.

The other important feature of Stratego is its computational meta-language. My two requirements for a term rewriting system were the ability to specify rewrite rules in terms of the concrete language, which Stratego provides with flying colors, and the ability to compute side conditions. Stratego's entire computational model is based on rewriting, so side conditions work by saving the current state of the world and performing a rewrite on the side. Their rewriting combinators, known as strategies, allow for some pretty powerful abstractions. It has the feel of programming in the backtracking monad, not unlike Prolog. It's a little unfamiliar for a functional programmer, but it's perfectly adequate for the job.

It is my hope, and I'm optimistic, that we'll use Stratego to model the whole of the ECMAScript Edition 4 semantics. It's not on the same level as modeling the language in a theorem prover and using it to prove safety properties of the language mechanically, but my experience so far has shown that just having an executable model of a language is extremely useful for testing and driving out bugs in the semantics.

Java module system

Fascinating! There's a Java module system in the works.

Huzzah!

I finally have a working DSL connection at home! Now I can submit those few cherished hours of daily rest to the will of the Great Lord Productivity.

On a related note: in the year 2006, setting up DSL shouldn't take a week of phone tag, a dozen tech support reps, and an entire day wasted on troubleshooting (after the technician finishes repairing the line). I think my favorite moment was when the precious phone rep announced "I've figured out what the problem is! You're not actually using Internet Explorer, you're using a web browser with a bug that it doesn't display web pages." Thanks, Sherlock.