[clean-list] exceptions again (a bit long, but this might actually be correct)

Simon Marlow simonmar@microsoft.com
Wed, 28 Jan 2004 23:13:26 -0000


 
> Here is the hole: f (x + y) may not equal f (y + x), because 
> the (lazy)
> evaluation of (x + y) within f may throw a different 
> exception than the
> evaluation of (y + x). And for different exceptions, h a e may differ.
> This is a serious problem that destroys referential transparency.

The hole is worse than that.  We know that (x + y) is supposed to be
observably equivalent to (y + x) for any x and y, so then it must be
true that

  (x + y)
  catch e = ...

is equivalent to 

  (y + x)
  catch e = ...

(by referential transparency: I just replaced an expression with an
equivalent one in a context).  However, these two are clearly not
equivalent: (x+y) might raise a different exception from (y+x), which
might get handled differently by the catch and hence the value of these
two expressions can differ.

Regardless of laziness, this language is has lost properties that it
used to have.

You have two options: accept that (x+y) and (y+x) are not the same, or
move catch into a non-determinism monad or somesuch.

Of course, I'm only using the addition operator as a specific example
here.  There is a whole class of equalities at stake: namely those in
which re-ordering evaluation does not change the denotation of an
expression.  See the imprecise exceptions paper[1] for details.

Cheers,
	Simon

[1] http://citeseer.nj.nec.com/196569.html