What makes a good paper?

Or: Theorems are the test cases of semantics

Good PL papers define their systems with enough greek symbols, funky operators, inference rules and the like (what Mitch calls "dirty pictures") to demonstrate depth and precision of intellectual content. Without proving subsequent theorems based on these systems, though, there's no evidence that these systems are actually consistent or even useful.

A programming language semantics is, as Mitch puts it, "a mathematical model for predicting the behavior of physical systems." One of its primary purposes is reasoning (at a particular level of abstraction) about programs written in that language. It's generally hard to prove that a semantics is "the right one" for the problem space, which is a fuzzy notion, but theorems raise its probability of being useful.

A semantics alone may at least convey information about a language, since math is often more concise and precise than English. But without being put into use, it's doubtful whether it is really a specification; it's far too easy to slip into specifics as an algorithm. Or at the other extreme, it may leave out too many details to address the salient issues in the problem space. And who knows what subtle errors are lurking within the language definition? The best way to ensure that a semantics accurately defines a language at an appropriate level of abstraction is to prove theorems with it.

Delicious dudgeon

From Joel.

Values in Non-Strict Languages

In the literature on non-strict languages, the term "value" seems to be used in a different way. In call-by-value languages, we classify a set of normal forms that we define as the "values" of the language, and arguments to functions must evaluate to values before the functions can be applied. But because in call-by-name or call-by-need languages, you can pass arbitrary, unevaluated expressions to functions, the notion of a value is in a sense less critical. You still need to define the normal forms in order to determine when to stop evaluating the whole program (or when to stop evaluating arguments to primitives with strict positions). But interestingly, in The Implementation of Functional Programming Languages, Peyton Jones still refers to the expression that a function argument is bound to as the variable's "value" -- despite the fact that it may not be in weak head normal form. Apparently the term "value" is informally used to mean a variable's binding, whereas the final result of an evaluation is only referred to as a normal form.

A packrat parser for Scheme

Through some random poking around the web, I just discovered this packrat parser in R5RS Scheme. I need to check that out.

Update: That's a parser in Scheme, not a parser for Scheme. (Thanks, Mitch.)

Update²: Not entirely random, Noel, thanks. Though discovering Tony's files by URL munging certainly was random.