Re: [Haskell-cafe] Re: evaluate vs seq
[EMAIL PROTECTED] 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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: evaluate vs seq
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 , [EMAIL PROTECTED] 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
Re: [Haskell-cafe] Re: evaluate vs seq
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 , [EMAIL PROTECTED] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: evaluate vs seq
On Sep 14, 2006, at 16:20 , [EMAIL PROTECTED] wrote: Michael Shulman wrote: On 9/13/06, [EMAIL PROTECTED] [EMAIL PROTECTED] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: evaluate vs seq
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
[Haskell-cafe] Re: evaluate vs seq
Michael Shulman wrote: On 9/11/06, [EMAIL PROTECTED] [EMAIL PROTECTED] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: evaluate vs seq
On 9/13/06, [EMAIL PROTECTED] [EMAIL PROTECTED] 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? Mike ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: evaluate vs seq
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: evaluate vs seq
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 () ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: evaluate vs seq
On 9/10/06, [EMAIL PROTECTED] [EMAIL PROTECTED] 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. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
