'any' and 'all' compared with the rest of the Report

Marko Schuetz marko@ki.informatik.uni-frankfurt.de
Fri, 26 Jan 2001 20:00:51 +0100


From: Jan-Willem Maessen <jmaessen@mit.edu>
Subject: Re: 'any' and 'all' compared with the rest of the Report
Date: Fri, 26 Jan 2001 12:26:17 -0500

> Marko Schuetz <MarkoSchuetz@web.de> starts an explanation of bottom
> vs. error with an assumption which I think is dangerous:
> > Assuming we want 
> > 
> > \forall s : bottom \le s
> > 
> > including s = error, then we should also have error \not\le
> > bottom.
> 
> He uses this, and an argument based on currying, to show that strict
> functions ought to force their arguments left to right.

I can't see where I did. I argued that distinguishing between error
and bottom seems to not leave much choice for bottom + error. 

[..]
> forever x = forever x  -- throughout.
> 
> addToForever :: Int -> Int
> addToForever b = forever () + b
> 
> main = print (addToForever (error "Bottom is naughty!"))
> 
> ==
> -- expanding the definition of +
> 
> addToForever b =
>   case forever () of
>   I# a# ->
>     case b of 
>     I# b# -> a# +# b#
> 
> ==
> -- At this point strictness analysis reveals that addToForever
> -- is strict in its argument.  As a result, we perform the worker-
> -- wrapper transformation:
> 
> addToForever b = 
>   case b of
>   I# b# -> addToForever_worker b#
> 
> addToForever_worker b# =
>   let b = I# b# 
>   in  case forever () of
>       I# a# ->
>         case b of 
>         I# b# -> a# +# b#
> 
> ==
> -- The semantics have changed---b will now be evaluated before
> -- forever(). 

Contextually, the original and the worker/wrapper versions do not
differ. I.e. there is no program into which the two could be inserted
which would detect a difference. So their semantics should be regarded
as equal.

> PS - Again, we don't try to recover from errors.  This is where the
> comparison with IEEE arithmetic breaks down: NaNs are specifically
> designed so you can _test_ for them and take action.  I'll also point
> out that infinities are _not_ exceptional values; they're semantically
> "at the same level" as regular floats---so the following comparison is
> a bit disingenuous:
> > If error \equiv bottom and you extend, say, Int with NaNs, how do you
> > implement arithmetic such that Infinity + Infinity \equiv Infinity and
> > Infinity/Infinity \equiv Invalid Operation?

Infinity was chosen as an example: from what you described I had the
impression the implementation needed to match on NaN constructors at
some point. Is this not the case?

Marko