return when desugaring to closures
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
> 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 . 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
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.
More information about the Es-discuss