
The GHC documentation says that (evaluate a) is not the same as (a `seq` return a). Can someone explain the difference to me, or point me to a place where it is explained? Mike

Michael Shulman wrote:
The GHC documentation says that (evaluate a) is not the same as (a `seq` return a). Can someone explain the difference to me, or point me to a place where it is explained?
(evaluate a) is "weaker" than (a `seq` return a). (a `seq` return a) is always _|_ whereas (evaluate a) is not _|_, but does throw an exception when executed. The appended code shows the differences. Regards, apfelmus import Prelude hiding (return,catch) import qualified Control.Monad as M import Control.Exception a = undefined :: () return = M.return :: a -> IO a e 0 = return a e 1 = a `seq` return a e 2 = evaluate a t x = e x >> return () -- t 0 == return () -- t 1 == throwIO something -- t 2 == throwIO something -- to check this, evaluate the expressions -- (t x >>= print) and (t x `seq` ()) u x = e x `seq` return () -- u 0 == return () -- u 1 == undefined -- u 2 == return () -- to check this, type (u x >>= print) into hugs/ghci v x = catch (e x) (\_ -> return ()) >>= print -- v 0 == throwIO something -- v 1 == print () -- v 2 == print ()

On 9/10/06, apfelmus@quantentunnel.de
The GHC documentation says that (evaluate a) is not the same as (a `seq` return a). Can someone explain the difference to me, or point me to a place where it is explained?
(evaluate a) is "weaker" than (a `seq` return a). (a `seq` return a) is always _|_ whereas (evaluate a) is not _|_, but does throw an exception when executed.
Okay... I think maybe I understand now. To check my understanding, is the following a correct description? * (return a) = produces an IO action which, when executed, returns a in the IO monad, but lazily evaluated. Thus, if a is undefined, it doesn't throw an exception unless and until its value is actually used. * (a `seq` return a) = evaluate a *right now*, then produce an IO action which, when executed, returns the result of evaluating a. Thus, if a is undefined, throws an exception right now. * (evaluate a) = produces an IO action which, when *executed*, evaluates a (not lazily) and returns the result in the IO monad. Thus, if a is undefined, throws an exception if and when the IO action in question is executed. If this is correct, then the way I would explain your examples is as follows. The "1" versions always throw an exception, since that happens when the function is first called.
e 0 = return a e 1 = a `seq` return a e 2 = evaluate a
t x = e x >> return () -- t 0 == return () -- t 1 == throwIO something -- t 2 == throwIO something
Here the IO action is executed, so 2 throws an exception; but its value is never used, so 0 doesn't.
u x = e x `seq` return () -- u 0 == return () -- u 1 == undefined -- u 2 == return ()
Here the IO action is never even executed, since it gets replaced with (return ()), so neither 0 nor 2 throws an exception.
v x = catch (e x) (\_ -> return ()) >>= print -- v 0 == throwIO something -- v 1 == print () -- v 2 == print ()
Here, again, the IO action is executed, so 2 throws an exception at that point, which gets caught and so the result is replaced with (). But 0 executes with no problem and returns a, lazily evaluated, which thereby slips out from under the `catch' to throw an error when its value is actually used, later, by `print'. Is that all correct? Thanks for your help! Mike

Hello Michael, you are correct. Only
* (a `seq` return a) = evaluate a *right now*, then produce an IO action which, when executed, returns the result of evaluating a. Thus, if a is undefined, throws an exception right now.
is a bit misleading as there is no evaluation "right now". It's better to say that (a `seq` return a) is _|_ ("bottom", i.e. undefined) when a == _|_. The subtle point is the difference between the action of throwing an exception (throw some_error :: IO a) and an undefined value (_|_). (throw ..) will cause your program to crash when "executed", but it's still a well defined value of type (IO a). For a more detailed semantics of exceptions in Haskell, see " Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell" http://research.microsoft.com/%7Esimonpj/Papers/marktoberdorf/ I further think (evaluate x) can be implemented as follows: evaluate x = catch (x `seq` return x) throw Regards, apfelmus

