Andrej Bauer on PLD

On Andrej Bauer's indispensible weblog, he posts On programming language design, which articulates some ideas about the value of safety of inductive data types, type safety, etc. Gains a thumbs up by Robert Harper.

Quibble: out-of-scope variables

One of his comments criticises allowing functions to refer to out-of-scope names in function definitions, on the grounds that the resulting error messages, in the case he gives, python-2.4, are hard to understand.

In fact, python-2.4's error messages do identify the context in which the unbound variable was invoked, saying something along the lines of:

>>> foo.bar(0) Traceback (most recent call last): File "", line 1, in File "foo.py", line 14, in bar val = n+i NameError: global name 'i' is not defined

I think in general this sort of error is of a superficial kind, and doesn't provide a strong basis for design criticism.

By Charles Stewart at Wed, 2009-04-22 11:08 | login or register to post comments

Re-quibble: and I said so

I do not understand your comment. I explicitly wrote in my blog: "To be honest, Python kindly displays the correct error message showing that the trouble is with the definition of f". I do not see where in the section on out of scope variables I complained about hard to understand errors. I only complained about errors appearing at runtime instead of compile time. Are you referring to some other section of the post, or another post?

By andrejbauer at Thu, 2009-04-23 05:26 | login or register to post comments

Shallow issues

I enjoyed your article, and I especially found the When should mistakes be discovered? section wise. I apologise for not having noticed your comment conceding exactly the point I made, but this is orthogonal to the point I tried, and failed to make. Let me try again.

Static typing is a language design discipline that has non-shallow consequences: it imposes nontrivial constraints on what counts as a correct program that generally improve the safety of programs, and permits more sophisticated correctness tools such as QuickCheck[1].

The issue of using variables before they have been assigned is modelled adequately in Python by simple syntactic analysis [2], and can be rolled into tools like PyChecker. For these sort of issues, one can be liberated from oppressive compilers and still deliver code free of certain classes of bug.

There's a couple of further points worth making. First, allowing the use of unallocated variables may facilitate top-down development, as its is used in Smalltalk-style "coding in the debugger". Second, maybe type inference is something that can sometimes be moved from the oppressive compiler to freely-invoked tools: the key finding making Typed Scheme possible is that a large corpus of Scheme code already conformed to a particular type discipline. Similar properties might hold for some other dynamically typed languages.

[1]: Erlang supports QuickCheck without type inference. This leads to more work by users to specify generators, and a higher risk of writing incorrect requirements, according to Arts, Hughes, Johansen, Wiger (2006) Testing Telecoms Software with Quviq QuickCheck. There's work on designing type systems for Erlang to support checkable requirements.
[2]: Of course, languages that allow conditionals to test whether variables are defined are another matter.

By Charles Stewart at Fri, 2009-04-24 08:30 | login or register to post comments

Conditional type-checking

One can often hear static type checking characterized as oppressing and limiting, perhaps on the grounds that we can successfully run code than we cannot type-check. What is seldom realized is that the converse is true as well: we can type-check code that we cannot run. The simplest example is "x+1". We can't evaluate the code as we don't know what "x" is. It is a free variable. We can still type-check it, obtaining the type: ``provided that x is of type int, the result is of type int.'' The type is conditional, imposing a constraint on contexts in which the expression can be used. Type-checking is often presented as a partial procedure that, given an expression and a type environment Gamma, returns the type of the expression. However, type checking can just as well receive only an expression and infer both the type and the (minimal) type environment Gamma. In fact, this is how type checking has been presented in earlier texts, e.g., John C. Mitchell's ``Foundations for Programming Languages'' (Section 11).

As an example, the file
http://okmij.org/ftp/Computation/FLOLAC/TInfTEnv.hs
implements the type reconstruction for essentially PCF (typed lambda-calculus with integers, conditionals and fixpoint). The test test3 shows that the term \x. if x then 1 else y has the type int->int provided the context binds y to an integer. On the other hand, the open term if (x 1) then x else 2 fails the type-check: it is ill-typed in any context (see test63).

Conditional type-checking is common for type-and-effect systems, e.g., delimited continuations. For example, the inferred type for shift k. if k 1 then 2 else 3 shows that the expression has the type int provided it is used in the delimited context with the answer-type bool.

By Oleg at Sat, 2009-04-25 04:29 | login or register to post comments

Degrees of oppression

Just to be clear, the term oppression comes from Andrej's post, and is a didactic issue: his students seemed to find it more dispiriting to be told by a static checker that their program is wrong than to find out the problem when they run it. I guess that this exact problem vanishes when the students understand what type soundness is about.

By Charles Stewart at Mon, 2009-04-27 07:54 | login or register to post comments

The web as we know it

Andrej Bauer said:
The web as we know it would not exist if every javascript error caused the browser to reject the entire web page (try finding a page on a major web site that does not have any javascript errors).

While I agree with the statement, I can't help but think the difference would be positive: a web with far fewer JavaScript errors, likely some better tools for programmers writing web-pages, and possibly better JavaScript performance.

By dmbarbour at Thu, 2009-04-23 04:00 | login or register to post comments

How can it be positive?

If you agree with the statement, then the positive difference would be that everybody would have javascript disabled (as was the case for many of us in the bad old days of no pop-up blockers), or that web developers wouldn't be using javascript.

The alternate reality would be that instead of javascript as the dynamic engine of a page, you would have some bytecode engine (Java, Flash, Silverlight...) running it.

By Dave Lopez at Thu, 2009-04-23 19:47 | login or register to post comments

If you agree with the

If you agree with the statement, then the positive difference would be that everybody would have javascript disabled

To agree with "the web as we know it would not exist" is only to agree that the web would not be as we know it. It does not logically follow that everybody would have JavaScript disabled. Indeed, if one could make more guarantees about the properties of JavaScript, it is ever more likely to be enabled. For example, support for object capability model (between JS and the DOM) would allow far more readily for constructing safe page mashups without risks to privacy.

Statically typed JavaScript would mean that errors - at least those that can be caught by static typing - occur fast and early in development, and that the browsers or IDEs would help the web-programmers find these errors. Provable safety with JavaScript wouldn't necessarily eliminate support for automatic conversions, nor does it imply manifest typing would be required.

or that web developers wouldn't be using javascript

That's another possibility, true. But I suspect web developers would use JavaScript more because browsers support JavaScript than because of its peculiar development properties.

The alternate reality would be that instead of javascript as the dynamic engine of a page, you would have some bytecode engine (Java, Flash, Silverlight...) running it.

Compiled page content for interactive scene-graphs and zoomable UIs, whether it be compiled remotely and delivered as proof-carrying-code or compiled locally by the browser, is a realistic and viable future that is already bleeding into the present (JavaScript V8 and SpiderMonkey's JIT, Google Web Toolkit, etc.). I don't believe we'll need to look for those features in an alternate reality.

By dmbarbour at Thu, 2009-04-23 20:39 | login or register to post comments

Lambda the Ultimate

User login

Navigation