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.

Unknown unknowns

I'm always pretty offended by people who intend to become programmers by taking a 1-week course on Java or reading a "Teach Yourself" tutorial. Here's Peter Norvig's advice on the topic. The more you know about programming, the more you become aware of your own limitations. People who think they can "pick up" programming quickly are blissfully ignorant of the vastness of their ignorance. I guess that's probably true of most skills.

Meta-mathematical reasoning

It's common in programming languages to write proofs about proofs. For example, when using a Gentzen-style deduction system for specifying a type system or a big-step operational semantics, we often write a proof by induction on the size of the proof tree of a derivation.

When proving type soundness, you can use a number of different dynamic semantics. It's sanest to attempt this with an operational semantics, but there are many flavors to choose from: big-step operational semantics, small-step semantics with compatibility rules for lifting the basic reductions into arbitrary evaluation contexts, small-step semantics with Gentzen-style rules for creating an inductive proof tree that lifts the reductions into evaluation contexts, or Felleisen-style small-step semantics where the evaluation contexts are reified as plain old mathematical objects.

The benefit of the latter is that it requires no meta-mathematical reasoning--this is not to say it's impossible to use any of the others to prove soundness, but it perhaps requires less subtlety to write a proof about ordinary objects than one about proofs.

It reminds me of what Andrew Pitts has been saying for a while about his and Gabbay's denotational framework for theories of binding. They originally formulated their theory by working in a different set theory (one invented in the early 20th century by Fraenkel and Mostowski), but discovered that this required a certain "meta-logical sophistication" that made their work less accessible:

[Pitts and Gabbay [2002]] expresses its results in terms of an axiomatic set theory, based on the classical Fraenkel-Mostowski permutation model of set theory. In my experience, this formalism impedes the take up within computer science of the new ideas contained in that article. There is an essentially equivalent, but more concrete description of the model as standard sets equipped with some simple extra structure. These so-called nominal sets are introduced by Pitts [2003], and I will use them here to express α-structural recursion and induction within "ordinary mathematics"...

From "Alpha-structural recursion and induction", p. 462

Again, I think the moral of the story is that when you place all the objects you want to reason about at the object level, you avoid the need for meta-reasoning, which can make your proofs simpler and more accessible.

Sigfpe explains comonads

I just discovered this very cool discussion of comonads, which starts with a really lovely review of monads. The basic idea: monads allow you to compose two functions that inject their inputs into some "fancy structure." If we have functions f : a → m b and g : b → m c (i.e., Kleisli arrows), we can lift g to a function m b → m (m c) by the law that m is a functor, and then use the "flattening" monad law to unwrap the extra layer of structure on the result. As sigfpe (what is his/her real name?) puts it: "twice as fancy is still just fancy." I like that this provides an intuition for monads using the map/flatten formulation, as opposed to the usual unit/bind formulation, while still preserving the notion of "plumbing."

As for comonads, I'm starting to see the duality: comonads allow us to take some things already inside some fancy structure and map them down to something outside of that structure. For functions (co-Kleisli arrows) f : m a → b and g : m b → c, we can map f to a function m (m a) → m b, compose this with g on one end and the comonad operation m a → m (m a) on the other to get a function m a → c.

I'm still working on understanding some of the applications.

Compiling to JavaScript

Treating JavaScript as a back-end for a compiler is becoming more and more popular. Here are some examples of compilers that already target JavaScript:

• Squeak Smalltalk
  
• Scheme
  
• NarrativeJS
  
• Links
  
• OpenLaszlo
  
• Lisp
  
• Java
  
• Java
  
• Java
  
• Cross-browser JavaScript
  
• C#
  
• Ruby
  

This has come up in some of the ECMA-TG1 discussions, and I think some of Edition 4 will help compiler writers, in particular proper tail calls. On the other hand, I'm not sure whether "compiling X to JavaScript" is always a priori a net gain.

Some of these compilers are more toys than anything else: people always get a kick out of translating idioms between languages. That's fun, if a little boring after a while. But a lot of these tools are aiming at building abstractions for web programming, which is much more ambitious.

If you can properly build an abstraction on top of the many incompatibilities and low-level details of web platforms, then the abstraction is probably appropriate. But without a model for the "ideal" behavior of web browsers as approximated by each of the real ones, then the abstraction is likely to be either crippled or flawed. In this case, adding this layer of indirection may actually be maddeningly difficult to work with when it fails. If it's too simplistic, you'll eventually have to give up and drop down to the lower layer. This might be fine, if there are "trap doors" -- such as a foreign interface to JavaScript -- that allow the programmer to dip into the lower level when necessary. But if the abstractions have flaws in them, debugging will have become worse than before, because it involves debugging through the extra level of abstraction, wading through generated code, understanding the compatibility layer, etc.

I still think these abstractions are an important goal, but the hard part isn't the compilers. It's understanding the models, i.e., the implicit specifications for web browsers. Apparently Ian Hickson has done a lot of great work compiling empirical data about the behavior of existing web browsers to infer the implicit specs for web standards. This kind of work is messy and tedious, but important.

You want REPL's? We got REPL's!

JavaScript programming desperately needs development tools. Luckily, it's got some.

• Stand-alone command-line JavaScript shell for any Unix, including cygwin
• Web application debugging environment for Firefox
• JavaScript debugger for Firefox
• Web-based JavaScript shell
  

It took me a long, long time to find a command-line shell I could build in Windows with nothing more than ./configure, make, make install.

A stack is a context zipper

An evaluation context is a tree, and the stack is a zipper representation of the tree, allowing the part that changes the most--the hole--to be updated in constant time. In a context-sensitive reduction semantics, which models control as a stack, the "focus-down" rules unzip the context all the way down to its redex.

One cool thing you can do with this is reconstruct the source program. Given an expression evaluation stack, first replace the hole with the current expression being evaluated, then zip the context back up, and voilà! the original source code. I'm doing this in my JavaScript stepper to provide an intuitive visualization of the evaluation context within each function activation.

The only catch is to handle cycles in the source code, either due to recursion or loops. I don't have to worry about recursion, because I'm only doing this for individual function activations. Loops shouldn't be too much trouble, since they never accumulate stack.