Hi,
I am using SMLNJ and trying to understand the difference between
callcc/throw and capture/escape. As far as I can tell, they differ
only in how they treat exception handlers; however the textual
descriptions of them that I have seen are not clear to me.
For instance:
capture f
Apply f to the "current continuation". If f invokes this continuation
with argument x, it is as if (capture f) had returned x as a result,
except that the exception-handler is not properly restored (it is
still that of the invoker).
This description makes it sound as though each continuation has only
one exception handler. However my intuition for exceptions suggests
that handlers should be sprinkled throughout the continuation (one for
every "handle" expression in the current dynamic extent). Is the
description I quote above written in terms of how exceptions are
implemented in SMLNJ (i.e. does a continuation have a single
"exception handler" that handles all exceptions), or does SML really
have a notion of a single exception handler?
Is there a formal specification of capture and escape somewhere?
Perhaps something similar to Felleisen and Wright's specification of
callcc in CoreML?
Thanks,
ron