Re: lillibridge, strong termination, exceptions


Subject: Re: lillibridge, strong termination, exceptions
From: Matthias Felleisen (matthias@ccs.neu.edu)
Date: Tue Feb 05 2002 - 07:57:39 EST


Mark's result is now a decade old and still not relevant to understanding
exceptions and continuations. The trick is that SML (note the S) style
exceptions automatically provide you with something like recursive types.
So, what he says is that STLC plus something like recursive types gives you
infinite loops. Duh.

If you really want to understand the relationship among state, exceptions,
and continuations, take a look at Hayo Thielecke's papers. He has studied
this in depth, based on my own theory of expressiveness. I can summarize
the ideas as follows:

 exceptions can't express continuations wrt to lambda [typed or not]
 continuations can't express exceptions "
 exceptions plus state can't express continuations "
 exceptions and continuations can't express state "
 exceptions and SML's capture/escape conts can express state
conjecture:
 continuations plus state can express exceptions "

-- Matthias



This archive was generated by hypermail 2b28 : Tue Feb 05 2002 - 07:57:40 EST