Your lambda-cube is puny.

Aaron just showed me this mind-blowing figure from a paper by van Glabbeek that attempts to abstract the wide variety of notions of equivalence in the concurrency literature:

A moment of respectful silence, please.

Hand-writing derivations

I've come to prefer one particular approach to writing out a derivation tree by hand. I used to try to draw the tree by stacking up rules with horizontal separators à la Gentzen, but I could never judge how much space I would need--I'm not accustomed to filling a page bottom to top--and one page never seemed to be enough anyway.

I've found that writing judgments top to bottom, indenting to represent nesting, is much more scalable. E.g.:

⊢ (λ f.f 1) (λ x.x) : int
  ⊢ (λ f.f 1) : (int → int) → int
    f : int → int ⊢ f 1 : int
      f : int → int ⊢ f : int → int
      f : int → int ⊢ 1 : int
  ⊢ (λ x.x) : int → int
    x : int ⊢ x : int

Make a miniature model first

I've been taught this time and time again, I've seen Cormac do it repeatedly in the ECMAScript design process, I've been told by Mitch repeatedly to do it, but it still hasn't become instinct for me: when you're facing a dauntingly large system, it's incredibly helpful to start by extracting coherent but manageably small subsets of the design and model them first. It's amazing how well that works to make a system less terrifying to work with.

PLT System Facilities (Software Components): Namespaces

So far I've described PLT Scheme's first-class component systems, as well as the second-class, static module system. Of course, Scheme is a reflective language. Where there's eval, there's not just one "compile time." Code can be compiled and evaluated at any time during the execution of a PLT Scheme virtual environment.

Moreover, considering that one of the most important applications written in PLT Scheme--DrScheme--is an IDE, it's clearly important to be able to load and reload a single module multiple times. Users have to be able to edit a module and re-evaluate it without restarting the Scheme image. (In fact, it's even possible to run DrScheme from DrScheme, so it must even be possible to have multiple instances of the same module running concurrently!)

Every instance of a module in a running PLT Scheme environment has associated with it a namespace. Namespaces serve two somewhat orthogonal purposes. The first is to store top-level bindings. A module's namespace contains the mapping of its global definitions (some of which may be made available to other modules via provide). There is also a namespace associated with the REPL, which can be dynamically modified; in DrScheme, that namespace is typically just the one associated with the current running instance of the module being edited. In a sense, this role of namespaces is to mediate between the static, segmented architecture of modules and the dynamic, global nature of the Scheme top-level. This is an interesting tension that comes in whenever designing a lexically scoped language with dynamic code evaluation such as with eval or a REPL.

The second purpose of namespaces is to maintain an internal module registry, which keeps track of running instances of modules. Every namespace has its own registry, but registries may share instances. This is how it's possible both to create multiple, isolated instances of modules and to share module instances and their associated state.

Cognitive dissonance and correctness

I don't pretend to be a psychologist, but I find the mental process of getting a program correct fascinating. It feels like the process goes something like this:

1. Cognitive dissonance ("this can't possibly always work, can it?")
2. Confronting the danger ("what might go wrong?")
3. Questioning assumptions ("what am I assuming, and why do I need to assume it?")
4. Codifying assumptions as invariants ("P")
5. Pushing invariants through the program ("∀x. P(x)")

There are lots of techniques for #5, of course, and modularity helps make it manageable; e.g., defensively add in checks to enforce P so it's safe to assume.

But the interesting part to me is really the fact that, if you have the discipline to follow it through, it's precisely that queasy feeling that something might go wrong that eventually leads you to discover the program's invariants and ultimately to get the program right.

I mentioned this to Mitch, and he added "it's that recognition of danger (#1) that keeps us honest."

's Birthday is Coming Up...

I wonder if early in life, 's parents used to call him/her little baby epsilon.

Whoa

This is a really neat new feature of the Northeastern University library catalog:

