[clean-list] Clean in the Real World

[Marco Kesseler]

Fergus wrote:
>On 15-Dec-2003, Marco Kesseler <m.wittebrood@mailbox.kun.nl> wrote:
>> Fergus wrote
>> >On 15-Dec-2003, Marco Kesseler <m.wittebrood@mailbox.kun.nl> wrote:
>> >If you don't inhibit such optimizations, then you would end up in the
>> >situation where applying simple and obvious transformations such as
>> >replacing a variable with its definition might change the program's
>> >behaviour.
>> 
>> Suppose I have:
>> 
>> Start
>>     = program
>>     catch DivideByZero = abort "divide by zero"
>>     catch StackOverFlow = abort "stack overflow"
>>     catch ...
>
>In your example code above, you didn't give a precise syntax or semantics
>for the new "catch" construct...

I am not really in a position to do such things in any sensible way 
(This is not my job).

>am I right to presume that you mean
>that this construct could be used in contexts where there is no World
>passing or nondeterminism monad?

Yes.

>For example, could it be used in
>
>	foo :: Int
>	foo
>	    = bar
>	    catch DivideByZero = baz

Yes.

>If so, then either (a) I won't be able to safely apply equational reasoning
>to my programs any more, or (b) compiler optimizations will be inhibited
>for any code which might be guarded by a catch.

You will:
(a) be able to apply equational reasoning within your program, in the 
sense that if an exception occurs within foo, it will always deliver 
the same result (baz), because it will always throw the same 
exception, by virtue of the compiler generating a fixed evaluation 
order for bar. If no exception occurs, everything will be as usual 
and bar gets returned (but also see below).
(b) have compiler optimisations both in bar and baz, as it does not 
matter which exception gets thrown in bar, as long as it is the same 
one each time within a single program.

The one thing that is not possible, in terms of optimisation, is to 
simply replace occurences of foo by bar. You cannot, because foo does 
not just equal bar, and there is no notation to attach the handler to 
a loose bar. And you should not because then the compiler would have 
to ensure that each of these occurences of bar employs the same 
evaluation order.

>> Yes, I agree that it depends on the optimisations which exception 
>> will get thrown first.
>
>Right.  And that in turn means that the value of "Start" (or "foo") may
>differ depending on what optimizations are applied.  Which may depend
>on seemingly unimportant details of the implementation of "program"
>(or "bar").

Yes, this is actually more reproducable than via a nondeterminism monad.

>Unless code which catches exceptions is restricted to a nondeterminism
>monad or equivalent, referential transparency will be violated.
>Programmers will no longer be able to safely apply equational reasoning
>to transform the definition of "bar", because such transformations
>might change the value of "foo".

Programmers can use whatever equational reasoning they want to 
transform the definiton of bar. Within bar there is _nothing_ that 
reminds the programmer of exceptions. And if they do not make 
mistakes, the meaning of bar will stay exactly the same.

Now if you recompile your program after transforming it, AND the 
evaluation of bar leads to an exception AND the transformation leads 
to a _different_ exception than before, then yes, foo _may_ deliver a 
different value than before. However, it will do so _consistently_ in 
your program, and you can honestly say that foo == foo. The latter is 
something you _cannot_ say if you use the Monadic approach, were a 
"deus ex machina" tells you which exception value to take each time 
you refer to getException.

Does it really matter whether this exception happens because the 
strictness analyser spent more time analysing, whether you changed an 
optimisation option, whether you made a mistake, or whether it 
happened because you reversed two arguments?

The important thing is, that if foo was previously able to transform 
all possible exceptions into sensible values, it should also be able 
to do it now, after the change.

>> But I don't see why the "program" expression cannot be optimised.
>
>If you're willing to violate referentially transparency,
>you can certainly perform such optimizations.  But then you lose
>most of the nice properties of pure functional programming, like
>equational reasoning.

I am not willing to violate referential transparency (just yet). If I 
were, this discussion would not have become this long. Speaking of 
referential transparency: what is so referentially transparent about 
the Monadic approach:

getException x >>= (\v1 ->
getException x >>= (\v2 ->
return (v1 == v2)

Why question this? For the simple fact that "getException x" does not 
deliver the same value each time.

[snipping in previous quote]
>> 
>> Well, perhaps we are not thinking/talking about the same thing. I 
>> meant to say that the _handler_ always delivers the same expression 
>> for the same set of function arguments, independed of the actual 
>> exception it caught (i.e. independent of optimisation).
>
>I understood that.  But maybe you didn't understand my reply, which I
>admittedly did not explain very clearly.  The problem is that as well
>as exceptions, there is also nontermination, and the semantics for
>"catch" needs to deal with them both.
>
>> In that way, it becomes impossible to detect from the outside of the
>> function (Start above) what exception was throw. This is trivially so,
>> if the  handler does not get the exception value as an argument.
>
>You can't detect what exception was thrown, but "catch" can still be
>used to distinguish the order of evaluation, because you can detect the
>difference between throwing an exception and going into an infinite loop.
>If we have
>
>	foo :: Int
>	foo
>	    = bar
>	    catch _ = baz
>
>	bar = (1/0) + loop
>
>and the compiler evaluates the addition left-to-right, then "bar"
>will throw a DivideByZero exception, and so "foo" will return "baz",
>but if the compiler evaluates the addition right-to-left, then neither
>"foo" nor "bar" will terminate.

Well, luckily our programs only have to be referentially transparent 
if they terminate.

In practice, this is a non-issue.


Marco
(Variation on a theme: the proof of the program is in the programming)

>-- 
>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.
>
>
>_______________________________________________
>clean-list mailing list
>clean-list@cs.kun.nl
>http://www.cs.kun.nl/mailman/listinfo/clean-list