[Prev][Next][Index][Thread]
Re: Call-by-value (eager) vs. Call-by-name (lazy) Re: Call-by-value (eager) vs. Call-by-name (lazy)
> A second set of questions have to do with programming language theory.
> Given the predominance of call-by-value languages in practice, what is
> the most appropriate theoretical approach? Does this necessarily imply
> that we should drop cpo's with bottom in favor of Plotkin's domain theory?
> ("Pre-cpo's" was the term I think Abramsky suggested.) On the positive side,
> in teaching, I find it much easier to explain the set-theoretic ordering
> on partial functions than the point-wise ordering on flat cpo's, for example.
> Furthermore, at higher types, it is clear that the partial function approach
> involves fewer artifical elements. On the other hand, I have found the
> discussion of alternate reduction strategies very successful in my class,
> with relationships to optimization, and I am somehow reluctant to drop
> call-by-name.
------------
I just finished teaching a course (to 3rd year undergraduates) on
semantics (operational and denotational). The domain theoretic parts
used bottomless cpo's and TOTAL continuous functions, with bottom
introduced as and when you need it via lifting---in other words, the
"standard" model of Moggi's computational lambda calculus where the
monad is lifting. (I didn't inflicted the students with this
categorical viewpoint explicitly.) I regard this as the
have-your-cake-and-eat-it approach, since in some sense you both do and
don't have bottom. One technical advantage of working in the category
of bottomless cpo's and total continuous functions is that it has nice
set-like things such as disjoint coproducts (hence conditional is a
derived concept---what's the problem?) and natural numbers object.
In the course I covered (albeit quite superficially, and only for a
first-order language) both call-by-value and call-by-name in this
setting and proved the standard adequecy results for operational
semantics of each. Tell you how the students found it when I mark the exams.....
BUT, the course didn't go as far as solving recursive domain equations.
Maybe the bottomless+total+lifting style isn't so good for teaching
this. Anyone out there tried?
Andy Pitts