Unless you spend the next 10 minutes taking screen shots and blogging about it, this is really convenient. And it saves our precious reserves of little scraps of paper.

PLT System Facilities (Software Components): Modules

Lexical scope in general and lambda in particular go a long way towards supporting modular, separate development. As I mentioned before, PLT Scheme builds a number of first-class, module-like component systems on top of lambda. But it also contains a more primitive module system in which modules are not first-class. This serves a number of purposes.

First of all, static modules provide systematic support for packaging, compiling, and deploying code. First-class modules are flexible and expressive, but they don't have anything to say about compilation and deployment. Somewhere along the line there has to be a notion of what the compiler takes as input, and when you have separate development, you need separate deployment and ideally separate compilation.

Another critical purpose of static modules is the ability to modularize static entities in a language. In ML, for example, modules can import and export types. Scheme is of course more [ed: dynamic] than ML, but it still has its own crucial compile-time abstractions: macros. With dynamic modules, there's no straightforward way to import and export static entities like macros. A secondary benefit of static modules is that you can import all the bindings from another module at once without having to spell them all out; this is admittedly less important but still very convenient.

Finally, PLT Scheme was designed to support multiple languages. For pedagogical purposes, this has allowed them to design multiple, concentric subsets of the language tailored to the How to Design Programs curriculum. This has also facilitated language research by making it easy to design and implement new languages (by macro-compiling them to Scheme) and to research language interactions in a multi-language environment. The relevant piece of the module system is a single hook at the beginning of a module definition: the grammar of a module is an S-expression containing the symbol module, a symbol naming the module, and an S-expression indicating the language of the body:

(module foo scheme body ...)

Typically the language chosen is the special built-in language scheme, as above, or the somewhat leaner scheme/base. But the language position works by simply importing another module that implements the required macros for compiling the body. In place of scheme, you can put in a module path for any module installed on the system.

It's also possible to specify a custom reader for a PLT language so it doesn't even have to be restricted to an S-expression syntax. The initial reader allows you to specify a language with the special shebang-like #lang syntax:

#lang scheme/base
body ...

From that point on, the language's reader has access to the input stream to parse it any way it likes.

Anyone can implement a language module, which means people have developed PLT implementations of Algol, Java, ML, and JavaScript, to name a few.

Update: Added in the missing word "dynamic" above. Also, this is a better link for module paths.

Also, Sam is right in the comments: the scheme language really isn't special or built-in in any significant way. It's simply another module provided in the standard PLT collections.

Ooh, that's pretty

OS X calculator "programmer" view:

PLT System Facilities (Software Components): Lexical scope

Like any programming system, PLT Scheme involves multiple people and a lot of code. So managing software components is a primary concern. And of course, as a Scheme, PLT uses lexical scope as the linguistic linchpin for managing software. The importance of lexical scope in a component architecture is that it allows code to be shared and mixed while guaranteeing the internal integrity of components.

With the power of macros, PLT has developed a number of software component abstractions on top of little lambda. One of these is a single-inheritance, class- and interface-based OOP system. Classes are first-class values, which means it's easy to implement mixins (i.e., classes parameterized over their superclass) as functions that return classes. More recently, they've introduced traits, which are like fragments of classes that can be more freely and flexibly combined than mixins. Also built with macros is the unit system, which is a first-class, parameterized, recursive module system.

All of these abstractions admit modular and separate development because they protect the internal integrity of their local bindings and definitions. You can hand out a component into an untrusted context and know that it won't be able to modify or even inspect the component's internals. And you can reason locally about your code knowing that no context can change its behavior based on these internals.

The PLT Scheme Operating System

Back in the day, programming languages were considered a systems concern. These days a lot of PL research is done in a vacuum, with abstract models and stand-alone prototypes. But programming languages rise and fall by their applications, and the deployment of a language always involves interesting and non-trivial systems challenges.

