[clean-list] Clean in the Real World

[Fergus Henderson]

On 16-Dec-2003, Marco Kesseler <m.wittebrood@mailbox.kun.nl> wrote:
> [Simon Marlow wrote:]
> >I think you've missed the point here.  Yes, you can still use equational
> >reasoning in your system, but there are now fewer equations which are
> >valid.  For example, previously I had the equation
> >
> >	a + b  =  b + a
> >
> >but now this doesn't apply.  If you don't put the exception catcher in a
> >nondeterminism monad (or similar), then your language ends up with fewer
> >equational properties.  This is precisely what we went to great lengths
> >to avoid in Haskell.
> 
> Commutativity is NOT a property of all functions. '-' is not 
> commutative. '+' is not commutative because it uses the '+' symbol. 
> Commutativity can only be established after inspecting the function 
> definition.

Yes.  But in mathematics, "+" is normally commutative.
It would be nice if that was true of our functional programming
languages too.

> Say that '+' has been defined like:
> 
> (+) a b = add a b.
> 
> 'add' is a primitive operation that is strict in its arguments. It 
> first evaluates arg 1, then evaluates arg 2, and then adds them. All 
> of these steps may throw exceptions. Kind of a real world thing (for 
> all of you who wonder about this thread's subject).
> 
> '+' remains commutative here:

No, it doesn't. 

It is commutative for arguments that do not throw
exceptions, or in the case where only one argument throws an exception,
or where both arguments throw the same exception.  But if both arguments
throw distinct exceptions, then the result of "a + b" will be different
from "b + a", because it will throw a different exception.

I suppose you could call it "semi-commutative" or something like that,
in the sense that it is commutative for non-exceptional arguments.
But we are also interested in cases where exceptions are thrown
or where the program fails to terminate.

> no exception thrown inside (a + b) will 
> _ever_ influence the value of (a + b), as all exceptions will just 
> pass up to higher levels.  These higher levels will _not_ be able to 
> establish the value of (a + b). They only know that some exception 
> was thrown while evaluating it.

Once you introduce exceptions, semantically the value of (a + b) is
a discriminated union of either a number or an exception.  Higher
levels can establish which exception was thrown.

> Now suppose that we add a general catch to the '+' definition. Just 
> for the sake of the argument, because this is probably pointless for 
> a function like '+'.
> 
> (+) a b
>     = add a b
>     catch _ = NotANumber /* map any exception to this special value */
> 
> Now, '+' is _still_ commutative, because any exception maps to the 
> same value.

This version of "+" is commutative (but not "_still_" commutative,
since the original one wasn't commutative!). 

However, it doesn't propagate any exceptions.  So it doesn't solve the
problem of introducing exceptions while retaining equational reasoning.

> We take the definition of (+) one step further:
> 
> (+) a b
>     = add a b
>     catch DivideByZero = NotANumber /* the only exception that we 
> handle */
>     catch e = throw e /* we pass all other exceptions to higher 
> levels */

This one is not commutative.

> So, let's REALLY break commutativity!
> 
> (+) a b
>     = add a b
>     catch DivideByZero = NotANumber
>     catch _ = AVeryBigValue /* Sad */

Yes, this one is not commutative either.

> Okay, so now we have defined a non-commutative '+'. Do we need 
> exceptions for that? No. If I want, I can define a non-commutative 
> '+' in Clean today.

We're not trying to define a non-commutative '+'.
We're trying to define a commutative one!
The point is that today in Clean one can easily define a commutative '+'.
If we introduce exceptions and allow catch only in a nondeterminism monad
or equivalent, then this will still be the case.  But if we introduce
exceptions in the way that you have proposed, it won't be possible to
define a commutative '+' without explicitly catching exceptions (as in
your second example above), and we don't want to do that, since the
whole point of introducing exceptions was to have them automatically
propagate through operations like '+'.

-- 
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.