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

26 Jan 2001


      From: Jan-Willem Maessen 
Subject: Re: 'any' and 'all' compared with the rest of the Report
Date: Fri, 26 Jan 2001 12:26:17 -0500
...
Marko Schuetz  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