On 9/14/06, [EMAIL PROTECTED] <[EMAIL PROTECTED]> wrote:
With this in mind the equations
1)  return _|_             == Return _|_
2)  _|_ `seq` (return _|_) == _|_
can be interpreted:
1) when reducing a return-redex (i.e. evaluating it), we get weak-head
normal form without evaluating the argument (which was _|_)
2) when reducing the `seq`-thing but not further evaluating the
arguments (_|_ in our case), we get nowhere (i.e. only _|_)

Thus, when evaluating the expressions (one step!, i.e. just to weak head
normal form), number 1) returns immediately but in 2), the `seq` needs
to evaluate its first argument. So the semantics of applying _|_ to a
function determines its behavior with respect to how much of its
arguments will be evaluated! I think this is the point our
misunderstanding is about?

For (evaluate :: a->IO a), I said something like
3)  evaluate _|_    == ThrowException
and meant, that when evaluating 3) one step to weak head normal form,
the argument does not get evaluated. 2) is much different to that.
Equation 3) is of course wrong and must be more like
    evaluate x == Evaluate x
where (Evaluate x) is a constructor but with a particular behavior when
executed in the IO-Monad.

Great, thank you!  I think this finally answers my question.

Mike
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to