On 9/11/06, apfelmus@quantentunnel.de
* (a `seq` return a) = evaluate a *right now*, then produce an IO action which, when executed, returns the result of evaluating a. Thus, if a is undefined, throws an exception right now.
is a bit misleading as there is no evaluation "right now". It's better to say that (a `seq` return a) is _|_ ("bottom", i.e. undefined) when a == _|_.
Sure... but what about when a is not _|_? I would also like to understand the difference between `seq' and `evaluate' for arguments that are defined. How would you describe that without talking about "when" expressions are evaluated?
For a more detailed semantics of exceptions in Haskell, see " Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell" http://research.microsoft.com/%7Esimonpj/Papers/marktoberdorf/
Thanks; I will take a look at it! Mike

Michael Shulman wrote:
On 9/11/06, apfelmus@quantentunnel.de
wrote: * (a `seq` return a) = evaluate a *right now*, then produce an IO action which, when executed, returns the result of evaluating a. Thus, if a is undefined, throws an exception right now.
is a bit misleading as there is no evaluation "right now". It's better to say that (a `seq` return a) is _|_ ("bottom", i.e. undefined) when a == _|_.
Sure... but what about when a is not _|_? I would also like to understand the difference between `seq' and `evaluate' for arguments that are defined. How would you describe that without talking about "when" expressions are evaluated?
Ah well, the discussion goes about denotational semantics of Haskell. Unfortunately, I did not find a good introductory website about this. Personally, I found the explanation from Bird and Wadler's book about infinite lists very enlightening. The game roughly goes as follows: denotational semantics have been invented to explain what a recursive definition should be. I mean, thinking of functions as things that map (mathematical) sets on sets excludes self-referencing definitions (russell's paradox!). The solution is to think functions of as fixed points of an iterative process: factorial is the fixed point of (fac f) n = if n == 0 then 1 else n*f(n-1) what means (fac factorial) n == factorial n Now, the iterative process goes as follows: factorial_0 n = _|_ factorial_1 n = fac (factorial_0) n = if n == 0 then 1 else _|_ factorial_2 n = fac (factorial_1) n = case n of 0 -> 1 1 -> 1 _ -> _|_ and so on. Everytime, a more refined version of the ultimate goal factorial is created, on says that _|_ == factorial_0 <= factorial_1 <= factorial_2 <= ... (<= means "less or equal than") That's why _|_ is called "bottom" (it's the smalled thing in the hierarchy). This was about functions. In a lazy language, "normal" values can show a similar behavior. For instance, we have _|_ <= 1:_|_ <= 1:2:_|_ <= 1:2:3:_|_ <= ... <= [1..] That's how the infinite list [1..] is approximated. The inequalities follow from the fact that bottom is below everything and that all constructors (like (:)) are monotone (by definition), i.e. 1:x <= 1:y iff x <= y A function f is called *strict*, if it fulfills f _|_ = _|_ which means that it does not produce a constructor ("information") without knowing what its argument is. Back to your original question, we can now talk about functions in terms of _|_ and *data constructors*. As an example, we want to think about the meaning of (take 2 [1..]). What should this be? I mean, one argument is an infinite list! By tracing the definition of (take 2), one finds take 2 _|_ == _|_ -- (btw (take 2) is strict) take 2 (1:_|_) == 1:_|_ take 2 (1:(2:_|_)) == 1:(2:[]) take 2 (1:(2:(3:_|_))) == 1:(2:[]) and so on. The right and side remains equal for all further refinements, so we must conclude take 2 [1..] == 1:(2:[]). For the evaluate and `seq` problem, we simplify things by specializing the polymorphic type to ([Int] -> IO [Int]). Then, we introduce two constructors (ThrowException :: IO [Int]) and (Return :: IO [Int]) with the obvious meaning. The semantics of `seq` are now as following: _|_ `seq` x == _|_ [] `seq` x == x (y:ys) `seq` x == x So `seq` forces its first argument. When we define f x = x `seq` (Return x) we thereby get f _|_ == _|_ f [] == Return [] f (x:xs) == Return (x:xs) To compare, the semantics of (evaluate) is evaluate _|_ == ThrowException =/= _|_ evaluate [] == Return [] evaluate (x:xs) == Return (x:xs) That should answer your question. Please note that this answer is actually a lie, as functions must be monotone (halting problem, fix id == _|_), but (evaluate) is not: _|_ <= [] yet evaluate _|_ == ThrowException = evaluate [] == Return [] This can be fixed by departing from denotational semantics and giving all (IO a)-things an operational meaning. Further explanations and further references are found in the paper I pointed out last time. Regards, apfelmus

