Too much recursion

Press this to see how even the high-level scripting languages in the mainstream prevent programmers from using recursion.

Different Javascript engines will give you different error messages, but the Mozilla one is the most offensive: "too much recursion." Groan.

Update: I've modified the Javascript so it should work in Safari, too. But I'm not going to spend more time making a broken script work in multiple browsers.

(TMTOWTDI)

And you thought there was more than one way to do it in Perl. Yeesh.

Point for The Economist

I was one of several people who wrote to The Economist correcting their Latin grammar, and it looks like the last laugh was on us--not only were we geeky enough to waste our time on this nonsense, but none of us completely agreed on the correct version. Hah! Well done.

And I don't think my suggestion was quite right. I chose the neuter plural form plura for "many," but plures would probably have been better. I think the neuter is only for things, whereas the masculine is used for people even when the gender is unknown.

Oh well. At least I got to make an idiot of myself in front of millions of readers worldwide.

Update: After conferring with Richard, we decided that a) the neuter plural was OK, since the original slogan uses the neuter, and b) I should've used ex instead of e, since it appears before a word beginning with a vowel. But this also means not one of the suggestions was right! Stupid Latin.

DHTML resources

Here's a preliminary a collection of resources on Javascript and DHTML with at least some halfway informative content. I'd be happy to receive more suggestions!

Tips, tricks, and best practices

• http://www.ditchnet.org/wp/?p=2
• http://www.crockford.com/javascript/inheritance.html
• http://www.webreference.com/js/column79/
• http://www.webreference.com/js/column80/

General information

• http://ditchnet.org/wp/
• http://www.crockford.com/javascript/
• http://www.onlinetools.org/articles/unobtrusivejavascript/

Libraries

• http://www.brainjacked.com/
• http://jsolait.net/
• http://prototype.conio.net/
• http://dojotoolkit.com/
• http://www.walterzorn.com/dragdrop/api_e.htm
• http://www.whitefrost.com/servlet/connector?file=reference/2003/06/17/libXmlRequest.html
• http://sarissa.sourceforge.net/

Demos

• http://trimpath.com/project/wiki/TrimSpreadsheet
• http://www.activewidgets.com/
• http://ditchnet.org/dhtmlgallery/jsdock.html
• http://ditchnet.org/google/example.html

Javascript surprises

Javascript is not a wholly unpleasant language to work in, but it has its share of surprises.

Lexical scope: Functions are first-class values, and variables declared within the var keyword are sort of lexically scoped with respect to the nesting of functions. However, despite the C-like syntax, there is no block-style scoping. This means that you can write strange-looking functions like

function f(b) {
    if (b) {
        var x = 3;
    }
    alert(x);
}

I think the meaning of this function is that the lexical scope of x is lifted to the entire function body, but if the if-branch isn't taken, x has the default undefined value. This means that in the following example:

var x = 2;
 
function g(b) {
    if (b) {
        var x = 3;
    }
    alert(x);
}

the variable x is always shadowed in the body of g, so that it displays either 3 or undefined, and never 2.

Furthermore, you can assign to variables that have not been declared with var, which is subtly necessary because of the dynamic scope of this (see below). Basically, if you assign to a variable that hasn't been declared lexically with var, the language first searches the dynamically scoped this object for a member of that name, and then up the prototype chain. Somewhat unfortunately, if it doesn't find any member of the given name, it silently generates a new global variable of that name and performs the assignment.

this is everywhere: There is always a special this variable available, but its binding is dynamically scoped. The upshot is that you can create an ordinary function that refers to this in its body, and then later assign that function as a member of an object, and the this automatically gets wired to the new container.

Bizarrely, there is a special "global" object, so that if such a function is not a member of any object, this refers to that special object; even more bizarre is that particular Javascript engines seem to be free to make that global object whatever they want. In DHTML engines it's some kind of window object or something, whereas in Rhino it might be something else (this is hearsay--I haven't tried it). Furthermore, all global variables are actually member variables of this global object.