The PLT group has done a ton of work in this area. A decade ago, Matthew, Robby, Shriram and Matthias wrote an ICFP paper on Programming Languages as Operating Systems, sketching a few of the highlights of the PLT virtual machine. They focused on MrEd, the GUI engine. But taking a step back, there are many more systems-y facilities in PLT Scheme than just the UI infrastructure. And of course, that paper is a decade old and beginning to show its age.

I'm planning to write a series of posts on some of the myriad systems facilities in PLT Scheme and how they fit together.

I feel much better about myself

I'd always felt stupid for being stymied by the syntax of C declarations. But I think I get it now.

First of all, you have to understand that a C declaration starts with one single base type followed by a sequence of fragments of declarations; you essentially can interpret this as a sequence of separate declarations, each created by plugging the base type into each separate fragment. Syntactically, the "hole" inside each fragment actually contains the name of the identifier being bound; conceptually, you pull out that identifier and bind it to the type you get by plugging the base type into the position where you found the identifier.

For example:

int x, *y, z[3];

declares an int x, an int pointer y, and an int array z. Now for function types, the base type is interpreted as the return type; in other words, a fragment of a declaration of function type has its "hole" in the return type position. So:

int x, f(char);

declares an integer x and a function f of type char → int. Next we have to worry about pointer types. Oh, pointer types. First of all, you have to know that pointer types in the declaration are associated with the fragments, not the base type. So:

int *p, x;

declares an int pointer p and a plain int x. Now, notice that the asterisk is a prefix operator, whereas the function and array type constructors are postfix operators. So now we get to worry about precedence. You just have to remember that the asterisk binds loosest. So:

int *f(char);

is a function that returns an int pointer, whereas

int (*f)(char);

is a pointer to a function that returns an int. (You can throw in parentheses most anywhere in these things; forgot to mention that.) Okay, but here's the kicker: the nesting of type constructors is interpreted inside-out. Consider:

int (*(foo[3]))(char);

