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.