It gets even weirder: this means that global function declarations of the form

function foo() { ... }

are really just syntactic sugar for

foo = function() { ... };

which is a declaration of a global variable, i.e., a member variable of the global object, whose value is a function. It's truly strange, but it has a sort of internal consistency, and you kind of have to admire their chutzpah.

Object system: Javascript is the only prototype-based OO language I've ever worked with, so this was all new to me. To start with, objects are essentially just associative arrays, i.e., tables mapping names to values, much like Python or Lua. But every object is also linked to a "prototype" object, and name resolution searches the chain of prototype references. This is quite different from class-based inheritance, but it does provide a kind of dynamic dispatch, so it serves similar purposes. (It can also be used to simulate class-based inheritance.) The prototype of an object is exposed via its prototype member variable, which is mutable like everything else in Javascript.

Rather than being defined in classes, constructors in Javascript are simply functions that, when called with the new operator, have their new object implicitly available via this. By convention, people usually capitalize the name of constructor functions, which makes it look like Java-style, class-based object creation. But that "class name" is in fact just an ordinary Javascript function.

for ... in: In addition to the ordinary integer-indexed for loops, Javascript has a for ... in syntax. But it's not at all what you'd expect! This special form is only used to range over the keys (i.e., member names) in an object. It has nothing to do with iterating over collections. Specifically, if you use this to try to use this form on an array, you end up iterating over all the names of the member variables of the array object (which includes the elements of the array, because they are also member variables, whose names are integers! wow). That one took some head-scratching the first time I encountered it.

Extension by mutation: It seems an industry standard form of "extension" is to mutate the prototype of an object. Lord help you if you accidentally overwrite an existing method. What, me, namespaces?

IE has "alien" types: All right, this isn't Javascript's fault. But it's annoying. In IE, the elements of the core DOM are not actually derived from the standard Object prototype, and their prototypes are not even visible. So there's no way to extend the behavior of the core DOM prototypes.

There and back again

From There and Back Again by Danvy and Goldberg (via Lambda the Ultimate):

Computing a Symbolic Convolution

Given two lists [x₁,x₂,...,x_n-1,x_n] and [y₁,y₂,...,y_n-1,y_n], where n is not known in advance, write a function that constructs

[(x₁,y_n),(x₂,y_n-1),...,(x_n-1,y₂),(x_n,y₁)]

in n recursive calls and with no auxiliary list.

Their direct style solution uses a generalization convolve' that produces the convolution of two lists where the first list may be shorter than the second, as well as the extra prefix of the second list. I've written it here in pseudo-Haskell with dependent type annotations representing the lengths of the lists:

convolve' :: [a]m → [b]n → ([(a,b)]m, [b]n-m)   -- n ≥ m
convolve' [] ys = ([], ys)
convolve' (x:xs) ys =
   let (r, (y:ys')) = convolve' xs ys in
     ((x,y):r, ys')

convolve :: [a]n → [b]n → [(a,b)]n
convolve xs ys = r where (r, []) = convolve' xs ys

What it's doing is recurring down the first list until it hits the end and then pairing up the elements as it returns; whatever elements are leftover from the beginning of the second list get placed in the second "return register."

The other solution uses a similar generalization, but in CPS:

convolve' :: [a]m → [b]n → ([(a,b)]m → [b]n-m → c) → c   -- n ≥ m
convolve' [] ys k = k [] ys
convolve' (x:xs) ys k =
   convolve' xs ys (λr (y:ys') . k ((x,y):r) ys')

convolve :: [a]n → [b]n → [(a,b)]n
convolve xs ys = convolve' xs ys (λr [] . r)

Same thing, really. The interesting part isn't the direct style vs. CPS, but rather the discovery of the invariant, i.e., the generalization of the problem. Once we know to write a function that a) allows the first list to be shorter than the second, and b) produces both the partial solution and the remaining elements of the second list, the rest is actually not so challenging.

Update: No, no, no... I described the purpose of convolve' wrong. It produces a pair containing 1) the convolution of a given suffix of the original first list with the corresponding prefix of the second list, and 2) the remaining suffix of the second list.

AOP is...

[Look out: there is hand-waving! -ed.]

I was reading the background on Dylan's condition system, where the author describes exceptions as "situations that must be handled gracefully but that are not conceptually part of the normal operation of the program." Exceptions are a nice example of a linguistic abstraction that strictly increases the expressive power of a programming language. (Stated without proof, but we've all seen the exception monad.) And they introduce the possibility of non-local effects in code that can't in general be detected by local inspection.

AOP is often described as an answer to the problem of "modularizing cross-cutting concerns." Any time you have something that can't be expressed with the abstraction mechanisms of your given language, it ends up being scattered throughout the program in multiple modules. Well, it sounds like they're trying to take credit for all of linguistic abstraction. But nobody is going to come up with the once-and-for-all abstraction mechanism to eradicate all need for new linguistic abstractions.

On the somewhat less over-reaching side, AOP has popularized a set of (relatively) new linguistic abstractions to the lexicon, and they're useful ones. The few that stand out are before/after and around patterns and control flow inspection. These are useful linguistic abstractions, and as usual, they introduce expressive power at some cost of local reasoning.

I wouldn't be upset if history forgot AOP as a field per se and just kept the collection of useful programming mechanisms it's produced. Because the heady claim that AOP "modularizes cross-cutting concerns" is really just hype. Or at least, it doesn't distinguish AOP from any other linguistic abstraction; any language feature that modularizes scattered code--exceptions, for example--helps separate cross-cutting concerns.

Deep ideas lurking in Object-Oriented Style, part II

The other important Deep Idea in Object-Oriented Style is the connection between object-oriented programming and recursion. He's not the first to notice this by any stretch of the imagination. This was the central idea in Cook and Palsberg's denotational semantics of inheritance. But it's an important idea that isn't well-enough understood, especially since recursion is so poorly understood in the OOP community.

This is a truly beautiful example:

(define math-object
 (vector
   (lambda (this n)
     (if (zero? n) #t ((vector-ref this 1) this (sub1 n))))
   (lambda (this n)
     (if (zero? n) #f ((vector-ref this 0) this (sub1 n))))))
> ((vector-ref math-object 0) math-object 5)
#f

Not only are objects a generalization of recursive functions, but they could serve as a much more accessible explanation of the Y combinator and "tying the knot" than the usual approaches.

Deep ideas lurking in Object-Oriented Style, part I

Object-Oriented Style
Dan Friedman

A style such as CPS or what Dan describes as Object-Oriented Style, is roughly a design pattern begging for linguistic abstraction. He describes a tension between abstracting out the design pattern--which results in all the usual benefits of abstraction--and gaining a better understanding of the semantics of the style by writing it out explicitly.

This is a fundamental tension in language design. A linguistic abstraction that increases the expressive power of the language results in code that is more concise but that masks widespread (global) effects. One example he gives is the semantics of method calls: when is a method call static and when does it involve searching the inheritance chain? It's hard to tell when they just look like ordinary procedure invocation, but when you write the style explicitly, you can see how the method lookup is implemented.

Now, the expressiveness paper talks about true linguistic abstractions being those that aren't macro-expressible (albeit by a very specific definition of macro-expressibility), and Dan's paper implements the linguistic abstraction via macros. So this seems to muddy my point somewhat. But I think they still capture the spirit of global transformations, since they transform the entire class bodies.

(Interesting: I wonder if macro-defining macros allow you to make transformations that are not macro-expressible by Felleisen's formal definition.)

Curry-Howard, logically

I tend to think of the Curry-Howard correspondence from the point of view of types: I repeat the slogan "types are propositions about programs" in my head, and that helps me remember that the types correspond to logical propositions, and the programs correspond to proofs of those propositions.

But upon reading the introduction to Proofs and Types, I was reminded of the parallel point of view of proofs. If we think of proofs as mathematical objects, then we can give them natural representations: a proof of A ∧ B is representable as a pair of proofs of A and B, respectively; a proof of A ∨ B is represented as a discriminated union of either a proof of A or a proof of B; and most importantly, a proof of A ⇒ B is representable as a function that takes any proof of A and produces a proof of B.

Multi-stage web programming

Something languages like Links may want to keep in mind: there could be a great deal of benefit from taking a multi-stage approach. For the moment, let's make a simplifying (though utterly wrong) assumption that a web application lives in a single page. Then we can see three stages:

1. The "runtime" is the dynamic aspect of a page that can be scripted with Javascript.
2. Before that comes the page-generation logic that happens on the server side.
3. Preceding both these phases is the generation of the static content (the "quoted" part of an ASP or JSP page).

Interestingly, all three of these stages have elements in common--specifically, the DOM. A unifying approach within a multi-stage language could be very powerful. For example, simply quoting an expression in this hypothetical high-level web development language would cause the compiler to change its output from some dynamic Javascript that, say, sets the innerHTML property of a DOM node, to JSP code that generates the HTML on the server.

But now reconsider the above assumption. Real web applications involve multiple round trips, and Ajax is popularizing the further complication of allowing semi-secret (let's never forget the back button, though!) round trips to occur within hidden frames. How does this cycle between the server and client sides change the multi-stage architecture?

Mitch has a blog!

Check it out!

Argument order

For multiple-arity functions, it would be more abstract to pass arguments by label rather than order. Just like pattern matching is more abstract than using explicit selectors, passing in arguments by label allows you to pass arguments in any order, and would allow for a more general form of currying. It would also simplify partial evaluation, since you wouldn't have to rearrange a function's arguments to apply it to a subset of them.

Nevertheless, tuples are a lighter-weight data structure than records, and lighter-weight solutions are easier to write and often easier to read. Positional function arguments are here to stay.

Because the order of arguments isn't always particularly relevant, the order can seem arbitrary. As the designer of a procedure, it's sometimes hard to know what order to choose. Here's one criterion: think about currying. It can be useful to put the arguments expected to be known earlier before the arguments expected to be known later.

For example, in Syntactic Abstraction in Scheme, the heart of the definition of the macro expansion algorithm is the rule for macro applications:

expand(e, r) =
  case parse(e, r) of
    ...
    macro-application(i, e) → expand(mark(t(mark(e, m)), m), r)
      where t = r(resolve(i)) and m is fresh

This is pretty hard to read. Without getting too much into the specific details of the algorithm, the idea of this rule is that to expand a macro application, you mark the expression with a fresh mark, apply the macro transformer t to the marked expression, then mark the output of that transformer again with the same mark, and finally expand the result.

There's a functional pipeline buried in that rule, but it's obscured by the order of arguments. This is actually a good candidate for point-free style. Since we expect the environment argument r for expand to be known before the expression, and the mark argument m for mark to be known before the expression argument, let's swap the order of arguments to both those functions. Now we get the new rule

...
macro-application(i, e) → ((expand r) ⋅ (mark m) ⋅ t ⋅ (mark m)) e
...

Freshness... with respect

In A New Approach to Abstract Syntax with Variable Binding, Pitts and Gabbay describe a "freshness" quantifier for their variant of set theory, where you can quantify over fresh names. This allows you to describe freshness conditions in a more formal way than the usual "x does not occur in M," and even reason about fresh names with formal logic. The quantification N x can be read: "for fresh x ..." This has a cool, dual universal/existential property: because the ambient universe of names is infinite, it's always true that there exists a fresh x, and because we don't care which one we choose, any proposition we prove using the freshness quantifier holds for all such fresh names.

What confused me for a while was that the quantifier just says "x is fresh;" it doesn't say "x is fresh with respect to M". But it seemed like if you take a name that's fresh at one point, but then use it in another context, you might have accidentally picked a name that conflicted with a name in the new context. In other words, I was concerned that having a local freshness condition without talking globally about all the names you're ever going to use doesn't carry enough information to avoid an incorrect choice of fresh name.

You have to dig a little deeper to see why this isn't a problem. The real meaning of the quantifier comes from the idea that the universe of names is infinite, but the construction of any particular term only involves a finite number of names. So not only can you find a fresh name at any point; but you can in fact choose any name other than the ones used in that term. So all but finitely many names are fresh. This is the more precise interpretation of N x: "for all but finitely many names x ..."

So the freshness quantifier isn't actually committing to a name. It's just saying that there's a huge set of names for which the proposition holds. Thus moving in and out of scope of particular terms doesn't affect the truth of a proposition built with the quantifier, because while the particular set of fresh names might change, the fact that that set involves all but a finite number of names does not. This allows us to abstract away from the actual choice of fresh names in a program when we're writing propositions about them.

The lambda machine

If the lambda calculus is a minimalist assembly language for modeling computation, then we can look at a lambda program as a mathematical black box with two possible outputs: halt and loop. These "outputs" of course correspond to whether a reduction in the abstract machine terminates, but we could just as well give them arbitrary labels, say, true and false.

When you encode a datatype and a computation in the lambda calculus, you might want to check that your computation gives the correct result, not just whether it halts. But the theorem will still be stated as a truth-valued proposition: either the computation got the right result, or it didn't. So assuming the encoding includes operations that can compare two results, you can always wrap the computation in an observer that drives the "lambda machine" to produce its true output (halt) if the computation produced the right result, and false output (loop forever) if the computation produced anything else.

For example, say we want to show that two different implementations of a function, f and f′, always produce the same result. We could do this directly by comparing their results, but this involves reasoning about the encoded result values. Since the datatype already has operations that simulate the inspection of its values, this would in a sense be a duplication of effort. Instead, we can use the observer operations--an equality test, for example--to compare the results to an expected value and then either halt or loop.

Thus if there is a context in which f and f′ are not equivalent, that is, in which they produce different results, then this implies that there is a context in which f causes the machine to halt and f′ causes the machine to loop. The statement of contextual equivalence is usually given as the contrapositive: if there are no such contexts, that is, in all contexts they either both halt or both loop (they "co-terminate"), then f and f′ are equivalent.

So these two outputs from the lambda machine are sufficient to formulate the statement of any proposition about expressions, so long as it depends only on properties that are observable within the lambda calculus.

How to read a semantics

Some tips for myself on how to read a semantics:

1. Follow the textual description first. Usually they have thought about an order in which you should try to understand the rules.
2. If you get stuck on one of the rules, circle the part that's confusing or write down what you don't get and skip it. Don't spend too long on any one part. (More often than not I embarrass myself by beating my head over something confusing only to find that it's explained in the next paragraph.)
   
3. To understand the role a particular expression form plays, read its introduction and elimination rules. To understand the role an environment plays, read its extension and lookup rules. To understand any one of these rules, read its dual rule. Most of these rules make much more sense in pairs.

Another couple of general tips: take notes on the semantics and actually copy down the rules, but don't copy down the rules that are simple structural inductions or unchanged from previous variations. Also, take breaks. And never get caught reading papers after 2am.

Lambda-encoding derivation, take 2

I had the basic idea of the lambda-encoding of lambda terms right, but I was sloppy with the type derivation. The important piece that I missed was that the result type of the continuation needs to appear in two places. In general, we say a type α is equivalently representable as a function from continuations to final results:

α = (α → ο) → ο

Or you can think of this in logical terms as the equivalence

α = (α ⇒ ο) ⇒ ο

I can prove this easily with classical logic, but I had trouble finding resources presenting the axioms and standard equivalences of intuitionistic logic, and I don't feel like trying to come up with a correct, intuitionistic derivation.

The derivation of disjoint unions as pure arrow types is simple, at least using the normal rules of classical logic:

  α ∨ β
= ((α ∨ β) ⇒ ο) ⇒ ο
= ((α ⇒ ο) ∧ (β ⇒ ο)) ⇒ ο
= (α ⇒ ο) ⇒ (β ⇒ ο) ⇒ ο

Notice how the currying makes much more sense than it did last time, now that the second occurrence of the result type is there. Implication and conjunction are obviously not equivalent (duh)! But you can curry a conjunction that occurs on the left-hand side of an implication.

Again, I'm not sure how hard this is to prove intuitionistically. But assuming that goes through okay, we get the type equivalence:

α + β = (α → ο) → (β → ο) → ο

Generative vs. generative

Crap. I just realized that I was borrowing a term to describe macros that already has another meaning in the macro literature. Generative macros, according to Ganz et al, are macros that do not inspect their arguments syntactically. I was using the term as I think it's used in the parameterized module literature, to mean procedures that produce different results every time they are invoked. Mumble.

Lambda-encoded lambda terms

In The Theory of Fexprs is Trivial, Mitch encodes a datatype in the lambda calculus that itself represents the abstract syntax of lambda calculus terms. The encoding trick involves both higher-order abstract syntax and some cute type equivalences.

Here's a data definition of the abstract syntax terms:

data Term α = Var α
            | Abs (α → Term α)
            | App (Term α) (Term α)

Notice that the variant representing abstractions is itself encoded using a (meta-language) abstraction. So we can represent the program λx.(x x) as:

Abs (λx.(App (Var x) (Var x)))

This is already a useful hack, because we don't have to come up with a datatype to represent variables, and if we wanted to deal with substitution it would be handled automatically by the substitution mechanisms of the meta-language.

But we need to have some way of representing algebraic datatypes. For this we use the following equivalences:

  α + β → ο
≈ (α → ο) × (β → ο)
≈ (α → ο) → (β → ο)

So to reduce the implementation of a k-variant disjoint union to pure lambda calculus, we CPS the values and split out their continuations into k separate partial continuations. Thus we get our final encoding of the abstract syntax of lambda terms:

⌈x⌉     = λabc.ax
⌈λx.M⌉  = λabc.b(λx.⌈M⌉)
⌈(M N)⌉ = λabc.c(⌈M⌉ ⌈N⌉)

Update: I hadn't made the Term datatype polymorphic in its variable type. I think this is right now.

If I were teaching macros

Yeah, if I were teaching macros I'd start without pattern matching. I would start with a programmed macro system like the one described by Dybvig et al, just without mentioning syntax-case. That way you'd have properly lexically scoped macros. And I wouldn't tell the students about datum->syntax-object so that they couldn't break hygiene. Here are some chapters in this hypothetical tutorial:

Lesson 1: Metaprogramming: programs that write programs.

Learn how to create syntax objects to create quoted code, by analogy to quote; talk about the phase distinction; write some simple macros that generate programs; make (over-)simplified analogy to cutting and pasting code.

Lesson 2: Macros are embedded metaprograms.

Demonstrate that macros can refer to identifiers that are in scope. Show that there's no danger of such identifiers getting captured when macros are referentially transparent; refine the idea of cutting and pasting code to being more than just textual replacement -- a variable reference identifies a binding and the generated code reproduces that binding, not necessarily the name.

Lesson 3: Macros can introduce identifiers.

Demonstrate how macros can introduce brand new identifiers; show that in hygienic macro systems those identifiers can never refer to existing bindings in any program, only to uses of the same identifier within a macro's templates; show how identifiers given as parameters can generate binding occurrences, bound occurrences, and quoted occurrences of the identifier.

If I could get through all of that without pattern matching, that'd be cool, but somewhere along the line the code might just get too hairy without it. (Then again, Lisp defmacro hackers live without it, don't they?) Since pattern matching is orthogonal to the above lessons, I would love to put it off until after mastering metaprogramming, the phase separation, and issues of scope.

Some might claim you can write macros in a hygienic macro system without understanding properly lexically scoped macros, since they're just taken care of for you. That's pretty much doomed to failure, because as a macro writer you need to understand the distinction between names and identifiers in order to know when you can and can't bind a particular identifier.