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.

Universal vs. existential properties of programs

There's an age-old debate about whether abstraction is an absolute necessity or an obstruction to programmer efficiency. It shows up in the static-vs.-dynamic typing war, the abstract datatypes-vs.-concrete representations war, etc. I've always suspected we'd be worse off if we let one side or the other win. Of course I don't claim to know how to resolve it, but I wonder if it would shed light on the issue to think about existential vs. universal properties of programs.

When you're debugging or testing code ("is it possible for this list to be empty?"), or when you're exploring an API at the REPL ("what happens when I pass the result of Foo to Bar?"), you're often looking to observe a single program trace that serves as a witness to an existential property. By contrast, when you're building robust systems, you often want to assert universal propositions about the code ("this function will only ever produce a non-negative integer").

When you're building a system, you want your invariants to be universally true. This is one place where enforcement of abstractions (as with static type systems) is important. Letting the software enforce the abstractions automates the process of verifying these properties.

When you're inspecting a system, though, you're often looking for particular, concrete examples. In my experience, people are better at going from the particular to the general rather than vice versa. I don't think we tend to think well in abstractions; at least not at first. That's why verifiers that work by searching for counterexamples produce such good errors: instead of directly proving ∀x.P(x), they try to prove ¬∃x.¬P(x), and if they fail, they give you a concrete x. Learning API's, interacting with the REPL, and writing test cases are all examples of this mode of programming where you're more interested in concrete paths through a program rather than universal properties.

How would we design software that facilitates both these modes of reasoning about programs?

Non-native shift/reset with exceptions, revisited

Filinski's implementation of shift and reset in terms of undelimited continuations and a mutable cell doesn't interact well with exceptions out of the box, but it turns out we can get the right behavior with only a slight modification. (Ryan, Jacob and I came up with this after John Reppy suggested it to me as a challenge that, if possible, would be far simpler to implement than a native implementation in SML/NJ.)

The problem is that, as Shan and Kiselyov point out, a delimited continuation should only close over the exception handlers (and dynamic parameters in general) bound up to its prompt, and when invoked, it should be invoked in the context of the handlers of the current global continuation extended by the handlers closed over by the delimited continuation. This really is the expected behavior; an exception raised in a delimited continuation should either be handled by an appropriate handler installed within the delimited context, or if there isn't one, by the global context in which the delimited continuation is being invoked.

For example, both of the following programs should evaluate to 100, since the exception inside the delimited continuation is raised within a new context that installs a handler for it:

