[Prev][Next][Index][Thread]
Re: "foundations built on sand"
I guess it is time for me to jump back into this discussion since my
book (Foundations of Object-Oriented Languages: Types and Semantics) is
again the focus of discussion. I'll add my response after Thomas' comments.
Thomas Streicher wrote:
...
>
> This last example also brings to the point that one NEED not insist on
> denotational methods, also operational or proof-theoretic methods definitely
> can do the job. Just sometimes denotational methods are more concise and,
> therefore, much easier to grasp.
>
> This brings me back to my original question concerning translation of SOOL
> to META + F_{sub,rec,state}. From my point of view everything would be ok
> if the target language F_{sub,rec,state} were endowed with an appropriate
> operational semantics. I haven't seen such work and it is not contained in the
> FOOL book. Some of it is sketched there but operational semantics of state
> isn't dealt with at all and that's what I consider most critical.
> As I understand the main theorem is that
>
> (Sound) if t : A in SOOL then [|t|] : [|A|] in META
>
> this definitely should be accompanied by a proof that
>
> (Refl) if [|t|] doesn't give rise to a run time error
> then t doesn't give rise to a run time error
>
> This second property is rather assumed than proved. That's my impression
> though I really might be mistaken as I didn't read everything in detail.
>
Unfortunately, this misses the entire point of a translational
semantics. The idea is that we compile SOOL to META and then run the
translated program in META. The reason you did not find the (Refl)
property proved anywhere is that I did not provide a direct (run-time)
semantics of SOOL! Hence this property doesn't make sense in the
context of my book. However, see below.
> In any case I don't insist on denotational models though I definitely prefer
> them when available. Also operational methods may allow one to find
> conceptually clear invariants (`a la logical relations) that allow one to
> guarantee the absence of some undesired effects.
>
I have used a variety of different semantics in studying these languages
over the last 10+ years. Originally I used a denotational semantics for
FOOPL, a functional OOL (see A Paradigmatic Object-Oriented Programming
Language: Design, Static Typing and Semantics, Journal of Functional
Programming 4(1994), pp. 127-206), but wasn't happy with the fact that I
didn't know a model with all of the features I needed, and, besides, I
was interested in moving to an imperative language where operational
semantics seemed more appropriate. Since then I have a couple of
different operational semantics for imperative extensions of this
language. The most recent version (PolyTOIL: A type-safe polymorphic
object-oriented language, by Kim B. Bruce, Adrian Fiech, Angela Schuett,
and Robert van Gent) is about to appear in TOPLAS. It can also be
gotten through my web page at:
http://www.cs.williams.edu/~kim/README.html
It uses a (natural -- big-step) operational semantics to prove
type-safety via a subject-reduction theorem. The development is long
and technical, but does provide direct run-time semantics for a
polymorphic object-oriented language very much like language PSOOL from
my book (it essentially adds polymorphism to SOOL).
Perhaps if I had used that in my book, you would have been happier.
While I personally believe I get a good intuition of the run-time
behavior of OOL's from the operational semantics, for pedagogical
reasons I chose to follow the lead of Pierce and others and use a
translational semantics. I didn't want to get hung up in the tedium of
a subject-reduction theorem and hoped that I could rely on the reader's
knowledge (and intuition!) about the polymorphic lambda calculus to
simplify my exposition. In particular, I have been somewhat dismayed
that the operational semantics has gotten much harder to read as the
details of the subject-reduction proof have been perfected.
So, if you want a proof built on rock-solid operational semantics, I
suggest that you take a look at the paper on-line. However, you might
first look at the translational semantics in the book for a better
pedagogic motivation of the semantics.
By the way, my book did not include the soundness of the language NOOL,
introduced in chapter 18. A paper with detailed operational semantics
and type-safety proof of LOOM, a very similar language, will be
forthcoming when we get a chance to finish revising the paper.
Meanwhile a conference version of the paper, Subtyping is not a good
``Match'' for object-oriented languages, with Fiech and Petersen, is
available on the web page referenced above (though the journal paper
semantics will be somewhat different).
Finally, let me make a quick response to Matthias' question about false
claims modified on the basis of semantics:
William Cook wrote a paper in ECOOP '89 pointing out type holes in
Eiffel, including those based on the "like Current" construct, which is
very much like MyType (except not statically type-safe). Cook et al
then showed in POPL '90 how to model a MyType construct in a type-safe
way in the polymorphic lambda calculus. Since then I've explored how to
incorporate this into a high-level language and provided static
type-checking rules (see my book). While no major language (aside from
Eiffel) has picked this up in its strongest form (and they have not
fixed the type-checking rules in ways many of us had hoped -- they've
done other things instead), I have hopes that someday such a construct
will be adopted in a major language. I also don't believe believe that
one could get the type-checking rules correct for such a construct
without a strong understanding of semantics. So, at the moment, there
is no "success story" here, but instead some pointers for future
language designers.
I believe there is also some work on making Beta statically type-safe
that may be relevant here, but I'll leave that to others more
knowledgeable about Beta.
Kim