Hello, I'm iTunes.

Apple can make fun of Vista's pesky security dialogs, but do you know what they make me do every time a sub-point release of iTunes is available?

1. iTunes asks me if I want to download the latest version.
2. I click yes.
3. Firefox opens to an ad-filled page with a form in the corner.
4. I uncheck the first "do you want us to email ads to you?" question.
5. I uncheck the second "do you want us to email ads to you?" question.
6. Here's a secret: if you uncheck both those boxes, you don't have to fill in an email address.
7. I click the "download" button.
8. Firefox asks me what to do with the file.
9. I click "Save file".
10. I wait for a thirty-five megabyte download, even if it's just a small patch.
    
11. I close the "Downloads" dialog box.
12. I close Firefox.
13. I close iTunes.
14. I find the downloaded setup executable.
15. I double-click the setup executable.
16. I click "Next".
17. I click "I accept".
18. I click "Next".
19. I click "Install".
20. I wait several musicless minutes for it to completely overwrite the entire existing installation directory, even if it's just a small patch.
21. Guess what, it still installs QuickTime on the side, as if I had any more interest in QuickTime than I have for the last 15 years.
22. I click "Finish".
23. iTunes starts (automatically! gee whiz!).
    
24. The license agreement pops up again.
25. I click "I Agree".
26. I wait a minute for iTunes to "update the iTunes library".
27. Here's the best part: as with every single previous release, iTunes still decides that maybe this time I really do want a QuickTime icon in the system tray.
28. I right-click the QuickTime tray icon and choose "QuickTime Preferences" (er, I prefer not to know about QuickTime?)
29. I click the "Advanced" tab.
30. I uncheck the "Install QuickTime icon in system tray" option at the bottom.
31. I click "OK".

And now I'm back to having iTunes working the way it did before. Only, as far as I can tell, the sole distinguishing feature of the new version is that it no longer asks me if I want to upgrade. For the moment.

Update: It looks like iTunes 7.0.2 installed a new "Apple Software Update" program on my computer. Does this mean my post was just in time to be obsolete? Here's hoping.

Hygienic typedefs

ECMAScript Edition 4 will have ML/C-style typedefs to allow the creation of type synonyms. You can think of these like macros in that, intuitively, references to such types are substituted by their definitions. This is simpler than a general macro system, because they are only substituting types in type contexts, not expressions in expression contexts. But even though types are a simpler subset of the syntactic structure of ES4 programs, due to generics, they still have binding structure!

Consider this example:

class C.<T> {
   type A = T
   function f.<T>() {
       var x : A = ...
   }
}

If we want to substitute away the type definition, we might naively get:

class C.<T> {
   function f.<T>() {
       var x : T = ...
   }
}

But then x's type annotation is referring to the wrong T! This corresponds exactly to the notion from hygienic macros (commonly referred to as referential transparency) that references in a macro definition should retain their meaning from the macro definition environment, never the macro use environment.

In other words, the above program should really be resolved to:

class C.<T> {
   function f.<T'>() {
       var x : T = ...
   }
}

Now consider another example, this time with a parameterized typedef:

type A.<X> = function.<T>():[X,T]
class C.<T> {
   var a : A.<T> = ...
}

A naive substitution would produce

class C.<T> {
   var a : function.<T>():[T,T] = ...
}

This time the bug is that we've allowed a type definition to introduce a binding that captured a binding in the context of the use of the typedef. This is an example of the hygiene condition, which states that bindings introduced by a macro should not capture variables in the macro application site. The proper expansion of the typedef would instead be:

class C.<T> {
   var a : function.<T'>():[T,T'] = ...
}

These are exactly the same conditions that hygienic macro expanders must meet in order to prevent unintended variable capture; the only difference is that here we're concerned with type variables rather than program variables.

A little goes a long way

I just completed an automated, machine-checked simulation proof. What was my proof assistant? Scheme! The proof relies on some reduction relations and an inductively defined invariant relation. The former can be defined in PLT Redex with just a little cleverness for performing symbolic reduction; the latter can be defined with good, old-fashioned recursion.

Granted, there are a number of places where I could have gone wrong. For example, I have no meta-theorems about the correctness of the representation or the exhaustiveness of the manually directed case analysis (a dozen cases in as many lines of code). But implementing the proof on the computer helped me debug a number of minor issues in my theorem, and it did all the heavy lifting for me (particularly the multi-step reductions--thanks Robby and Jacob for PLT Redex!).

The moral? A little goes a long way, as Wand and Sullivan wrote. For a simple proof involving inductive invariants and lots of rote calculation, there's no need for complicated meta-logical frameworks. Implementing the proof in a general-purpose programming language gives you a higher degree of quality assuredness for a reasonable implementation cost.

Next, if I do more of these simulation proofs, I might start abstracting out the common patterns into a library to work in conjunction with PLT Redex. It would essentially be a simple proof assistant for simulations.

Lazy substitutions

Substitution is expensive. That's why we tend to use environments in efficient implementations of programming languages. They encode all the information we need to do substitutions, but we wait until as late as possible to perform the substitutions. The complication, however, arises when expressions containing free variables (i.e., variables that haven't yet been substituted) travel around to disparate parts of the program. This happens in the lambda calculus when functions get passed or returned as values, and that's why we have to introduce closures. Closures allow expressions with free variables to travel around with enough information to continue performing their lazy substitutions.

In macro systems, we have exactly the same problem: the substitutions we need to perform (among others) are fresh names for bound variables. We need to substitute these fresh names throughout the bodies of expressions, but it's expensive to revisit syntax. So we close expressions over their substitutions and rename lazily.

But in macro systems, these kinds of closures are even more complicated than in the lambda calculus, because each macro invocation produces more code and mixes it together with other code. What we want is for the renamings to occur only on the code as it appears at the particular time of the current macro invocation. So in Dybvig, Hieb and Bruggeman's macro-expansion algorithm, the solution is to produce a fresh "mark" or "time-stamp" distinguishing code that resulted from a particular macro invocation. This way, renamings are applied only to code that existed at the time that the eager substitution would have been applied. When different code gets mixed together from different macro invocations, these marks keep track of what renamings apply to what pieces of syntax.

There are two salient features required of these marks: 1) every distinct invocation of a macro should have a distinct mark associated with it, and 2) only new code produced by a macro invocation should be marked as new, not code that it received as input. The first requirement is satisfied simply by generating fresh marks on each invocation. The second is satisfied by giving the mark algebra a "toggling" feature: re-applying the same mark twice to a piece of syntax erases the mark. The expander marks both the input and output of each macro invocation, which has the effect of "staining" new syntax generated by the invocation.

Symbolic evaluation with PLT Redex

PLT Redex is a great tool for testing and debugging a small-step operational semantics (particularly a reduction semantics using Felleisen-style evaluation contexts). I've just learned it's also useful for doing symbolic evaluation, where a program term may contain symbolic placeholders for some of its subterms. This is important when doing proofs, where you want to know how a fragment of a program is going to reduce for an entire class of terms.

For example, in a simulation proof I'm writing, I want to reason about how a program fragment would reduce in any initial continuation K0. So I extended the grammar of continuations to include the form

K ::= ... | (sym variable)

i.e., an s-expression containing the symbol 'sym followed by any variable. Then I could represent the abstract continuation K0 as '(sym K0). That's all it took, and Redex happily reduced my program.

Of course, once the reduction sequence gets to the point where it's returning a value to the continuation K0, it gets stuck, because there are no reduction rules that operate on these symbolic terms. But that's fine, because I'll never need to do such concrete reasoning about abstract terms.