;; handler installed in body of shift
(reset (lambda ()
         (+ (shift (lambda (k)
                     (with-handlers ([symbol? (lambda (exn) 100)])
                       (k 1))))
            (raise 'boo))))

;; handler installed in new context
(let ([k (reset (lambda ()
                  (shift (lambda (k) k))
                  (raise 'boo)))])
  (with-handlers ([symbol? (lambda (exn) 100)])
    (k 1)))

However, with Filinski's implementation applied naively to a language with exceptions, neither example manages to catch the exception because the delimited continuations close over the wrong exception handlers. However, we can get the right behavior with only a slight modification to the implementation. The trick is to modify the protocol between the captured Scheme continuations to pass an exception along from one context to another to be re-raised.

As before, we store the global continuation (or "meta-continuation") in the single mutable cell:

(define meta-k (lambda (x) (raise 'missing-reset)))

But we'll change the contract of the meta-continuation to accept two different variants of results, those representing a normal return from a delimited continuation, and those representing an unhandled exception that should be re-raised in the context of the meta-continuation's handlers:

(define-struct succeeded (result))
(define-struct failed (exception))

(This is the familiar pattern of representing different return paths in the exception monad.)

Now, reset needs to be modified to ensure that evaluation of the body of the prompt is wrapped in a handler to prevent uncaught exceptions from escaping to the original global continuation. The wrapped result is sent to the meta-continuation, and the context of the call/cc performs the unwrapping, either to return the ordinary value or re-raised the exception. (I've highlighted the new parts.)

(define (reset thunk)
  (let ([result
         (call/cc (lambda (k)
                    (let ([meta-k0 meta-k])
                      (set! meta-k (lambda (r)
                                     (set! meta-k meta-k0)
                                     (k r)))
                      (let ([v (with-handlers
                                   ([(lambda (exn) #t) make-failed])
                                 (make-succeeded (thunk)))])
                        (meta-k v)))))])
    (if (succeeded? result)
        (succeeded-result result)
        (raise (failed-exception result)))))

The only change to shift is that again, where it invokes the meta-continuation, it needs to wrap the result in this variant type. Because the meta-continuation is called here to represent the case where evaluation of the delimited continuation terminates successfully, we wrap the result with make-succeeded.

(define (shift f)
  (call/cc (lambda (k)
             (let ([v (f (lambda (v)
                           (reset (lambda ()
                                    (k v)))))])
               (meta-k (make-succeeded v))))))

That's it! Trying out the test cases above, we get 100 and 100, as we should.

This is also well-typed and implementable in SML, for example as a modification to Oleg's code.

POPL 2007 Program

I've found at least some version of all but two of the papers being presented at POPL next week. Here's a program with links to the papers I found.

Does type inference have to suck?

Type inference with tools like Haskell and SML obviously sucks. Hard. The error messages are useless. I have to pinpoint my errors manually, narrowing down the error by commenting out half the program at a time. Any time you're using binary search to find a bug, it's safe to say your debugging tools aren't helping you.

There's been a fair amount of pretty hardcore research on this. But does it really need to be hard? If I could just have some help from a modern IDE, it seems like type inference errors should be perfectly adequate. At the very least, the type inference engine could keep track of source location for every type constraint it acquires, and then when it finds conflicts, the GUI could simply draw an arrow between the two conflicting expressions. If it doesn't know which one is wrong, fine! I'll know which one is wrong, but it has to show me both!

SML/NJ's approach of picking one at random to blame is pure madness.

Another useful tool would be for the IDE to show me the inferred type of any expression in the program, so that if it's not manifest, I can at least make it manifest. Annotating one or two expressions at a time and recompiling is a colossal waste of time.

I've got plenty of criticisms for Eclipse, but if there's one thing we can learn from it, it's that compiled languages don't have to force the programmer into the edit-recompile cycle. It's perfectly possible these days to run the compiler incrementally and continuously. (Conversely, you could say that there's no reason why interpreted languages can't be incrementally compiled.)

I know I'm not the first to point this out. Why hasn't anyone in the statically-typed functional languages community done this? You don't need to reinvent the IDE, just build some plug-ins for emacs or Eclipse.

Dynamically optimizing dynamic dispatch

Robert O'Callahan just explained to me the basic optimization approach for dynamically typed languages that I've been hearing about lately. It's the approach used in the Strongtalk VM, recently mentioned by Avi Bryant and Gilad Bracha. At least, I think that's what they were talking about, but I didn't understand it until Robert explained it to me.

Performing a dynamic dispatch compiles into a branch deciding which class's method to invoke:

if (class == C) {
  C::foo();
}
else if (class == B) {
  B::foo();
}
else ...

With some runtime profiling, you can figure out which branch is most likely to occur and dynamically rewrite the branch so that the common case comes first in the branch.

if (class == B) {
  B::foo();
}
else if (class == C) {
  C::foo();
}
else ...

This then feeds into the hardware branch prediction.

With branch prediction, the hardware will keep some small history to help it predict which way to take. But if the particular branch in question is not in the history (say, because it's part of a loop with a large body whose branch history is bigger than the hardware branch history table), a conditional branch is an either-or; the branch predictor will still pick one. So as long as you structure the conditional so that the branch predictor will always guess the common path, even absent any branch history, it will still predict correctly in the common case.

This is something that you can't do with a vtable, because branch history tables are smaller for computed jumps (since each entry is a pointer rather than a single branch-taken/branch-not-taken bit), and because the hardware predictor can't guess right when it doesn't have a history.

You can then do even better by actually inlining the method body directly into the branching code, so it looks like

if (class == B) {
  // B::foo method body
}
else ...

and then even better, by merging several inlined methods in sequence. With some simple dataflow analysis on locals (between mutations), you can eliminate redundant checks. That is, code that looks like:

if (x.class == B) {
  // B::foo method body
}
else ...
if (x.class == B) {
  // B::bar method body
}
else ...

gets optimized to:

if (x.class == B) {
  // B::foo method body
  // B::bar method body
}
else ...

Non-native shift/reset with exceptions

Filinski's implementation of shift and reset has undesirable behavior in a language with exceptions. Consider the following example:

(reset (lambda ()
         (+ (shift (lambda (k)
                     (with-handlers ([symbol? (lambda (exn) 100)])
                       (k 1))))
            (raise 'boo))))

You'd expect this program to evaluate to 100, but with Filinski's implementation, it raises the uncaught exception 'boo. The same example with MzScheme's native delimited continuations yields 100.

Filinski's implementation of shift and reset

With the nice specification of shift and reset via local and global continuations, it's easier to understand Filinski's implementation in terms of a host language with undelimited continuations and mutable state. He uses a mutable cell to represent the global continuation:

(define meta-k (lambda (x) (raise 'missing-reset)))

The implementations of shift and reset push and pop representations of the local continuation onto this cell.

(define (reset thunk)
  (call/cc (lambda (k)
             (let ([meta-k0 meta-k])
               (set! meta-k (lambda (r)
                              (set! meta-k meta-k0)
                              (k r)))
               (let ([v (thunk)])
                 (meta-k v))))))

The reset function simulates pushing the local continuation onto the global one by updating it with a function that, when invoked, both pops the local continuation off (by simply mutating the global continuation back to its previous value) and jumps to the local continuation (by invoking the host language continuation captured by call/cc)--see the next-to-last eval rule. To ensure that the meta-continuation really does act like the global continuation, it is invoked on the result of the thunk; so even if the thunk never invokes a control effect, control eventually jumps to the initial global continuation.

(define (shift f)
  (call/cc (lambda (k)
             (let ([v (f (lambda (v)
                           (reset (lambda ()
                                    (k v)))))])
               (meta-k v)))))

The implementation of shift invokes its function argument and then forces a jump back to the global continuation afterwards--see the last eval rule. Even though the semantics suggests that the local continuation is immediately abandoned before evaluating the function argument, this implementation is morally equivalent; it doesn't bother to throw away the local continuation until after the function returns, but it still throws it away. The local continuation argument passed to the function argument is represented as a function that pushes the current local continuation onto the global continuation before jumping to the current local continuation--see the last cont1 rule.

Now, when taking into account proper tail recursion and space efficiency, this implementation is spectacularly wrong. Furthermore, stack reflection via language features like continuation marks will render this implementation inequivalent to native implementations of delimited control.

Shift and reset via two-continuations

I did a little pleasure-reading while I was out of town this weekend. Biernacki, Danvy, and Shan have a paper on delimited continuations with a nice formulation of shift and reset based on Filinski's specification. Filinski's approach is to evaluate every expression in two continuations. The first is the local continuation, representing the dynamic context up to the nearest delimiter. The second is the global continuation (which he calls the "meta-continuation"), representing everything above the delimiter. The nice thing about separating these two is that control effects are only able to affect the local continuation; the global continuation is completely off-limits to the user program.

Filinski uses a two-continuation version of CPS for his specification, but Biernacki et al give a nice CEK machine semantics (which I have a certain fondness for). The two continuations are represented as evaluation contexts, which themselves are represented as composable sequences of context frames.

The first rules specify the evaluation of a term. The interesting rules are the last two: installing a prompt promotes the current local continuation to "inviolable" status by placing it in the global continuation; and capturing the current local continuation removes it and stores it in the environment.

eval <x, e, C1, C2>     → cont1 <C1, e(x), C2>
eval <λx.t, e, C1, C2>  → cont1 <C1, [x,t,e], C2>
eval <t0 t1, e, C1, C2> → eval <t0, e, C1 o (t1 [])^e, C2>
eval <#t, e, C1, C2>    → eval <t, e, [], C2 o C1>
eval <Sk.t, e, C1, C2>  → eval <t, e[k := C1], [], C2>

The second set of rules represent returning a value to the local continuation. The most interesting rules is the last one, which represents applying a captured continuation: it simulates "returning" the operand to the captured continuation and saves the current local continuation in the global continuation, so as to preserve the current state of the computation.

cont1 <[], v, C2>                → cont2 <C2, v>
cont1 <C1 o (t [])^e, v, C2>     → eval <t, e, C1 o (v []), C2>
cont1 <C1 o ([x,t,e] []), v, C2> → eval <t, e[x := v], C1, C2>
cont1 <C1 o (C1' []), v, C2>     → cont1 <C1', v, C1 o C2>

The last rules represent returning values to the global continuation. If it has some local computing to do, that gets placed back into the local continuation, and otherwise it returns the final value.

cont2 <C2 o C1, v> → cont1 <C1, v, C2>
cont2 <[], v>      → v

This is a lovely presentation of delimited continuations. I'd also never thought of the connection between delimited continuations and two-continuation backtracking (having still never read Filinski's work).

Skolem meets Quine

How's this for the crazy hack of the day? I was writing a little code generator for SML (because as a Schemer in ML-land, it was only a matter of time before I'd start trying to write macros) and I wanted to use quasiquotation for constructing code. (I'm sure Lisp was the first programming language with quasiquotation, although the concept originated from logic, at least dating back to Quine.)

SML/NJ includes a quasiquotation facility, but you have to write your own parser for the object language. In this case, my object language was ML itself. So I wanted to reuse the ML parsing libraries that come with SML/NJ. But a quasiquoted source expression is a list of "fragments"--either a (quoted) string or an (unquoted) term:

datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a

So I needed a way to extend the existing parser to be able to parse not just raw ML source, but ML with holes in it.

My solution is to generate fresh variables at the holes (analogous to "Skolem constants" in a type inference algorithm) to 1) generate a single, parseable string; 2) parse that string using the existing parser; and then 3) replace instances of the fresh variables in the resulting AST with their original unquoted terms. Luckily the parser that comes with SML/NJ (from the MLRISC library) has a generic term-rewriting library so this last step was easy.

Here's the entire parser:

fun parseQuasiML frags =
   let fun skolemize [] = ([], [])
         | skolemize ((QUOTE s)::frags) =
               let val (ss, skolems) = skolemize frags
               in
                   (s::ss, skolems)
               end
         | skolemize ((ANTIQUOTE x)::frags) =
               let val skolem = gensym "qqSkolem"
                   val (ss, skolems) = skolemize frags
               in
                   (skolem::ss, (skolem, x)::skolems)
               end
       val (ss, skolems) = skolemize frags
       fun exp _ (e as (IDexp (IDENT ([], x)))) =
               (case lookup (x, skolems) of
                     NONE => e
                   | SOME e' => e')
         | exp _ e = e
       val NIL = MLAstRewriter.noRewrite
       val rw = #exp(MLAstRewriter.rewrite
                     {exp=exp,pat=NIL,decl=NIL,ty=NIL,sexp=NIL})
   in
       rw (parseMLExp (String.concat ss))
   end

The skolemize function traverses the list of fragments, generating fresh "skolem variables" for each unquoted term. The ML parser then parses the resulting string. The last part (the exp function and MLAstRewriter.rewrite) simply uses the rewriter module to replace any instances of IDexp (an AST representing an ML variable reference) that contain skolem variables with their original, unquoted terms, and otherwise leave the expressions intact.

Update: Bawden suggests that quasiquotation (or at least the term "quasiquotation") is indeed due to Quine.

Temporarily violating invariants

Standard ML doesn't allow you to put anything on the right-hand side of a val rec declaration except for a lambda expression. This means that you can't create a cyclic data structure unless you use a ref cell with an option type inside it, temporarily create the cell to be empty, and then immediately mutate it to SOME of its contents. Unfortunately, this means that a) you always have to refer to that value by dereferencing it, and b) you can't enforce that the ref cell won't be assigned to later.

I found an old discussion on comp.lang.ml about this, where Xavier Leroy explains that you could in fact relax the restriction to allow not just syntactic functions but variable references, constants, and constructor applications on the right-hand side of a val rec, since none of these expression forms cause side effects. The underlying language implementation would temporarily create an empty data structure and mutate it, but this would never be observable to the program. Leroy claims you need all sorts of crazy math to prove it, but it should actually be simple to prove operationally.

Just to free associate for a moment, this also reminds me of dynamic code-rewriting techniques, such as JIT compilation or dynamic optimization based on runtime profiling. If you can prove that a dynamic drop-in replacement is observationally equivalent, you can push the temporary mutation down under the model/hood and make the object language safer.

In the spirit of Alan Perlis...

"The pain of testing for bottom-up development is producing test data without a front-end. The pain of testing for top-down development is that you can't."

- Richard Cobbe

Stacked contracts are not intersection types

In contract systems like PLT Scheme's, a value can acquire multiple contracts during control flow. For example, a value might get passed to and returned from a function with a C → C contract, and then later passed to and returned from a funtion with a D → D contract. This value will now be dynamically wrapped with both C and D contracts. Conceptually, this means that the value must satisfy the constraints of both C and D. I was long tempted to think of this like an intersection type: the value "is a C and a D".

But this intuition will lead you astray. Here's a simple example of stacked contracts which do not behave like intersection types at all:

(module wrap-int mzscheme
  (require (lib "contract.ss"))
  (define (wrap-int f) f)
  (provide/contract
   [wrap-int ((integer? . -> . integer?) . -> .
              (integer? . -> . integer?))]))

(module wrap-bool mzscheme
  (require (lib "contract.ss"))
  (define (wrap-bool f) f)
  (provide/contract
   [wrap-bool ((boolean? . -> . boolean?) . -> .
               (boolean? . -> . boolean?))]))

(module main mzscheme
  (require wrap-int wrap-bool)
  (define id (wrap-int (wrap-bool (lambda (x) x))))
  (provide id))

The first two modules both provide functions that take in a function argument and return it wrapped with integer → integer and boolean → boolean contracts, respectively. The main module then wraps the identity function in both of these contracts.

Now, if these were to behave like intersection types, the identity function would have type integer → integer ∧ boolean → boolean, and would be perfectly well-typed.

But with contracts, the function's contracts are checked one piece at a time by checking all arguments against all the contracts' domains and all results against all the contracts' ranges. This means that if we apply id to any value, it will be checked to be both an integer and a boolean. And if it ever produces a result (it won't) that result will also be checked to be both an integer and a boolean. That is, the resulting contract is more analogous to (integer ∧ boolean) → (integer ∧ boolean) than to (integer → boolean) ∧ (integer → boolean).

Lambdas everywhere

From Mitch Wand's lecture notes for CSG264, Semantics of Programming Languages:

+----------------------------------------------------------------+
| Key questions:                                                 |
|                                                                |
|                                                                |
|            Syntax: What _is_ a program?                        |
|                   |                                            |
|                   |                                            |
|                   |                                            |
|                   |                                            |
|            Operational Semantics: What does a program compute? |
|                  /\                                            |
|                 /  \                                           |
|                /    \                                          |
|               /      \                                         |
|              /        \                                        |
|             /          \                                       |
|            /            \                                      |
|           /              \                                     |
| Equational Theories:      Denotational Semantics:              |
| When are two expressions  What does an expression mean?        |
| equivalent?                                                    |
+----------------------------------------------------------------+

I think I need more sleep--I'm seeing lambdas everywhere...

Even may not be odd after all

Yesterday I complained that even streams can lead to unenforced dependencies between computations. In fact, I think there isn't a problem, at least in the usual implementation strategy. As long as you implement a non-empty stream as a promise of a pair, rather than a pair of promises (or a promise of a pair of promises), you can guarantee the right order of evaluation.

Let me actually test my point this time. First we need an effectful stream computation:

(define (make-reader in)
  (stream-delay
   (let ([first (read in)])
     (if (eof-object? first)
         stream-null
         (stream-cons first (make-reader in))))))

This function creates a stream by reading from an input port, so the order in which its cells are computed is significant. Now here are two different implementations of stream-map:

(define (stream-map1 proc str)
  (stream-delay
   (if (stream-null? str)
       stream-null
       (stream-cons (proc (stream-car str))
                    (stream-map1 proc (stream-cdr str))))))

(define (stream-map2 proc str)
  (stream-delay
   (if (stream-null? str)
       stream-null
       (let ([rest (stream-map2 proc (stream-cdr str))])
         (stream-cons (proc (stream-car str)) rest)))))

The second implementation forces the tail of the list before the head. When I tried these both in PLT Scheme, they evaluated the same:

> (stream→list
   (stream-map1 add1 (make-reader
                      (open-input-string "0 1 2 3 4"))))
(1 2 3 4 5)
> (stream→list
   (stream-map2 add1 (make-reader
                      (open-input-string "0 1 2 3 4"))))
(1 2 3 4 5)

There you have it: the SRFI 40 implementation of even streams (at least the reference implementation and PLT Scheme implementation) doesn't exhibit a sensitivity to the order of observation of elements of a lazy pair.

Now, to make this falsifiable, I should demonstrate a broken implementation of even streams, to watch the same test fail. Uh... exercise for the reader.

Even can be odd

Wadler et al's criticism of the "odd" style of laziness is that it forces some unnecessary (and possibly unwanted) computation. Because only the tail of a stream is delayed, a stream-valued function always computes the head eagerly, even when it isn't needed. They show an example like the following, where taking a prefix of a stream still ends up computing too much because take can't prevent stream-map from computing the first element of the unwanted suffix:

...
→ E[(take 0 (stream-map div (countdown 0)))]
→ E[(take 0 (cons (div 0)
                  (delay
                   (stream-map div (countdown -1)))))]
→ error: division by zero

Their point is well-taken: languages like Haskell have a clearer model of need, and the SICP style of semi-lazy lists is, well, a bit odd.

But today Richard Cobbe warned me of an important subtlety with the authors' proposed "even" streams. Making streams fully lazy, so that neither the head nor the tail is forced unless it is observed, effectively removes any enforcement of order between their computations. In a pure functional language like Haskell, this is fine, but if your stream abstraction is built on top of, say, file I/O, it's all too easy to perform a simple refactoring like lifting a recursion into a let-bound variable:

(define (f str)
  ... (let ([rest (f (stream-cdr str))])
        ... (stream-car str) ... rest ...))

and suddenly you'll find your result stream is backwards, or even permuted!

I'm actually surprised the monadologists in question didn't address this (I've only skimmed the paper, so maybe I missed it). Monads add strictness to a non-strict language to pave the way for side effects, so naturally adding non-strictness to a strict language that already had side effects is going to be tricky.

I don't have any great categorical magic tricks to offer as a solution. But I imagine you could enforce the dependency by brute force: use even streams, except implement stream-cdr in such a way that it first forces the evaluation of the head.

Now I need to read SRFI-45 to understand the subtleties of tail-safe lazy computation, and then maybe I'll finally start feeling comfortable writing stream abstractions in Scheme. I really want to use streams: they make excellent abstractions of many I/O patterns. But they are fiendishly subtle.