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.
Monday, November 27, 2006
Wednesday, November 15, 2006
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:
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
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 ...if (class == B) {
B::foo();
}
else if (class == C) {
C::foo();
}
else ...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 ...if (x.class == B) {
// B::foo method body
}
else ...
if (x.class == B) {
// B::bar method body
}
else ...if (x.class == B) {
// B::foo method body
// B::bar method body
}
else ...Monday, November 13, 2006
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:
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.(reset (lambda ()
(+ (shift (lambda (k)
(with-handlers ([symbol? (lambda (exn) 100)])
(k 1))))
(raise 'boo))))
Sunday, November 12, 2006
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:
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.
The implementations of shift and reset push and pop representations of the local continuation onto this cell.(define meta-k (lambda (x) (raise 'missing-reset)))
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 (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 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.(define (shift f)
(call/cc (lambda (k)
(let ([v (f (lambda (v)
(reset (lambda ()
(k v)))))])
(meta-k v)))))
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.
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.
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.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 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.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>
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).cont2 <C2 o C1, v> → cont1 <C1, v, C2>
cont2 <[], v> → v
Thursday, November 09, 2006
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:
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:
Update: Bawden suggests that quasiquotation (or at least the term "quasiquotation") is indeed due 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:
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.datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a
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:
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.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
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.
Thursday, October 26, 2006
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
Friday, October 20, 2006
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:
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).
But this intuition will lead you astray. Here's a simple example of stacked contracts which do not behave like intersection types at all:
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.(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))
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).
Thursday, October 05, 2006
Lambdas everywhere
From Mitch Wand's lecture notes for CSG264, Semantics of Programming Languages:
I think I need more sleep--I'm seeing lambdas everywhere...+----------------------------------------------------------------+
| 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? |
+----------------------------------------------------------------+
Tuesday, August 29, 2006
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:
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.
Let me actually test my point this time. First we need an effectful stream computation:
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 (make-reader in)
(stream-delay
(let ([first (read in)])
(if (eof-object? first)
stream-null
(stream-cons first (make-reader in))))))
The second implementation forces the tail of the list before the head. When I tried these both in PLT Scheme, they evaluated the same:(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)))))
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.> (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)
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.
Monday, August 28, 2006
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:
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:
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.
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....
→ E[(take 0 (stream-map div (countdown 0)))]
→ E[(take 0 (cons (div 0)
(delay
(stream-map div (countdown -1)))))]
→ error: division by zero
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:
and suddenly you'll find your result stream is backwards, or even permuted!(define (f str)
... (let ([rest (f (stream-cdr str))])
... (stream-car str) ... rest ...))
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.
Sunday, August 27, 2006
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.
Friday, August 25, 2006
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:
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.
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.
Wednesday, August 09, 2006
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.
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.
Tuesday, August 08, 2006
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:
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.
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.
Thursday, August 03, 2006
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
Tuesday, August 01, 2006
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.
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.
Wednesday, June 28, 2006
Backwards compatibility
One of the biggest lessons I've learned from the ECMA process is how critical backwards compatibility is. When you have millions of users, the enormous weight of existing software holds you back from doing just about anything that breaks compatibility. An email from Brendan on the ES4 public mailing list (you have to subscribe to the mailing list to view the original email) crystallizes the difference:
...we are not breaking backward compatibility except in selected and few ways that actually improve the bugscape.In other words, if you expect that a break in compatibility will cause fewer bugs than it fixes, then it's acceptable.
Wednesday, June 21, 2006
A semantics for prophecies
Here's a quick sketch of a semantics for prophecies. Let's model a multi-threaded mini-Scheme where thread interleaving is represented by non-deterministically choosing a thread from a list of active threads and reducing it one step:
(e1, ..., E[e], e2, ...) → (e1, ..., E[e'], e2, ...)We also need a store to represent creating and updating prophecy queues. So the rule for cleaning up a terminated thread looks like:
<(e1, ..., v, e2, ...), σ>And beta-reduction occurs in a thread like so:
→ <(e1, ..., e2, ...), σ>
<(e1, ..., E[((lambda (x) e) v)], e2, ...), σ>Creating a new prophecy causes a new thread to be spawned and allocates a new, empty queue on the store. The prophecy's thread marks its context with the location of the queue so that subsequent calls to yield will know where to store their values.
→ <(e1, ..., E[e[v/x]], e2, ...), σ>
<(e1, ..., E[(prophecy e)], e2, ...), σ>When yielding a value, we look up the current thread's prophecy context to find its associated queue, and add the value to the queue. (Because this is an atomic step, queue updates are thread-safe.)
→ <(e1, ..., E[<prophecy: i>], e2, ..., e'), σ[i := <queue:>]>
where e' = (prophecy-context i e)
<(e1, ..., E[(yield v)], e2, ...), σ>Finally, reading a prophecy off the queue succeeds whenever the queue is non-empty.
→ <(e1, ..., E[null], e2, ...), σ[i := <queue: v1, ..., vn, v>]>
where E = (prophecy-context E0)
and σ[i] = <queue: v1, ..., vn>
<(e1, ..., E[(prophecy-next <prophecy: i>)], e2, ...), σ>Conspicuously missing from this first draft: the stop-iteration exception (because I didn't feel like adding exceptions to the model), and prophecy->stream, which really can be considered a library function added on top, implementable in a language with delay and force by means of a recursive function that produces null when it catches the stop-iteration exception.
→ <(e1, ..., E[v1], e2, ...), σ[i := <queue: v2, ..., vn>]>
where E ≠ (prophecy-context i E0)
and σ[i] = <queue: v1, v2, ..., vn>
The prophecy was unclear
My explanation of prophecies wasn't very clear. Ezra Cooper asked in the comments:
When any other thread requests a value from the prophecy, it either dequeues the first yielded value, blocks if no values have yet been queued, or raises a stop-iteration exception if the prophecy is complete (i.e., the prophecy background thread has terminated and all yielded values have been dequeue).
But in my servlet example, each page in the servlet only wants to read one single yielded value, so there's no need to block the page from loading until all the values have been yielded. That's why the prophecy->stream library function provides a lazy stream view of the prophecy which the servlet can use to pull items off the queue by need. That is:
You say that the subexprs of the prophecy form are evaluated in a separate thread; is each one evaluated in its own separate thread? Or is one background thread generated for that whole prophecy? What happens after yielding--it queues up a value for other threads, but what does the present thread do?The idea is that a prophecy form spawns one single background thread, which immediately goes to work evaluating the prophecy's subexpressions sequentially. Within that thread, each call to yield queues up its value and the thread immediately continues evaluating (this is in contrast to generators, which cause a transfer of control upon a yield).
When any other thread requests a value from the prophecy, it either dequeues the first yielded value, blocks if no values have yet been queued, or raises a stop-iteration exception if the prophecy is complete (i.e., the prophecy background thread has terminated and all yielded values have been dequeue).
But in my servlet example, each page in the servlet only wants to read one single yielded value, so there's no need to block the page from loading until all the values have been yielded. That's why the prophecy->stream library function provides a lazy stream view of the prophecy which the servlet can use to pull items off the queue by need. That is:
This procedure generates a web page that shows a view over the first item in the stream, with a link to display the next. When the user goes back to the previous page and reclicks the link, the servlet simply reloads this same stream (which was the cdr of the previous page's stream). In other words, we've effectively masked out any mutation. The streams provide a lazy view of an immutable sequence of values, but which are produced "eagerly" in a background thread by the prophecy.(define (view stream)
(if (null? (force stream))
;; produce a web page signalling that we're done
'(html (body "DONE"))
;; produce a web page displaying the first item in the stream
(send/suspend/dispatch
(lambda (proc->url)
`(html
(body
(p ,(render-item (car (force stream))))
;; a link to view the next item in the stream
(p ,(a ([href ,(proc->url
(lambda (request)
(view (cdr (force stream)))))])
"Next"))))))))
Tuesday, June 20, 2006
Prophecies: future-generators
I've discovered a neat idiom. I have a web servlet that spawns a separate process and reads a bunch of terms from the process's output. I want to be able to view those terms one at a time in the web page, but I don't want to leave the process hanging indefinitely based on the user's interaction. At the same time, I want it to be safe for clone/back as all web programs should. So the program should be able to process the terms in a lazy fashion, and allow backtracking (without having to re-read terms after backtracking), but the actual reading of the terms should happen concurrently in order to close the separate process as soon as possible.
This is a sort of combination of generators, which allow programmers to separate producers from consumers, and futures, which are a concurrent variation of laziness, where evaluation of a subexpression can happen concurrently, but evaluation of the containing expression must block if it needs the value of the subexpression.
Let's call these future-generators "prophecies." We create a prophecy with a special syntax whose subexpressions are evaluated immediately but in a separate thread from the creator of the prophecy:
We can access the yielded values with a library function prophecy-next, which takes a prophecy and blocks until there is a value available, or raises the sentinal value stop-iteration to indicate that "the prophecy is fulfilled."
Or we can extract the values lazily with a stream with prophecy->stream, which produces a stream, where (streamof a) = (promiseof (union null (cons a (streamof a)))).
Now my servlet is easy to write:
Update: Added to PLaneT.
This is a sort of combination of generators, which allow programmers to separate producers from consumers, and futures, which are a concurrent variation of laziness, where evaluation of a subexpression can happen concurrently, but evaluation of the containing expression must block if it needs the value of the subexpression.
Let's call these future-generators "prophecies." We create a prophecy with a special syntax whose subexpressions are evaluated immediately but in a separate thread from the creator of the prophecy:
The difference between this and traditional generators is that yield does not halt evaluation in the current local evaluation context, which is happening in a separate thread. It simply queues up the value to make it accessible to the rest of the world.(let ([p (prophecy
(yield 1)
(yield 2)
(yield 3))])
...)
We can access the yielded values with a library function prophecy-next, which takes a prophecy and blocks until there is a value available, or raises the sentinal value stop-iteration to indicate that "the prophecy is fulfilled."
Or we can extract the values lazily with a stream with prophecy->stream, which produces a stream, where (streamof a) = (promiseof (union null (cons a (streamof a)))).
Now my servlet is easy to write:
The separate program launches immediately, and all its output is read in as soon as possible. But the terms are packaged up via a prophecy into a lazy stream, which the web servlet reads in one page at a time. Users can safely backtrack, clone windows, and/or refresh any of the pages in the interaction, and the values always appear in the proper sequence, without ever having to regenerate them from the separate process.(define (start request)
(let ([p (prophecy
... (launch "prog.exe") ...
(let loop ()
... (yield (read-term)) ...)])
(go (prophecy->stream p))))
(define (go stream)
(if (null? (force stream))
`(html (body "DONE"))
(send/suspend/dispatch
(lambda (proc->url)
`(html
(body
(p ,(format "~a" (car (force stream))))
(p (a ([href ,(proc->url (lambda (req)
(go (cdr (force stream))))
"Next"))))))))
Update: Added to PLaneT.
Wednesday, June 14, 2006
Formalizing JavaScript
Last week I gave a talk at the UCSC Software Engineering Seminar entitled Formalizing JavaScript.* I talked about the approach I've been taking to specifying the operational semantics of JavaScript, in terms of both the formal approach to the model and the engineering of the executable model.
*You'll probably want a better cursive font than Comic Sans MS, such as Monotype Corsiva, Textile, or one of the Chancery fonts.
Update: I've written up some notes to accompany the talk as well.
*You'll probably want a better cursive font than Comic Sans MS, such as Monotype Corsiva, Textile, or one of the Chancery fonts.
Update: I've written up some notes to accompany the talk as well.
Tuesday, May 30, 2006
Customized literals in ECMAScript 4
One neat little feature that has come up in the design of ECMAScript Edition 4 is the ability to define conversions between datatypes. Class-based OO is nice for some purposes, and is certainly popular, but the ability to use syntactic literals to construct data is nice, and usually disappears when you "upgrade" to a bondage-and-discipline language like Java.
In ES4, it looks like you'll be able to define a sort of customized literal syntax for any class by means of an automatic conversion method. For example, imagine the following code:
We achieve this by defining a conversion method on the Color class:
In ES4, it looks like you'll be able to define a sort of customized literal syntax for any class by means of an automatic conversion method. For example, imagine the following code:
We can define a Color class with whatever methods we want (such as toCMYK) while still constructing one with a simple, lightweight array literal syntax.var kleinBlue : Color = [ 0x00, 0x2F, 0xA7 ]
...
kleinBlue.toCMYK()
...
We achieve this by defining a conversion method on the Color class:
class Color {
...
type RGB = [ UInt, UInt, UInt ]
function to(triple : RGB) {
type switch (triple) {
case ([ r, g, b ] : RGB) {
return new Color(...)
}
}
}
}Friday, May 26, 2006
ECMAScript reference values
Try this in SpiderMonkey or Firefox:
function foo(flag) {
if (flag) {
print('hello') = 10
}
return 42
}
foo(false) // 42
foo(true) // SyntaxError: invalid assignment left-hand sideTuesday, May 23, 2006
Solving today's web problems
Gilad Bracha's provocative Will Continuations Continue? has stirred up some controversy this week. His objection to continuations stems from the observation that in Ajax applications, the back button is less important than in traditional web programs, sometimes even effectively disabled. For an architect deciding whether to implement continuations for a web framework or its underlying VM, this has to alter the equation. Are Ajax applications rendering continuations obsolete? [1]
I'm a little late to respond, thanks to several days of netlessness. Gilad's post has generated some thoughtful discussion: Tim Bray protests that the web's simple UI model is well understood by users, Don Box points out that the web is not necessarily the only killer app for continuations, and Avi Bryant explains a few of the different kinds of state in web applications and where continuations fit into the picture. Later, Ian Griffiths raises deeper technical complaints about server-side continuations persistence about resource management (what happens when the user walks away?) and thread migration; Ezra Cooper responds that these problems don't exist for Links, where continuations live on the client side.
What makes Gilad's argument unrealistic is that Ajax applications currently account for some miniscule percentage of the web. Even if interactive applications are the future, the web never forgets its past. It's as naive to think you can stop supporting the back button as it would be for browsers to stop supporting HTML 4. You could protest that only the browsers have to support these "legacy" web pages, whereas on the server side, web programmers should start writing Ajax apps right now. But I don't see amazon.com or hotwire.com throwing away their shopping carts in favor of a Ruby on Rails codebase. There are way more existing applications with huge codebases that could benefit from a backwards-compatible solution to the Orbitz problem than there are companies itching to throw their entire codebase away to make way for an all-Ajax site.
None of this changes the fact that adding continuations to the JVM isn't easy. It's still a design decision with the attendant trade-offs. But speculation that everyone will be writing programs that make no use of the back button, say, 10 years from now, is not a compelling excuse not to support those programs now.
[1] As a pedantic aside, continuations could no more become obsolete than variables, or functions, or algorithms could. Continuations are an abstract concept, not a programming construct. More precisely, the real question is whether Ajax applications are rendering obsolete the use of first-class continuations as an implementation strategy for web application frameworks. In particular, I think a number of people have the misconception that programmers have to understand and use call/cc in order to program with these frameworks. In fact, the frameworks only use continuations under the hood to allow the programmer to write their web programs in a natural style.
I'm a little late to respond, thanks to several days of netlessness. Gilad's post has generated some thoughtful discussion: Tim Bray protests that the web's simple UI model is well understood by users, Don Box points out that the web is not necessarily the only killer app for continuations, and Avi Bryant explains a few of the different kinds of state in web applications and where continuations fit into the picture. Later, Ian Griffiths raises deeper technical complaints about server-side continuations persistence about resource management (what happens when the user walks away?) and thread migration; Ezra Cooper responds that these problems don't exist for Links, where continuations live on the client side.
What makes Gilad's argument unrealistic is that Ajax applications currently account for some miniscule percentage of the web. Even if interactive applications are the future, the web never forgets its past. It's as naive to think you can stop supporting the back button as it would be for browsers to stop supporting HTML 4. You could protest that only the browsers have to support these "legacy" web pages, whereas on the server side, web programmers should start writing Ajax apps right now. But I don't see amazon.com or hotwire.com throwing away their shopping carts in favor of a Ruby on Rails codebase. There are way more existing applications with huge codebases that could benefit from a backwards-compatible solution to the Orbitz problem than there are companies itching to throw their entire codebase away to make way for an all-Ajax site.
None of this changes the fact that adding continuations to the JVM isn't easy. It's still a design decision with the attendant trade-offs. But speculation that everyone will be writing programs that make no use of the back button, say, 10 years from now, is not a compelling excuse not to support those programs now.
[1] As a pedantic aside, continuations could no more become obsolete than variables, or functions, or algorithms could. Continuations are an abstract concept, not a programming construct. More precisely, the real question is whether Ajax applications are rendering obsolete the use of first-class continuations as an implementation strategy for web application frameworks. In particular, I think a number of people have the misconception that programmers have to understand and use call/cc in order to program with these frameworks. In fact, the frameworks only use continuations under the hood to allow the programmer to write their web programs in a natural style.
Friday, May 19, 2006
Late and early binding
It's taken me a long time to figure out what people mean when they talk about "late binding" and "early binding." Little by little, I was beginning to get a handle on it, when Brendan showed me this Python spec which used the terms to refer to order of expression evaluation in a syntactic form! According to the spec's terminology, evaluating an expression earlier is ostensibly "early binding." This freaked me out, but Brendan reassured me that this was probably just a misuse of terminology on the part of the Pythonistas.
At any rate, as I understand them, late and early binding describe the point in the lifetime of a computer program (usually, compile-time versus runtime) at which a particular variable reference becomes dereferenced, i.e., at what point its binding is discovered. Lisp, which is dynamically scoped, doesn't dereference function arguments until runtime, based on the dynamic context. Scheme variables, by contrast, can be early bound, since all variables' bindings are based on their lexical scope. Dynamic dispatch is another instance of late binding, where method names are resolved at runtime.
Dynamic scope is generally regarded as a liability, because it completely violates abstractions, exposing programmers' choice of variable names and making them vulnerable to accidental capture. Dynamic dispatch is a somewhat more restricted form of late binding, where the programmer has finer control over what names can be overridden by unknown external parties.
Compiler writers like early binding because it's an opportunity for optimization--variable references can be compiled into direct pointer dereferences rather than map lookups. From the perspective of program design, early binding is good because it results in clearer programs that are easier to reason about. However, in certain restricted forms, late-bound variables can be useful as a way of leaving a program open to subsequent extension. This is the purpose behind dynamic dispatch, as well as implicit parameters such as in MzScheme or Haskell.
At any rate, as I understand them, late and early binding describe the point in the lifetime of a computer program (usually, compile-time versus runtime) at which a particular variable reference becomes dereferenced, i.e., at what point its binding is discovered. Lisp, which is dynamically scoped, doesn't dereference function arguments until runtime, based on the dynamic context. Scheme variables, by contrast, can be early bound, since all variables' bindings are based on their lexical scope. Dynamic dispatch is another instance of late binding, where method names are resolved at runtime.
Dynamic scope is generally regarded as a liability, because it completely violates abstractions, exposing programmers' choice of variable names and making them vulnerable to accidental capture. Dynamic dispatch is a somewhat more restricted form of late binding, where the programmer has finer control over what names can be overridden by unknown external parties.
Compiler writers like early binding because it's an opportunity for optimization--variable references can be compiled into direct pointer dereferences rather than map lookups. From the perspective of program design, early binding is good because it results in clearer programs that are easier to reason about. However, in certain restricted forms, late-bound variables can be useful as a way of leaving a program open to subsequent extension. This is the purpose behind dynamic dispatch, as well as implicit parameters such as in MzScheme or Haskell.
Resumable exceptions
One more thing I learned from Avi: there's a simpler way to implement resumable exceptions than the way I'd thought of. Having been perverted by my formative years as a Java programmer, I always assume the meaning of throw was carved in stone tablets:
I suppose this means the handler runs on top of the portion of the stack where the raise happened, and there must be some provision for what to do if the handler finishes without a control operation; presumably this would have the same behavior as resume nil, or however you'd express "don't unwind the stack; resume where the exception occurred; but I don't have any useful result value for the failed operation."
- Thou shalt abandon thy current context.
- Thou shalt unwind the stack, verily, until thou findest the first handler.
I suppose this means the handler runs on top of the portion of the stack where the raise happened, and there must be some provision for what to do if the handler finishes without a control operation; presumably this would have the same behavior as resume nil, or however you'd express "don't unwind the stack; resume where the exception occurred; but I don't have any useful result value for the failed operation."
My introduction to Smalltalk
Another highlight of my trip to Amsterdam this week was meeting Avi Bryant, of Seaside fame. We talked about Smalltalk, web programming, and his latest project, Dabble. In the past, I've had trouble knowing where to begin with Smalltalk, so he sat down with me and walked me through building a simple program. It was enough to give me a flavor of the language, and to get me started if I want to experiment with it at some point (no time these days!). It's an absolutely breathtaking language. I am still skeptical about excessive reflection. It's clearly extremely powerful, and attractive in its conceptual simplicity. But I generally favor a careful balance between expressive power and local reasoning, and Smalltalk seems to tip awfully far towards the former. Nevertheless, I'd need to learn more and build real systems in Smalltalk before making judgments.
The way Avi designed Seaside leads to a beautiful style of web programming. Of course, there's the fact that the control flow is both compatible with the back button and window cloning and written in a natural style, thanks to continuations under the hood--but that's no surprise. It's in fact roughly the same approach as send/suspend/dispatch (though with the rather more friendly method name renderContentOn). But what I really enjoyed was the object-oriented approach to modeling the components of a web page.
In Squeak, essentially every component in the entire VM--numbers, blocks (closures), windows, stack frames, metaclasses, you name it--is represented as a Smalltalk object, with some particular set of supported methods and various ways to view it. The "system browser" provides a useful view: it introspects the object for its properties and their values, its methods and their source code, and any associated documentation, and displays them in an informative GUI window.
In Seaside, web pages can be seen as simply a different view on objects (that have special methods for rendering on the web, of course). When you change properties of a web component, its web view changes accordingly. Usually, these changes in state are triggered by user actions via the web: clicking links or submitting forms. If you change the property through the Squeak UI, then you can just reload the web page to see the changes. Most impressively, if you change the source code of a method on the object--say, the code that responds to a user action--there's no need to reload whatsoever! The next action simply invokes the method, which now happens to have a new implementation.
The way Avi designed Seaside leads to a beautiful style of web programming. Of course, there's the fact that the control flow is both compatible with the back button and window cloning and written in a natural style, thanks to continuations under the hood--but that's no surprise. It's in fact roughly the same approach as send/suspend/dispatch (though with the rather more friendly method name renderContentOn). But what I really enjoyed was the object-oriented approach to modeling the components of a web page.
In Squeak, essentially every component in the entire VM--numbers, blocks (closures), windows, stack frames, metaclasses, you name it--is represented as a Smalltalk object, with some particular set of supported methods and various ways to view it. The "system browser" provides a useful view: it introspects the object for its properties and their values, its methods and their source code, and any associated documentation, and displays them in an informative GUI window.
In Seaside, web pages can be seen as simply a different view on objects (that have special methods for rendering on the web, of course). When you change properties of a web component, its web view changes accordingly. Usually, these changes in state are triggered by user actions via the web: clicking links or submitting forms. If you change the property through the Squeak UI, then you can just reload the web page to see the changes. Most impressively, if you change the source code of a method on the object--say, the code that responds to a user action--there's no need to reload whatsoever! The next action simply invokes the method, which now happens to have a new implementation.
Exciting week!
I've had an exciting week in Amsterdam, attending XTech 2006 thanks to the generosity of Mozilla. On Thursday I visited Eelco Visser and Martin Bravenboer at the University of Utrecht. It was a fun and productive visit.
In the last couple of months I have started using Stratego/XT to model the semantics of ECMAScript. I believe that it's possible to scale the semantic frameworks that we use in research up to model whole, industry-sized programming languages. Now, these modeling frameworks are formal systems, just like programming languages themselves. So it should also be possible to express these models in a machine-executable form. There are several benefits to this approach:
Eelco and Martin liked my model--they found the CEKS machine representation of continuations lovely--and are glad to have an interesting application of Stratego. We talked about some of the things I could do better (and they already found a few subtle bugs in my implementation) as well as a couple of requests I had for Stratego. They're interested in what kinds of optimizations they could apply to their compiler that would provide the most benefit to applications like mine. For instance, since my abstract machine generally operates on only a few small forms that have fixed shapes, deforestation might be applicable.
Martin is now working on implementing the ECMAScript grammar, which is notoriously difficult to express in traditional parser generation frameworks. The module grammar formalism SDF, based on Tomita's generalized LR parsing algorithm and used in the Stratego/XT system, should actually allow us to define the syntax quite elegantly. This will allow us to parse actual ECMAScript programs, as well as to model eval realistically, since it relies on parsing strings as ECMAScript programs.
In the last couple of months I have started using Stratego/XT to model the semantics of ECMAScript. I believe that it's possible to scale the semantic frameworks that we use in research up to model whole, industry-sized programming languages. Now, these modeling frameworks are formal systems, just like programming languages themselves. So it should also be possible to express these models in a machine-executable form. There are several benefits to this approach:
- The added rigor that comes from the level of detail and precision required to get a machine to understand the model.
- The ability to test actual ECMAScript programs against the model.
- A reference implementation against which implementations can be tested.
- The eventual possibility of applying automated reasoning tools to the model (though not immediately!).
Eelco and Martin liked my model--they found the CEKS machine representation of continuations lovely--and are glad to have an interesting application of Stratego. We talked about some of the things I could do better (and they already found a few subtle bugs in my implementation) as well as a couple of requests I had for Stratego. They're interested in what kinds of optimizations they could apply to their compiler that would provide the most benefit to applications like mine. For instance, since my abstract machine generally operates on only a few small forms that have fixed shapes, deforestation might be applicable.
Martin is now working on implementing the ECMAScript grammar, which is notoriously difficult to express in traditional parser generation frameworks. The module grammar formalism SDF, based on Tomita's generalized LR parsing algorithm and used in the Stratego/XT system, should actually allow us to define the syntax quite elegantly. This will allow us to parse actual ECMAScript programs, as well as to model eval realistically, since it relies on parsing strings as ECMAScript programs.
Wednesday, May 17, 2006
Syntactic capital
When you step outside your familiar community, you learn interesting things about your assumptions. Something I've learned on the ECMA committee is that in Scheme, new syntax is "cheap," but not so in other languages.
Because syntax definition is in the hands of Scheme user programmers, we expect to see new syntactic forms all the time. As a result, implementing a feature as a syntactic form is uncontroversial in Scheme. In other languages, however, a new syntactic form signals (at least intuitively) a global change to the language. Users know that a new API is something they can put off learning until they feel they need it. But if there's a syntactic form in a language that you don't understand, you feel as though you don't have a handle on the language.
In terms of pragmatics, it's easier for language implementors to implement a subset of an API than it is to implement a subset of the syntax; you can at least guarantee that all programs will parse the same. What this really comes down to is scoped syntactic extensions, i.e., macros. If you can modularize syntactic forms, you can signal a parse error that says "I'm sorry, I don't support this syntactic form," which is the same as "I don't support this API."
In terms of cognitive load, modularizing syntactic forms allows users to learn subsets of a language in exactly the same way they learn subsets of libraries.
Because syntax definition is in the hands of Scheme user programmers, we expect to see new syntactic forms all the time. As a result, implementing a feature as a syntactic form is uncontroversial in Scheme. In other languages, however, a new syntactic form signals (at least intuitively) a global change to the language. Users know that a new API is something they can put off learning until they feel they need it. But if there's a syntactic form in a language that you don't understand, you feel as though you don't have a handle on the language.
In terms of pragmatics, it's easier for language implementors to implement a subset of an API than it is to implement a subset of the syntax; you can at least guarantee that all programs will parse the same. What this really comes down to is scoped syntactic extensions, i.e., macros. If you can modularize syntactic forms, you can signal a parse error that says "I'm sorry, I don't support this syntactic form," which is the same as "I don't support this API."
In terms of cognitive load, modularizing syntactic forms allows users to learn subsets of a language in exactly the same way they learn subsets of libraries.
Thursday, May 04, 2006
Friday, April 28, 2006
Jewels of the lambda calculus: scope
If abstraction is the grand prize-winning jewel of the lambda calculus, then scope is the first runner-up. Mitch Wand teaches his graduate students that the scoping properties of a language are one of the Four Questions we ask in order to understand its semantics ("why is this language different from all other languages?").
Scope is the first static property of any programming language. Lexical scope gives us a static context in which to understand a fragment of a program. Within the following program:
The static aspects of a program are what communicate its properties to the reader, allowing the reader to understand its behavior logically, as opposed to experimentally. Scope is the property that communicates the relationships between fragments of a program, whether through arguments, module imports, or class hierarchies. Scope is the static assignment of responsibility to these units of the program for communicating dynamic information.
Scope is the first static property of any programming language. Lexical scope gives us a static context in which to understand a fragment of a program. Within the following program:
λy.λx.ywe can look at the inner portion, λx.y, and in order to understand what portion of the program gives meaning to its body, we must understand that y is bound to--i.e., will receive its runtime meaning from--the static context of the fragment that binds it, i.e., the outer binding.
The static aspects of a program are what communicate its properties to the reader, allowing the reader to understand its behavior logically, as opposed to experimentally. Scope is the property that communicates the relationships between fragments of a program, whether through arguments, module imports, or class hierarchies. Scope is the static assignment of responsibility to these units of the program for communicating dynamic information.
Thursday, April 27, 2006
Jewels of the lambda calculus: abstraction as generalization
Since there are few things as likely to inspire in me a sense of religious reverence as the lambda calculus, I've decided to start a new series on some of the deep principles of computer science lurking in the lambda calculus.
Let's start with the crown jewel, abstraction:
Lambda abstractions represent the generalization of repeated patterns by parameterizing over their differences. If you perform several computations that are similar but not identical:
Let's start with the crown jewel, abstraction:
λx.eThis simple form represents the first rule of programming. Ruby hackers call it the "don't repeat yourself" rule. Perl hackers call it laziness: good programmers avoid repetitive, manual tasks. No matter the size, shape, or form, any time you write a program, you create an abstraction, a piece of code that automates a common task that otherwise would have to be repeated by a human.
Lambda abstractions represent the generalization of repeated patterns by parameterizing over their differences. If you perform several computations that are similar but not identical:
(9/5 × 23 + 32)then each one of these computations is a special case of a more generalized procedure. The abstraction of the three is represented by parameterizing over the portion where they differ:
(9/5 × 40 + 32)
(9/5 × 13 + 32)
λc.(9/5 × c + 32)From functions to abstract classes to Microsoft Office macros to parametric polymorphism, every form of abstraction is at its heart this same phenomenon.
Thursday, April 13, 2006
Stratego is cool
I've been meaning to talk about this for a while. Stratego is a very cool language. Their raison d'être seems to be performing program transformations, such as compilers and program optimizations. But because it's a term rewriting system, it's also perfectly reasonable to use it as a framework for specifying operational semantics of programming languages.
Here's an example rewrite rule, specifying the evaluation of variable references in a CEKS machine:
Stratego is based in part on SDF, the Syntax Definition Formalism, which is a lovely system for defining modular grammars. SDF is based on Tomita's Generalized LR (GLR) parsing algorithm, which recognizes the full class of context-free grammars, even ambiguous ones. If you want extensible grammars, you have to work with a class of grammars that's closed under composition, so they've chosen the most permissive, the full CFG class. Unfortunately this means you can end up with ambiguities, but as far as I know I haven't run into any sneaky ambiguities yet.
The other important feature of Stratego is its computational meta-language. My two requirements for a term rewriting system were the ability to specify rewrite rules in terms of the concrete language, which Stratego provides with flying colors, and the ability to compute side conditions. Stratego's entire computational model is based on rewriting, so side conditions work by saving the current state of the world and performing a rewrite on the side. Their rewriting combinators, known as strategies, allow for some pretty powerful abstractions. It has the feel of programming in the backtracking monad, not unlike Prolog. It's a little unfamiliar for a functional programmer, but it's perfectly adequate for the job.
It is my hope, and I'm optimistic, that we'll use Stratego to model the whole of the ECMAScript Edition 4 semantics. It's not on the same level as modeling the language in a theorem prover and using it to prove safety properties of the language mechanically, but my experience so far has shown that just having an executable model of a language is extremely useful for testing and driving out bugs in the semantics.
Here's an example rewrite rule, specifying the evaluation of variable references in a CEKS machine:
Unless you know Stratego, you won't realize the most remarkable thing about this code: it's using a custom syntax for the representation of the configurations in the CEKS machine! That is, I've extended the syntax of Stratego with a concrete syntax for configurations, bracketed between |[ and ]| tokens. I've also added unquotation to that concrete syntax in the form of $ tokens followed by Stratego terms. This allows me to bind meta-variables within the left-hand side of the rewrite rule and the where clauses and refer to bound meta-variables within the right-hand side of the rewrite rule and again in the where clauses.EvalVar :
|[
Expr: $e,
Env: $r,
Cont: $k,
Store: $s
]|
→
|[
Value: $v,
Cont: $k,
Store: $s
]|
where <is-var> e
; x := <var-name> e
; v := <resolve>(x,r)
Stratego is based in part on SDF, the Syntax Definition Formalism, which is a lovely system for defining modular grammars. SDF is based on Tomita's Generalized LR (GLR) parsing algorithm, which recognizes the full class of context-free grammars, even ambiguous ones. If you want extensible grammars, you have to work with a class of grammars that's closed under composition, so they've chosen the most permissive, the full CFG class. Unfortunately this means you can end up with ambiguities, but as far as I know I haven't run into any sneaky ambiguities yet.
The other important feature of Stratego is its computational meta-language. My two requirements for a term rewriting system were the ability to specify rewrite rules in terms of the concrete language, which Stratego provides with flying colors, and the ability to compute side conditions. Stratego's entire computational model is based on rewriting, so side conditions work by saving the current state of the world and performing a rewrite on the side. Their rewriting combinators, known as strategies, allow for some pretty powerful abstractions. It has the feel of programming in the backtracking monad, not unlike Prolog. It's a little unfamiliar for a functional programmer, but it's perfectly adequate for the job.
It is my hope, and I'm optimistic, that we'll use Stratego to model the whole of the ECMAScript Edition 4 semantics. It's not on the same level as modeling the language in a theorem prover and using it to prove safety properties of the language mechanically, but my experience so far has shown that just having an executable model of a language is extremely useful for testing and driving out bugs in the semantics.
Tuesday, April 04, 2006
Huzzah!
I finally have a working DSL connection at home! Now I can submit those few cherished hours of daily rest to the will of the Great Lord Productivity.
On a related note: in the year 2006, setting up DSL shouldn't take a week of phone tag, a dozen tech support reps, and an entire day wasted on troubleshooting (after the technician finishes repairing the line). I think my favorite moment was when the precious phone rep announced "I've figured out what the problem is! You're not actually using Internet Explorer, you're using a web browser with a bug that it doesn't display web pages." Thanks, Sherlock.
On a related note: in the year 2006, setting up DSL shouldn't take a week of phone tag, a dozen tech support reps, and an entire day wasted on troubleshooting (after the technician finishes repairing the line). I think my favorite moment was when the precious phone rep announced "I've figured out what the problem is! You're not actually using Internet Explorer, you're using a web browser with a bug that it doesn't display web pages." Thanks, Sherlock.
Tuesday, March 28, 2006
How do you say "maybe"?
- Haskell, ML: Maybe T, T option
- Scheme: either T or #f
- Java, C#: either an ordinary T or null
- ML, Scheme, Java, C#: either a value or an exception
- Prolog: success or failure
Monday, March 27, 2006
C rots the brain
It's high time for a good rant. I'll warm up by quoting Cassandra:
Consider the pure lambda calculus. Application of a β-redex completely replaces the application node with the body of the function being applied. That is, there is never any space consumed in the representation of control for a procedure application. Rather, it is when one of these applications occurs in the context of some other computation that the program's control consumes space. To quote Guy Steele:
The pernicious legacy of C is that we assume entry to a procedure body must always create a stack frame. But what is this frame for? It keeps a finger on our current point in the program, i.e., the program counter, and perhaps it stores some local data that we'll need in order to complete the evaluation of the function. If the procedure happens to be a leaf procedure, i.e., does not make any function calls, there's no need to save the current position, since we're not going anywhere else. Or maybe the procedure only conditionally calls another procedure. In that case, we might not need a continuation frame until we jump to the particular branch that is guaranteed to make the procedure call.
The assumption that procedure calls must push stack is so built-in to my head that I constantly have to remind myself: procedure entry and continuation frame allocation are not necessarily correlated!
But now the true folly is in the representation of the continuation as a simple stack. Gone are the days where we were told "if you want a string, just allocate a fixed buffer that's really, really big and hope you never need any more than that." (Well, gone should be the days.) Why then do we only get a fixed buffer size for the single most important part of every single program, the program's control itself? It's absurd to have your program tell you, "other than, like, those couple of gigabytes sitting over there, I'm totally out of space."
Why do these silly limitations persist? Because C rots the brain.
Update: Sam doesn't think it's fair for me to blame C. I guess C has been the drug that led to my personal brain damage, but it's perfectly possible for programmers of older generations to have been addled by Algol or Fortran, or newer generations by Java or C#. There's plenty of blame to go around...
I'm sorry to be politically incorrect, but for the ACM to then laud "C" andOne of our nastiest inheritances from C is a set of ingrained assumptions about the implementation of the control of any programming language.
its inventors as a major advance in computer science has to rank right up
there with Chamberlain's appeasement of Hitler.
Consider the pure lambda calculus. Application of a β-redex completely replaces the application node with the body of the function being applied. That is, there is never any space consumed in the representation of control for a procedure application. Rather, it is when one of these applications occurs in the context of some other computation that the program's control consumes space. To quote Guy Steele:
Intuitively, function calls do not "push control stack"; instead, it is argument evaluation which pushes control stack.A continuation frame represents a kind of to-do list of what the program has left to do. It only needs to save this information in memory somewhere if it's going to do something else first, i.e., call another procedure.
The pernicious legacy of C is that we assume entry to a procedure body must always create a stack frame. But what is this frame for? It keeps a finger on our current point in the program, i.e., the program counter, and perhaps it stores some local data that we'll need in order to complete the evaluation of the function. If the procedure happens to be a leaf procedure, i.e., does not make any function calls, there's no need to save the current position, since we're not going anywhere else. Or maybe the procedure only conditionally calls another procedure. In that case, we might not need a continuation frame until we jump to the particular branch that is guaranteed to make the procedure call.
The assumption that procedure calls must push stack is so built-in to my head that I constantly have to remind myself: procedure entry and continuation frame allocation are not necessarily correlated!
But now the true folly is in the representation of the continuation as a simple stack. Gone are the days where we were told "if you want a string, just allocate a fixed buffer that's really, really big and hope you never need any more than that." (Well, gone should be the days.) Why then do we only get a fixed buffer size for the single most important part of every single program, the program's control itself? It's absurd to have your program tell you, "other than, like, those couple of gigabytes sitting over there, I'm totally out of space."
Why do these silly limitations persist? Because C rots the brain.
Update: Sam doesn't think it's fair for me to blame C. I guess C has been the drug that led to my personal brain damage, but it's perfectly possible for programmers of older generations to have been addled by Algol or Fortran, or newer generations by Java or C#. There's plenty of blame to go around...
Sunday, March 19, 2006
Why the CPS simulation of CBV works
Incidentally, it's exactly the common element of call-by-name and call-by-value I mentioned a moment ago that facilitates the CPS simulation of call-by-value in call-by-name. Both reduction rules require that the operator of a redex be a value. In either calculus, reduction relies on instantiating a bound variable within the body of a function; there's no obvious way you could know how to reduce if you don't actually know what the operator is. So both systems force evaluation of an operator in order to evaluate an application. The difference is whether you also force the operand.
The CPS transform just makes it so that all evaluation within an entire program occurs exclusively in operator positions. After the translation, all operands are values and therefore irreducible. This property is also preserved under reduction, so at every step, a CPS'ed program behaves the same in either calculus.
In other words, if every operand is always a value, there's no difference between the β-rule and the βv rule.
The CPS transform just makes it so that all evaluation within an entire program occurs exclusively in operator positions. After the translation, all operands are values and therefore irreducible. This property is also preserved under reduction, so at every step, a CPS'ed program behaves the same in either calculus.
In other words, if every operand is always a value, there's no difference between the β-rule and the βv rule.
Observable differences between reduction strategies
It's easy to misunderstand the difference between lazy and eager evaluation. You might be tempted to think that 1) lazy evaluation does reductions from the "outside in," meaning that finds the outermost redex and reduces it before reducing its subterms, and 2) eager evaluation, by contrast, reduces from the "inside out," not performing an outer reduction until it has reduced all its subterms.
But this isn't the case. The difference between lazy and eager evaluation is not a difference in evaluation strategy, but rather a difference in the definition of what is reducible. In ordinary evaluation (as opposed to, say, compiler optimizations using partial evaluation), we always use the exact same strategy when reducing terms--typically, always reduce the leftmost, outermost redex. The difference is in the definition of redexes.
In call-by-name lambda calculus, the definition of a reducible expression is an application whose operator is a value. The operand can be any arbitrary expression. As a result, non-values end up being passed as arguments to functions. In call-by-value, we likewise only perform reduction when the operator is a value, but we also require that the operand be a value as well.
The combination of an outermost reduction strategy with the call-by-value rule may appear to be the same as an innermost reduction strategy; after all, it forces the evaluation of subterms before reducing a compound term. But it doesn't force the evaluation of all subterms, specifically, underneath abstractions. This is the key distinction.
Here's an example that distinguishes the three semantics. Imagine an untyped lambda calculus with two effects: we can ask Alice a question, say by sending her computer a message over the network and receiving a response, or we can similarly ask Bob a question. Each of these operations results in a distinct observable effect. Now take the following simple program:
In call-by-name lambda calculus with a leftmost-outermost reduction strategy:
I added a couple simple effects to the lambda calculus to demonstrate the idea. But in pure lambda calculus, we can still observe differences between these systems because we can demonstrate side effects through non-termination. An expression that leads to non-termination results in different evaluation behavior of a system when the system makes different decisions about when and whether to evaluate the expression.
But this isn't the case. The difference between lazy and eager evaluation is not a difference in evaluation strategy, but rather a difference in the definition of what is reducible. In ordinary evaluation (as opposed to, say, compiler optimizations using partial evaluation), we always use the exact same strategy when reducing terms--typically, always reduce the leftmost, outermost redex. The difference is in the definition of redexes.
In call-by-name lambda calculus, the definition of a reducible expression is an application whose operator is a value. The operand can be any arbitrary expression. As a result, non-values end up being passed as arguments to functions. In call-by-value, we likewise only perform reduction when the operator is a value, but we also require that the operand be a value as well.
The combination of an outermost reduction strategy with the call-by-value rule may appear to be the same as an innermost reduction strategy; after all, it forces the evaluation of subterms before reducing a compound term. But it doesn't force the evaluation of all subterms, specifically, underneath abstractions. This is the key distinction.
Here's an example that distinguishes the three semantics. Imagine an untyped lambda calculus with two effects: we can ask Alice a question, say by sending her computer a message over the network and receiving a response, or we can similarly ask Bob a question. Each of these operations results in a distinct observable effect. Now take the following simple program:
(λx.(ask bob)) (ask alice)In call-by-name lambda calculus with a leftmost-outermost reduction strategy:
(λx.(ask bob)) (ask alice)
-> (ask bob)
b! -> 22 (λx.(ask bob)) (ask alice)
a! -> (λx.(ask bob)) 11
-> (ask bob)
b! -> 22 (λx.(ask bob)) (ask alice)
b! -> (λx.22) (ask alice)
a! -> (λx.22) 44
-> 22I added a couple simple effects to the lambda calculus to demonstrate the idea. But in pure lambda calculus, we can still observe differences between these systems because we can demonstrate side effects through non-termination. An expression that leads to non-termination results in different evaluation behavior of a system when the system makes different decisions about when and whether to evaluate the expression.
Tuesday, March 14, 2006
Proper tail recursion and space efficiency
I just read through Will Clinger's Proper Tail Recursion and Space Efficiency. I'd been scared of it for a few years because I had the impression it was a very technical and subtle paper. There are perhaps a few subtleties but I actually found it very clear and well-written. Here are some interesting points made in the paper:
1. Proper tail recursion is a property of the asymptotic space complexity of a language's runtime behavior. That is, in improperly tail recursive languages, control can consume unbounded amounts of space for programs that, when run in properly tail recursive languages, only require a constant amount of space.
2. In order to measure the space complexity of a language, you have to measure the entire system, not just, say, the stack. Otherwise, someone could always cheat and hide away its representation of the stack in the heap to make it look like the control is more space-efficient than it really is.
3. But when you measure everything including the heap, you have to deal with the fact that the language doesn't ever explicitly deallocate storage. This means that you have to add garbage collection into your model or else the model always increases its space usage unrealistically.
4. Proper tail recursion is totally natural in the lambda calculus. An application is always replaced by the body of the applied function, regardless of whether it's a tail call. It's just languages with that freaky return construct that accidentally make the mistake of leaving around residue of the application expression until it's completed evaluating. In order to model improper tail calls in Scheme, Will actually has to add a silly return context frame, whose sole purpose is to degrade the space efficiency of the language.
5. By leaving the expression language the same but changing the definition of the runtime system (in this case, the set of context frames), you can compare apples to apples and look at the same space consumption of the exact same program in one system or another, assuming the systems always produce the same results from the programs. Then we can actually construct space complexity classes to classify the different systems.
1. Proper tail recursion is a property of the asymptotic space complexity of a language's runtime behavior. That is, in improperly tail recursive languages, control can consume unbounded amounts of space for programs that, when run in properly tail recursive languages, only require a constant amount of space.
2. In order to measure the space complexity of a language, you have to measure the entire system, not just, say, the stack. Otherwise, someone could always cheat and hide away its representation of the stack in the heap to make it look like the control is more space-efficient than it really is.
3. But when you measure everything including the heap, you have to deal with the fact that the language doesn't ever explicitly deallocate storage. This means that you have to add garbage collection into your model or else the model always increases its space usage unrealistically.
4. Proper tail recursion is totally natural in the lambda calculus. An application is always replaced by the body of the applied function, regardless of whether it's a tail call. It's just languages with that freaky return construct that accidentally make the mistake of leaving around residue of the application expression until it's completed evaluating. In order to model improper tail calls in Scheme, Will actually has to add a silly return context frame, whose sole purpose is to degrade the space efficiency of the language.
5. By leaving the expression language the same but changing the definition of the runtime system (in this case, the set of context frames), you can compare apples to apples and look at the same space consumption of the exact same program in one system or another, assuming the systems always produce the same results from the programs. Then we can actually construct space complexity classes to classify the different systems.
Friday, March 10, 2006
The Rule of Least Power
Via Phil Wadler's blog, I see that Tim Berners-Lee has written a "W3C Finding" on a principle he terms the rule of least power. The idea is that you should use the least powerful language possible to solve any given problem, in order to achieve the greatest ability to reason about the program statically.
I've talked about this principle before as the balance of expressive power with reasoning power.
In working on the ECMAScript design, I've already seen this issue come up several times, for example with the problems caused by dynamic scoping.
I've talked about this principle before as the balance of expressive power with reasoning power.
In working on the ECMAScript design, I've already seen this issue come up several times, for example with the problems caused by dynamic scoping.
Mom was right...
...hygiene really is important!
It took me hours the other day to catch a bug that came from an unintended variable capture in a macro I'd written.
In a reduction semantics I'm implementing with PLT Redex, I wrote a macro to abstract over certain common patterns in my reduction rules. The macro template introduced a temporary name via a call to the name macro in PLT Redex. I thought name was implemented with a Scheme binding and would therefore be hygienically renamed. This was my mistaken assumption; name is implemented with a quoted symbol.
Then later in a reduction rule, I was using my macro and by chance introducing another variable at the call site with the same name as the temporary variable in the macro definition. This silently caused a capture of the quoted name, with unexpected consequences on the meaning of the reduction rule. In this particular case, it cause the reduction rule not to match when it should.
It took hours to discover that it wasn't a bug in my reduction rule at all, but in the implementation of my macro. Imagine trying to debug this if I hadn't just spent years studying macros and hygiene!
It took me hours the other day to catch a bug that came from an unintended variable capture in a macro I'd written.
In a reduction semantics I'm implementing with PLT Redex, I wrote a macro to abstract over certain common patterns in my reduction rules. The macro template introduced a temporary name via a call to the name macro in PLT Redex. I thought name was implemented with a Scheme binding and would therefore be hygienically renamed. This was my mistaken assumption; name is implemented with a quoted symbol.
Then later in a reduction rule, I was using my macro and by chance introducing another variable at the call site with the same name as the temporary variable in the macro definition. This silently caused a capture of the quoted name, with unexpected consequences on the meaning of the reduction rule. In this particular case, it cause the reduction rule not to match when it should.
It took hours to discover that it wasn't a bug in my reduction rule at all, but in the implementation of my macro. Imagine trying to debug this if I hadn't just spent years studying macros and hygiene!
Monday, March 06, 2006
Redex is cool
I hadn't looked at PLT Redex since its pre-publication days, but yesterday I started using it to implement my draft model for Topsl, the programming language for implementing online surveys. I couldn't believe how easy it was! I expected it to take quite a while, but within an hour I had a working operational model of core Scheme, and half an hour later I had the entire grammar of Topsl and even a few nice abstractions. I haven't quite finished the implementation yet, but it's been surprisingly painless.
Of course, it helps to have a good understanding of macrological* pattern-matching and template instantiation, capture-avoiding substitution, and Felleisen-style context-sensitive reduction semantics, so you might say I'm uniquely suited to use the tool. Regardless, I'm very impressed.
* This is a very silly adjective. Please don't ever use it. Someone could get hurt.
Of course, it helps to have a good understanding of macrological* pattern-matching and template instantiation, capture-avoiding substitution, and Felleisen-style context-sensitive reduction semantics, so you might say I'm uniquely suited to use the tool. Regardless, I'm very impressed.
* This is a very silly adjective. Please don't ever use it. Someone could get hurt.
Wednesday, March 01, 2006
The call stack is not a history
I had a fascinating conversation with John Clements yesterday about continuation marks, and he gave me a nice way of clarifying a common misconception about the call stack. There are two major pieces of information you might like to inspect about the control flow of a program: what the program has already done (its history), and what it has left to do (its future).
The call stack might appear to be giving you information about the history of the program execution, but in fact, it's an incomplete history. For example, any functions that have already returned are not recorded; they've already popped off the stack. Languages that implement proper tail calls also remove information about function calls that have completed just about everything but may not yet have returned from their tail operations. Now, if this is information you need, it doesn't mean you can't record it through some other means. It just means the default behavior of the runtime is not to record it--and for good reason, too. Not accumulating that information affects the asymptotic space complexity of the runtime. You wouldn't want your runtime collecting complete information about every iteration of a for-loop by default, either, just on the off-chance that information might be useful!
The evaluation context, i.e. call stack, is not about the history of the program execution. It contains a complete record of the remainder of the program execution, the work the program has left to do. That's the whole reason for maintaining stack frames, so that when a function returns, the runtime knows what to do next. So stack inspection is fundamentally about inspecting the future of the computation, not about recording its history.
The call stack might appear to be giving you information about the history of the program execution, but in fact, it's an incomplete history. For example, any functions that have already returned are not recorded; they've already popped off the stack. Languages that implement proper tail calls also remove information about function calls that have completed just about everything but may not yet have returned from their tail operations. Now, if this is information you need, it doesn't mean you can't record it through some other means. It just means the default behavior of the runtime is not to record it--and for good reason, too. Not accumulating that information affects the asymptotic space complexity of the runtime. You wouldn't want your runtime collecting complete information about every iteration of a for-loop by default, either, just on the off-chance that information might be useful!
The evaluation context, i.e. call stack, is not about the history of the program execution. It contains a complete record of the remainder of the program execution, the work the program has left to do. That's the whole reason for maintaining stack frames, so that when a function returns, the runtime knows what to do next. So stack inspection is fundamentally about inspecting the future of the computation, not about recording its history.
Sunday, February 26, 2006
From the that'll-be-the-day department
On the plt-scheme mailing list, Matthew announces that PLT Scheme now builds on the new macs. Now who ever expected to see statements like the following in this lifetime?
MzScheme passes its test suite. I don't know whether MrEd and DrScheme
actually work, because I've only had console access to an Intel Mac.
Thursday, February 23, 2006
Nancy typing
It's popular in scripting languages to perform lots of automatic conversions on data in an attempt to "do what I mean". In some cases, the heuristics for conversion are arguably relatively clear, but sometimes the language is so eager to find some way to make the operation consistent rather than simply give an error (and force the programmer to be more explicit) that extremely bizarre and unpredictable behavior ensues.
I call this Nancy typing, for a delicious reason that will soon become clear. What this has to do with duck typing, I'm not sure--I can't find a straight-forward definition. According to Wikipedia's rather confused entry it's not the same thing as structural types, but the jury seems to be out in this LtU thread. As far as I can tell, duck typing either has something to do with the idea of performing conversions between separate datatypes in order to support an operation or simply subtyping based on the set of supported operations. Actually, in the TAPL chapter on structural types, Pierce points out that structural type systems often include axioms that assert subtyping relationships between types whose runtime representations are completely different (such as float and int, for example), and these coercions actually have to be implemented in the runtime by conversions. So maybe the distinction is artificial, and duck typing really is the same thing as structural subtyping.
Anyway, the typical example used to demonstrate the hazards of structural subtyping is a GraphicalObject class and Cowboy class that both implement draw operations with entirely different meanings. But I prefer the Nancy bug.
My friend Mike MacHenry told me this story. Mike's company has an expert system, written in Perl, that employs heuristics to determine whether a customer is likely to have filled out a form incorrectly. One of the heuristics is supposed to check that the names given in two different columns of a record are the same. Now, it turns out that the comparison was implemented wrong--the software was almost always reporting that the names were the same, even when they weren't--but because the expert system is only making a best guess, this just passed unnoticed for a while as a false negative.
But every once in a while, the system reported a false positive, i.e., that the names were not the same when in fact they were. And it just so happened that in each one of these cases, the name in the record was "Nancy."
The explanation is that the programmer had accidentally used the numeric equality operation, rather than string equality. Perl silently converted the strings to numbers in order to make the operation succeed. Since in most of the cases, the strings were not numeric, Perl parsed the maximum numeric prefix of the string, namely the empty string. It so happens that the empty string happily converts to 0 in Perl, so most of the time, any pair of strings both convert to 0, and the equality comparison evaluates to true.
But "Nan" is parseable in Perl as not-a-number, which is always considered unequal to any number, including itself. So "Nancy" happily converts to not-a-number, and then tests false for numeric equality to itself.
Tada! The Nancy bug.
Update:
I call this Nancy typing, for a delicious reason that will soon become clear. What this has to do with duck typing, I'm not sure--I can't find a straight-forward definition. According to Wikipedia's rather confused entry it's not the same thing as structural types, but the jury seems to be out in this LtU thread. As far as I can tell, duck typing either has something to do with the idea of performing conversions between separate datatypes in order to support an operation or simply subtyping based on the set of supported operations. Actually, in the TAPL chapter on structural types, Pierce points out that structural type systems often include axioms that assert subtyping relationships between types whose runtime representations are completely different (such as float and int, for example), and these coercions actually have to be implemented in the runtime by conversions. So maybe the distinction is artificial, and duck typing really is the same thing as structural subtyping.
Anyway, the typical example used to demonstrate the hazards of structural subtyping is a GraphicalObject class and Cowboy class that both implement draw operations with entirely different meanings. But I prefer the Nancy bug.
My friend Mike MacHenry told me this story. Mike's company has an expert system, written in Perl, that employs heuristics to determine whether a customer is likely to have filled out a form incorrectly. One of the heuristics is supposed to check that the names given in two different columns of a record are the same. Now, it turns out that the comparison was implemented wrong--the software was almost always reporting that the names were the same, even when they weren't--but because the expert system is only making a best guess, this just passed unnoticed for a while as a false negative.
But every once in a while, the system reported a false positive, i.e., that the names were not the same when in fact they were. And it just so happened that in each one of these cases, the name in the record was "Nancy."
The explanation is that the programmer had accidentally used the numeric equality operation, rather than string equality. Perl silently converted the strings to numbers in order to make the operation succeed. Since in most of the cases, the strings were not numeric, Perl parsed the maximum numeric prefix of the string, namely the empty string. It so happens that the empty string happily converts to 0 in Perl, so most of the time, any pair of strings both convert to 0, and the equality comparison evaluates to true.
But "Nan" is parseable in Perl as not-a-number, which is always considered unequal to any number, including itself. So "Nancy" happily converts to not-a-number, and then tests false for numeric equality to itself.
Tada! The Nancy bug.
Update:
Subscribe to:
Posts (Atom)
