[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:

[snip]

>> >	foo :: Int
>> >	foo
>> >	    = bar
>> >	    catch DivideByZero = baz

[snip]
>
>Suppose the expression "a + b" occurs in the definition of "bar".
>I can't safely apply equational reasoning to replace this with "b + a",
>because that might change the value returned from foo.
>
>Or, if we consider a slightly different example,
>where foo takes a parameter x,
>
>	foo :: Int -> Int
>	foo x
>	    = bar x
>	    catch DivideByZero = baz x
>
>you may have "foo (a + b)" being different than "foo (b + a)".

Ah, of course: laziness. How stupid of me (and I do use it all the 
time, in many ways...). My apologies.

Still: I REALLY do not like the Monadic solution. Sorry about that 
too, but that is something I cannot help. This is NOT a Monad thing 
in particular: I wouldn't like a "Unique World" solution either.

Now there are a few things worth considering (in order of preference):

* use something else than stack trimming. For _handling_ exceptions 
it is not that important that things go blazingly fast. However, I am 
afraid that things like (a) defining an order over exceptions and 
delivering the largest or (b) delivering the complete set of 
exceptions are no serious options either. At this moment, I cannot 
oversee what it would do to ordinary execution, but I am sure that 
you (Fergus) have looked into this.

* Last resort solution: basically, allow only a single exception 
type, so that handlers cannot detect what hit them. Useful for some 
things, but not all.

* Hurt referential transparency. Hmmmm. The only thing that is worse is:

* Use another programming language.

Now that I have admitted defeat, there is more (yes there is)... 
Please keep in mind: I am not defending lack of referential 
transparency 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.
>
>That's not the only thing which is not possible, in general.
>You also can't easily specialize occurrences of foo.
>That's not important for that original example,
>but consider another slight variation:
>
>	foo :: Int -> Int -> Int
>	foo f
>	    = bar f
>	    catch DivideByZero = baz f
>
>If "bar" calls "f" often, and there is a call to "foo (\ x y -> x + y)",
>then it may be very important for performance to specialize both
>"foo" and "bar", so that the calls to f can be inlined to a single
>cheap add instruction rather than the expensive sequence of instructions
>needed for a call to an unknown higher-order function term.

Yes, but actually I would not start being concerned about the 
efficiency of functions that contain exception handlers. I think the 
"efficiency" remarks take away the attention from the more 
fundamental issues. The more because it remains to be seen how often 
the example above appears in practice.

I do agree however that the exception mechanism should not affect 
ordinary evaluation (badly). With this, I mean evaluation that does 
not in any way goes through a function with a handler.

>Well, I suppose the compiler could do the specialization, provided that it
>was done _after_ any optimizations that change the order of evaluation.
>But normally the compiler should do such specializations first, and then
>apply all the other optimizations, such as inlining, constant propagation,
>etc., so that the specialized code can be simplified.
>
>> 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.
>
>"getException x" always evaluates to the same value, an IO action.

Yes, I know. But that does not help reasoning about the value you get 
back. That's what I mean if I say that the proof of the program is in 
the programming. The syntax above is equivalent to:

v1 = getException(x);
v2 = getException(x);
return v1 == v2;

In terms of the official semantics, this may be referential 
transparant. In terms of what the programmer sees and experiences, it 
is not. THAT is something that I do not like at all.

>When you talk about "delivering" a value, you mean applying this action
>to some particular world state to get a concrete value rather than
>an IO action.  If you apply the action to two different states then
>naturally you may get different values delivered.  That is the case in
>your example above.
>
>> >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.
>
>If the compiler transforms a terminating program into a non-terminating
>one, that is usually considered to be a rather serious issue :)

Do you call this a terminating program? That's indeed a rather 
serious issue :-)

In the lamda calculus, there are no exceptions. Just diverging 
computations. If you have written such a program, it already _is_ 
officially non-terminating. It just happens that the system is nice 
enough to sometimes catch one of these and tell you.

And it does not really matter whether the compiler makes it 
non-terminating, or some non-determism monad at runtime. It is not 
like the Monadic approach will spare you from non-termination. This 
program is a recipe for disaster. It's a deceased program. If you 
were a hired programmer, you'd be lucky if your boss does not find 
out. That's why it is a non-issue.

Now I come to think of it... I could hide behind the argument that if 
foo(a + b) <> foo(b + a) that this was caused by a diverging 
computation that the system happened to catch. And, as lamda calculus 
does not guarantee _anything_ about diverging expressions, the 
exception handler can do anything it likes (call abort, for example).

But that is kind of, how do you say,... a red herring?



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