[Re: [clean-list] Clean in the Real World]

Fergus Henderson fjh@cs.mu.oz.au
Thu, 18 Dec 2003 11:58:12 +1100


On 17-Dec-2003, Marco Kesseler <m.wittebrood@mailbox.kun.nl> wrote:
> >> If (a + b) throws an exception, it HAS NO RESULT. 
> >
> >Yes it has: the exception itself (at least in a language where 
> >exceptions are first-class). As Fergus said, the output type of
> >a function (normally) returning an xxx and (possibly) throwing
> >an eee is the discriminated union of xxx and eee.
> >
> >Or did I misconstrue his posting?

No, that's what I meant.

> Yes, I think that the exception itself should be a first-class value. 
> At least, I see no good reason not to.
> 
> There is no law however that says that the output type of a function 
> should be interpreted as the union of its "actual" type and some 
> exception type.  I like the idea that the type that I write down for a 
> function result is actually the type it has.

You're right, that's not the only way of doing it.
It is the standard way of modelling the semantics of lazy
functional languages, but it is not the only possible way.

Another alternative -- which we use for Mercury! -- is to not try to
model exceptions in the declarative (denotational) semantics,
and instead define the semantics of exception handling only in the
operational semantics.  Of course you do have to give some semantics for
the try/catch construct in the declarative (denotational) semantics,
but so long as this construct is in a nondeterminism monad or equivalent,
those semantics can be loose.  The denotation of the try/catch construct
can give a set of possible results, which includes the possibility that
an exception occurred as well as the possibility that it didn't.

This approach has the advantage that the semantics of types are more
obvious; for example, the boolean type has two values, not three.

However, it is not without some counter-intuitive effects.  Consider an
expression such as "1/0 - 1/0".  You still need to give a denotational
semantics for each subexpression and for the expression as a whole.
In Mercury's declarative semantics, this expression has the value 0,
since the denotational semantics of 1/0 must be the same each time,
and x - x = 0 for all x.  But in the operational semantics, "1/0 - 1/0"
may obviously throw an exception.  The operational semantics is sound
w.r.t. the declarative semantics, but not necessarily complete.

For more on this, see the Haskell mailing list archives, in particular
<http://www.dcs.gla.ac.uk/mail-www/haskell/msg02086.html> and the thread
which follows, and <http://www.dcs.gla.ac.uk/mail-www/haskell/msg01709.html>.

-- 
Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.