On 9/13/06, apfelmus@quantentunnel.de
So `seq` forces its first argument. When we define f x = x `seq` (Return x) we thereby get f _|_ == _|_ f [] == Return [] f (x:xs) == Return (x:xs) To compare, the semantics of (evaluate) is evaluate _|_ == ThrowException =/= _|_ evaluate [] == Return [] evaluate (x:xs) == Return (x:xs) That should answer your question.
I must not be phrasing my question very well; I feel like we're talking past each other. It seems to me that when writing actual programs (rather than reasoning about denotational semantics) the reason one would use `seq' or `evaluate' is to force something to be evaluated "now" rather than "later", i.e. to get around Haskell's default lazy execution. Your semantics say that (x `seq` return x) and (evaluate x) have the same result when x is anything other than _|_. All well and good, but (return x) *also* has those same results when x is not _|_. Why would one use the former two rather than (return x), if x is known not to be _|_? Because they evaluate x at different "times", right? Even though the eventual return value is the same, and thus the *semantics* are the same. So laying aside the formal semantics, what is the difference in terms of actual, real, Haskell programs? Mike

Michael Shulman wrote:
On 9/13/06, apfelmus@quantentunnel.de
wrote: So `seq` forces its first argument. When we define f x = x `seq` (Return x) we thereby get f _|_ == _|_ f [] == Return [] f (x:xs) == Return (x:xs) To compare, the semantics of (evaluate) is evaluate _|_ == ThrowException =/= _|_ evaluate [] == Return [] evaluate (x:xs) == Return (x:xs) That should answer your question.
I must not be phrasing my question very well; I feel like we're talking past each other. It seems to me that when writing actual programs (rather than reasoning about denotational semantics) the reason one would use `seq' or `evaluate' is to force something to be evaluated "now" rather than "later", i.e. to get around Haskell's default lazy execution.
Your semantics say that (x `seq` return x) and (evaluate x) have the same result when x is anything other than _|_. All well and good, but (return x) *also* has those same results when x is not _|_. Why would one use the former two rather than (return x), if x is known not to be _|_? Because they evaluate x at different "times", right? Even though the eventual return value is the same, and thus the *semantics* are the same. So laying aside the formal semantics, what is the difference in terms of actual, real, Haskell programs?
You are right, I completely forgot that executing a real Haskell program is a graph reduction and that `seq`'s purpose is to control this reduction and associated memory usage. But it's possible to use denotational semantics as an approximation to the actual graph reduction. To achieve that, we think of _|_ as an *unevaluated expression*, i.e. something that is not a constructor like (:) or [] in weak head normal form. This is different from interpreting _|_ as "divergent program" and coincides with the denotational view that _|_ is a value we don't know anything about. So to speak, when executing a program which evaluates the list [1..3], the evaluation steps proceed as follows: _|_ , 1:_|_, 1:(2:_|_), 1:(2:(3:_|_)) and finally 1:(2:(3:[])) In different terms, one might say that a notation like (1:_|_) is a shorthand for the set of all possible lists that start with 1. The task of a program is to select a single one out of these by narrowing down the possible sets. This is the intuition behind why every function must be monotone (so for example _|_ <= 1:_|_ implies f (_|_) <= f (1:_|_) and <= is interpreted the way that larger sets are <= smaller sets). 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. Note that `seq` and evaluate only force weak head normal form, so evaluate (1:undefined) >>= print . head will not rise an exception. Regards, apfelmus

