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.
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?
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:
JavaScript language level
I've released the first version of my JavaScript language level for DrScheme in PLaneT, the centralized package distribution system for PLT Scheme. To try it out, do the following:
- Install DrScheme version 30x.
- Add the binaries directory (
$PLTHOME/binunder Unix derivatives and%PLTHOME%under Windows) to your system'sPATH. - From the command line, run:
planet -i dherman javascript.plt 1 0
- Now start up DrScheme and select "JavaScript" from the "Choose Language..." menu item.
Tuesday, February 21, 2006
ECMA-262 Edition 4
As Brendan Eich announced yesterday, I've been invited to join Mozilla and ECMA in the process of defining and specifying the next version of JavaScript--erm, EcmaScript. Brendan kindly refers to me as an "expert" (for which I've heard no end of snickers from my colleagues--thanks guys), but I expect to learn a lot from this experience. I just met the Mozilla and ECMA guys last week, and they seem great to work with.
I'm really excited about the marriage of formal methods and practical application. I love to see this kind of cooperation between research and industry. At a minimum, the PL community's knowledge about formal specification should help the committee with its goal of making the spec clear and precise. We are actually hoping to see some correctness proofs as well--e.g., type and contract soundness. And I'm keeping my eyes peeled for other useful consistency properties worth verifying.
Sorry about the silence lately. Now that the word's out, I hope to talk more about some of the interesting points that come up in the EcmaScript process.
I'm really excited about the marriage of formal methods and practical application. I love to see this kind of cooperation between research and industry. At a minimum, the PL community's knowledge about formal specification should help the committee with its goal of making the spec clear and precise. We are actually hoping to see some correctness proofs as well--e.g., type and contract soundness. And I'm keeping my eyes peeled for other useful consistency properties worth verifying.
Sorry about the silence lately. Now that the word's out, I hope to talk more about some of the interesting points that come up in the EcmaScript process.
Subscribe to:
Posts (Atom)