((Not that it helps, but I've over-parenthesized to avoid precedence issues.)) If you're still trying, you might be tempted to read this as declaring a function that returns an array of int pointers, or maybe a pointer to an array of ints. But the inner-most syntactically nested type constructor is interpreted as the outer-most semantically nested type constructor. So foo is in fact an array of pointers to functions.

My first PLT patch

I've submitted my first patch to the internals of PLT Scheme. It's a tiny thing: the ability to unquote inside a quasiquoted hash-table literal, e.g.:

> `#hash((x . ,(+ 1 2)))
#hash((x . 3))

And Matthew had to fix up some issues with it.

But anyway, making contributions to PLT is easier these days due to a couple of factors. First, the creation of plt-dev, a public mailing list for discussing the development of PLT Scheme, means that there's better support for people who want to contribute. Second, I'm told that more of the internals of PLT Scheme are self-hosted than apparently they used to be, i.e. a lot of PLT Scheme is itself implemented in PLT Scheme. This makes it a lot less scary to dive into the code.

The C Typedef Parsing Problem

The well-known "typedef problem" with parsing C is that the standard C grammar is ambiguous unless the lexer distinguishes identifiers bound by typedef and other identifiers as two separate lexical classes. This means that the parser needs to feed scope information to the lexer during parsing. One upshot is that lexing must be done concurrently with parsing. That's standard, although because parser generators usually allow fixed lookahead, you have to pay very close attention to making sure the lexer stays properly in synch with the parser, even when it gets ahead. For example:

typedef int my_int;
my_int x;

At the semicolon, the type environment needs to be updated with an entry for my_int. But if the lexer has already looked ahead to my_int, it will have lexed it as an identifier rather than a type name. But this is just a small matter of heroic hacking.

The real problem is a larger engineering one. Just to parse a program, you need to have the full type environment. And the program you're parsing may have included other programs. So if you want to write tools that perform analyses on fragments of C, you still have to feed them the entire environment one way or another. Either that becomes a requirement you foist onto the user ("this tool takes two inputs: a fragment of C and an initial type environment"), or you only allow whole programs instead of fragments, or you use an ambiguous grammar with, say, a GLR parser and divine some clever disambiguation heuristics.

And of course, C's braindead non-module-system is just a preprocessor directive (#include). So if you punt and require whole programs, that means you have to implement the C preprocessor, too. Or at least feed it through an existing implementation of the C preprocessor. And then process stdio.h, stdlib.h, etc. etc. every time you analyze just about any C program. So then you start thinking about caching results of #include for efficiency...

All this because of one silly grammar ambiguity.

History lesson

A history and semantics lesson from Matthias on plt-scheme:

Normal order and applicative order are failed attempts to explain the nature of call-by-name programming languages and call-by-value programming languages as models of the lambda calculus. Each describes a so-called reduction strategy, which is an algorithm that picks the position of next redex BETA that should be reduced. By 1972, it was clear that instead you want different kind of calculi for different calling conventions and evaluation strategies (to the first outermost lambda, not inside). That is, you always reduce at the leftmost-outermost point in a program but you use either BETA-NAME or BETA-VALUE. Non-PL people were confused (and still are) because BETA-NAME looks like BETA but nearly 40 years later, everyone should figure this out. SICP was written when the majority of people were still confused. -- Matthias

A funny reader context

Trivia time: find a place in the Scheme reader where ,expr is not equivalent to (unquote expr).

Answer:

> (define ls '(1 2 3))
> `#(unquote ls)
#(1 2 3)
> `#,ls
#,ls

Using C to talk to C

I've released the first version of a PLaneT package for working with C. It's based on an idea I got from Felix Klock's Scheme Workshop 2008 paper: rather than try to do manual pointer arithmetic based on the current architecture's ABI, you can find out byte offsets of data structures by creating a C program that tells you what they should be. So that's what c.plt allows you to do; using a system-installed C compiler, you can generate a representation of the binary layouts of data structures. Here's a sample interaction:

> (define time.h
   (make-header
     #reader (planet dherman/c/reader) {
         struct tm {
             int tm_sec;
             int tm_min;
             int tm_hour;
             int tm_mday;
             int tm_mon;
             int tm_year;
             int tm_wday;
             int tm_yday;
             int tm_isdst;
         };
     }))
> (define time-abi
   (compile-header time.h
     (system-compiler #:include<> '("time.h") gcc)))
> (layout-size (time-abi 'tm))
36
> (layout-offset (time-abi 'tm) 'tm_sec)
0
> (layout-offset (time-abi 'tm) 'tm_year)
20

Quiz answer

Reader Mitch (not my advisor, apparently) comes closest to the answer to my quiz question:

Some kind of alignment thing? I can't think of how code would be affected by that, though.

As it happens, changing the code was affecting the particular size of the activation record allocated by the GCC-generated code. Somehow the extra code ended up with a slightly smaller activation record. And then it turned out that the slight difference (something like 8 or 16 bytes) was pushing the activation record over the edge of a page boundary. Boom!

It's still a mystery to me exactly how throwing in an asm("noop\n") can affect the size of the activation record. Such are the arcane mysteries of GCC code generation. I had to catch my flight home before Dave had worked out all the details but by now I bet he has an even better understanding of it. It was fun and inspiring to watch Dave's detective skills in action.

Quiz question

Here's a fun puzzle I watched Dave Mandelin track down yesterday. Why would adding a guaranteed no-op such as

if (FALSE) { printf("can't happen\n"); }

or even

asm("noop\n");

to the body of a procedure cause a program to run measurably and consistently faster? I'll post the answer later today. (Or as much as I understand, anyway.)

Java, we don't care about you

Joel Spolsky pretty much nails it.

I actually grabbed a screen shot of this very same dialog box some time last year because it was so absurd. The part that always amazes me is why people think customers are going to care about their product as much as they do. It seems to me that I'm more likely to be loyal to a technology brand that shows a little humility and restraint.