On Sep 14, 2006, at 16:20 , apfelmus@quantentunnel.de wrote:
Michael Shulman wrote:
On 9/13/06, apfelmus@quantentunnel.de
wrote: So `seq` forces its first argument. When we define f x = x `seq` (Return x) we thereby get f _|_ == _|_ f [] == Return [] f (x:xs) == Return (x:xs) To compare, the semantics of (evaluate) is evaluate _|_ == ThrowException =/= _|_ evaluate [] == Return [] evaluate (x:xs) == Return (x:xs) That should answer your question.
I must not be phrasing my question very well; I feel like we're talking past each other. It seems to me that when writing actual programs (rather than reasoning about denotational semantics) the reason one would use `seq' or `evaluate' is to force something to be evaluated "now" rather than "later", i.e. to get around Haskell's default lazy execution.
Your semantics say that (x `seq` return x) and (evaluate x) have the same result when x is anything other than _|_. All well and good, but (return x) *also* has those same results when x is not _|_. Why would one use the former two rather than (return x), if x is known not to be _|_? Because they evaluate x at different "times", right? Even though the eventual return value is the same, and thus the *semantics* are the same. So laying aside the formal semantics, what is the difference in terms of actual, real, Haskell programs?
You are right, I completely forgot that executing a real Haskell program is a graph reduction and that `seq`'s purpose is to control this reduction and associated memory usage. But it's possible to use denotational semantics as an approximation to the actual graph reduction.
No, you were right the first time. :) The denotational semantics is the important one. Haskell can be executed by other means than graph reduction. (That's why the report says a "non-strict" rather than "lazy" language.) Peculiar language constructs may allow you to tell the difference, but then they are highly dubious (and like all dubious things, they should be in the IO monad :) ). -- Lennart

Lennart Augustsson wrote:
No, you were right the first time. :) The denotational semantics is the important one. Haskell can be executed by other means than graph reduction. (That's why the report says a "non-strict" rather than "lazy" language.) Peculiar language constructs may allow you to tell the difference, but then they are highly dubious (and like all dubious things, they should be in the IO monad :) ).
You suggest that (evaluate) or something else actually can tell me the difference? That would be interesting. And what alternatives (besides call by name without sharing) are there? I always think lazy evaluation is space and time optimal. Regards, apfelmus

apfelmus@quantentunnel.de wrote:
And what alternatives (besides call by name without sharing) are there?
http://doi.acm.org/10.1145/944705.944731 http://doi.acm.org/10.1145/581690.581694
I always think lazy evaluation is space and time optimal.
Google for "optimal reduction" (Lamping, Asperti, Guerrini, ...). Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

No, I wasn't suggesting that evaluate can tell the difference, just that you can add dubious "functions". You can evaluate with eager evaluation and some kind of threads+fair scheduler. Both pH and the (short lived) Eager Haskell version of ghc did this. (Well, I'm not sure pH ever got the fair scheduler.) -- Lennart On Sep 15, 2006, at 05:00 , apfelmus@quantentunnel.de wrote:
Lennart Augustsson wrote:
No, you were right the first time. :) The denotational semantics is the important one. Haskell can be executed by other means than graph reduction. (That's why the report says a "non-strict" rather than "lazy" language.) Peculiar language constructs may allow you to tell the difference, but then they are highly dubious (and like all dubious things, they should be in the IO monad :) ).
You suggest that (evaluate) or something else actually can tell me the difference? That would be interesting.
And what alternatives (besides call by name without sharing) are there? I always think lazy evaluation is space and time optimal.
Regards, apfelmus
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Sorry, it is of course Jan-Willem's compiler that is called Eager Haskell, the Ghc version was called optimistic Haskell. There's also the old precursor to these, the Optimistic G-machine, that performs some non-lazy computations. (And it can even do them while garbage collecting!) -- Lennart On Sep 15, 2006, at 07:59 , Lennart Augustsson wrote:
No, I wasn't suggesting that evaluate can tell the difference, just that you can add dubious "functions".
You can evaluate with eager evaluation and some kind of threads +fair scheduler. Both pH and the (short lived) Eager Haskell version of ghc did this. (Well, I'm not sure pH ever got the fair scheduler.)
-- Lennart
On Sep 15, 2006, at 05:00 , apfelmus@quantentunnel.de wrote:
Lennart Augustsson wrote:
No, you were right the first time. :) The denotational semantics is the important one. Haskell can be executed by other means than graph reduction. (That's why the report says a "non-strict" rather than "lazy" language.) Peculiar language constructs may allow you to tell the difference, but then they are highly dubious (and like all dubious things, they should be in the IO monad :) ).
You suggest that (evaluate) or something else actually can tell me the difference? That would be interesting.
And what alternatives (besides call by name without sharing) are there? I always think lazy evaluation is space and time optimal.
Regards, apfelmus
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On 9/14/06, apfelmus@quantentunnel.de
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
participants (4)
-
apfelmus@quantentunnel.de
-
Janis Voigtlaender
-
Lennart Augustsson
-
Michael Shulman