return when desugaring to closures

Dave Herman dherman at ccs.neu.edu
Thu Sep 4 12:38:39 PDT 2008


> Hmm. I thought the motivation for using SML is that it had a definite
> formal semantics (for which the last revision was published a decade ago),

Not really; I suppose it's nice to know that the underlying 
meta-language is formalized, but this would really only provide 
practical utility if we were proving theorems about ES. While there are 
interesting theorems that you might like to prove, it's not as high a 
priority as the actual design, specification, and reference 
implementation work. Being able to execute the spec and run test cases 
is an enormous leap forward in terms of quality assurance; being able to 
prove correctness properties would be even better but not as *much* 
better as just being able to run code.

In practice, proving theorems about PL's means either choosing stylized 
subsets or using mechanized frameworks. It's just not efficient or 
cost-effective to prove theorems manually about artifacts as large as 
real-world languages. Mechanized frameworks like ACL2, Coq, Twelf, and 
Agda are making great progress, but they are still unwieldy and too 
challenging. We settled on ML as a simple, well-understood language that 
is well-suited for implementing PL's.

Down the road, if we were to use one of these mechanized frameworks, 
we'd have to transliterate the RI code into the meta-language of the 
framework we'd chosen, which would be stylistically similar to ML but 
wouldn't be ML. And the language wouldn't have *any* of the side effects 
of ML, so then we'd still have to add shift/reset on top of the 
meta-language, as well as mutation and exceptions (and possibly even 
non-termination).

> that had already been looked at and understood by many people.
> Handwaving about the possibility of adding delimited continuations to
> that formalization is not the same thing, even if you are right in
> saying it is "easy".

I've written a paper that shows you can implement shift/reset in ML as a 
library using call/cc [1]. And call/cc is very well-understood -- it's 
been around for decades in Scheme and has been formalized repeatedly, 
and it's been in SML/NJ for over a decade. It's been added to models of 
ML in the literature and proved type-sound. More directly, shift/reset 
has been formalized as well.

But that's for the academic pin-heads. :) In much more conceptually 
appealing terms, this is my favorite explanation to date of delimited 
continuations:

http://blog.moertel.com/articles/2008/05/05/olegs-great-way-of-explaining-delimited-continuations

I like to imagine that demonstrates that as programmers we actually 
already have good intuitions about delimited continuations, and that 
they aren't as scary as they sound.

But you're right that this comes down to a question of clarity. Which 
option is more obfuscated: specifying the entire language in CPS just 
for one feature, or using an esoteric low-level language construct that 
isn't well-known outside of the research world? It's definitely a 
trade-off. But I don't think the real concern is whether this makes the 
spec "less formal." It's just a concern about clarity.

Dave

[1] 
http://www.ccs.neu.edu/home/dherman/research/papers/icfp07-great-escape.pdf


More information about the Es-discuss mailing list