Re: State monads don't respect the monad laws in Haskell
Dylan Thurston <dpt@lotus.bostoncoop.net> writes:
I don't think this is necessarily wise to drop this from the report altogether. To me, it seems comparable to associativity of addition for instances of Num; many instances don't satisfy it (e.g., Float), but it's a useful guideline to keep in mind.
I've often been bothered by the inconsistent treatment of laws in the report; why are there laws for functors, monads, and quot/rem and div/mod, and not much else? I'm pleased to see that the laws that are given actually do have exceptions.
Chalk me up as someone in favor of laws without exceptions. Allow me for a moment to make a reductio argument: We should just make Haskell into a strict language. Our equational laws still hold 95% of the time---after all, we don't really write non-terminating computations that often, and that's where the laws break down. And gosh darn, we sure get an efficient implementation. Of course, this argument doesn't really work out for the Haskell constructs we know and love (monadic computations spring to mind given the present conversation, along with certain uses of parsing combinators, but I bet you can think of your own examples). Having spent several years working with versions of Haskell with weakened equational semantics, I have become a bit of a reactionary on this point. Sort-of equational semantics just aren't powerful enough for many applications---we spend our time mired in the corner cases (such as non-termination), which is exactly what we were trying to avoid by using Haskell in the first place. I can't stress that enough. Freedom from crazy corner cases is Haskell's big selling point. None of this "except for infinite computations" stuff. None of this "as long as f has no side effects". If I have to worry about corner cases, I'm probably better off adding type classes and beautiful syntax to OCaml. That said, "seq" is a big wart on Haskell to begin with. I might be willing to allow "nice" rules like the monad laws to apply *as long as the results are not passed (directly or indirectly) to seq*. But I'm not willing to go from "the IO monad disobeys the laws in the presence of seq, and that might be OK" to "my monad disobeys the laws in code that never uses seq, and that's OK because even IO breaks the monad laws". And I'd really much rather we cleaned up the semantics of seq---or better yet, fixed the problems with lazy evaluation which make seq necessary in the first place. [Let me be clear: I believe hybrid eager/lazy evaluation, the subject of my dissertation, does eliminate the need for seq in most cases---so I'm a bit biased here.] -Jan-Willem Maessen
On 2002-05-14T12:32:30-0400, Jan-Willem Maessen wrote:
And I'd really much rather we cleaned up the semantics of seq---or better yet, fixed the problems with lazy evaluation which make seq necessary in the first place.
A general question: What is seq useful for, other than efficiency? -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig QUIET! Do you smell something?
It's useful for: debug :: Show a => a -> a debug x = unsafePerformIO (hPutStrLn stderr (show x)) `seq` x (Presumably "trace" is defined similarly) One may ask the question: what is seq useful for not in conjunction with unsafePerformIO, other than efficiency. That, I don't know the answer to. - Hal -- Hal Daume III "Computer science is no more about computers | hdaume@isi.edu than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume On Tue, 14 May 2002, Ken Shan wrote:
On 2002-05-14T12:32:30-0400, Jan-Willem Maessen wrote:
And I'd really much rather we cleaned up the semantics of seq---or better yet, fixed the problems with lazy evaluation which make seq necessary in the first place.
A general question: What is seq useful for, other than efficiency?
-- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig QUIET! Do you smell something?
One may ask the question: what is seq useful for not in conjunction with unsafePerformIO, other than efficiency. That, I don't know the answer to.
Here is an example.
main::IO() main=do time1 <- getCPUTime w <- return $! calcSomething time2 <- getCPUTime ...
J.A.
hello, this is misleading. seq only evaluates to whnf, i.e. the outermost lazy constructor (or lambda) and that only if the "seq ..." expression is actually evaluated, which is often tricky to ensure. furthermore, for non-functions one can get the same behaviour, by using a case with a pattern. here is why i think the example does not illustrate what is seq good for:
main::IO() main=do time1 <- getCPUTime w <- return $! map undefined [1..] time2 <- getCPUTime ....
the above computation does not take very long. bye iavor Jorge Adriano wrote:
One may ask the question: what is seq useful for not in conjunction with unsafePerformIO, other than efficiency. That, I don't know the answer to.
Here is an example.
main::IO() main=do time1 <- getCPUTime w <- return $! calcSomething time2 <- getCPUTime
...
J.A.
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
-- ================================================== | Iavor S. Diatchki, Ph.D. student | | Department of Computer Science and Engineering | | School of OGI at OHSU | | http://www.cse.ogi.edu/~diatchki | ==================================================
True, but using seq you can define deepSeq/rnf (depening on which camp you're from), which isn't misleading in this way. -- Hal Daume III "Computer science is no more about computers | hdaume@isi.edu than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume On Tue, 14 May 2002, Iavor S. Diatchki wrote:
hello,
this is misleading. seq only evaluates to whnf, i.e. the outermost lazy constructor (or lambda) and that only if the "seq ..." expression is actually evaluated, which is often tricky to ensure. furthermore, for non-functions one can get the same behaviour, by using a case with a pattern.
here is why i think the example does not illustrate what is seq good for:
main::IO() main=do time1 <- getCPUTime w <- return $! map undefined [1..] time2 <- getCPUTime ....
the above computation does not take very long.
bye iavor
Jorge Adriano wrote:
One may ask the question: what is seq useful for not in conjunction with unsafePerformIO, other than efficiency. That, I don't know the answer to.
Here is an example.
main::IO() main=do time1 <- getCPUTime w <- return $! calcSomething time2 <- getCPUTime
...
J.A.
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
-- ================================================== | Iavor S. Diatchki, Ph.D. student | | Department of Computer Science and Engineering | | School of OGI at OHSU | | http://www.cse.ogi.edu/~diatchki | ==================================================
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Hal Daume <hdaume@ISI.EDU> writes:
[seq is] useful for:
debug :: Show a => a -> a debug x = unsafePerformIO (hPutStrLn stderr (show x)) `seq` x
(Presumably "trace" is defined similarly)
One may ask the question: what is seq useful for not in conjunction with unsafePerformIO, other than efficiency. That, I don't know the answer to.
Of course, this can be defined without seq:
debug :: Show a => a -> a debug x = unsafePerformIO (hPutStrLn stderr (show x) >> return x)
-- Alastair Reid Reid Consulting (UK) Ltd
On Tue, 14 May 2002, Ken Shan wrote:
On 2002-05-14T12:32:30-0400, Jan-Willem Maessen wrote:
And I'd really much rather we cleaned up the semantics of seq---or better yet, fixed the problems with lazy evaluation which make seq necessary in the first place.
A general question: What is seq useful for, other than efficiency?
seq can create a new, strict definition of a function from an existing non-strict function. const a = \_ -> a (const nonstrict in second arg) strict_const a b = seq b (const a b) strict_const now strict in second arg, even though it doesnt use arg. I believe the strictness properties of functions in haskell and program-execution-flow are very much intertwined, as in one defines the other. This seems like a simple concept, and I know of no real proof, but I think the idea is worth considering. I have found that functions can be classified three ways (for some given argument to the function) I will use the first argument for simplicity. Strict: 1. For all values x for all of v_1 ... v_n , f _|_ v_1 ... v_n = _|_ Conditionally-Strict: 2. There exists a value x for v_i (1<=i<=n) such that when v_i =x f _|_ v_1 ... v_i .. vn = _|_ but it is not the case that f is "strict" (in the argument in question). Lazy: 3. There exists no value x for v_i (1<=i<=n) such that f _|_ v1 .. vn = _|_ When there is only one argument, the cases are wittled down to case one and case three, or strict versis nonstrict. When f _|_ a = _|_ for some a, that means when f is reduced, f causes some reduction in the first argument of f. For the third case, f doesn't cause any reduction in the first argument. Most functions I believe are in case two, or conditionally strict in some argument. here's an example. lets define a simplified "take" function take 0 _ = [] take n (x:xs) = x :take (n-1) xs Prelude> take 0 undefined :: [Int] [] Prelude> take 1 undefined :: [Int] *** Exception: Prelude.undefined It just so happens that take is not strict in the second argument when the first argument happens to be zero. we can fix this with seq (or perhaps by redefining take just a tad so it pattern matches on the list or something) take' 0 [] = [] take' 0 xs = [] take' n (x:xs) = x:take' (n-1) xs take'' n l = seq l (take n l) so now then Main> take' 0 undefined :: [Int] *** Exception: Prelude.undefined Main> take'' 0 undefined :: [Int] *** Exception: Prelude.undefined /**Aside: but did I really fix take''? that is, are take' and take'' the same? Main> take' 1 (9:undefined) *** Exception: Prelude.undefined Main> take'' 1 (9:undefined) [9] No. an almost equivalant definition to take could be. take'' 0 [] = [] take'' 0 xs = [] take'' n (x:xs) = x:take (n-1) xs ^^notice the use of "take" instead of "take''" !! **/ So what have I done? With strict_const, I took a lazy function and made it strict. with take'', I took a conditionally strict function and made it strict. all with the simple application of seq. I also changed the order of evaluation for the application of both functions, obviously. I hope I have shown some evidence of why I think my conjecture is correct. Why does it matter if my conjecture is correct and what does it have to do with this thread? I'm sure it has something to do with it, but my head hurts trying to think of it. Seq has to do with changing the order of operations, which I'm trying to say also changes strictness properties. Ugh. I swear they're all related somehow, I just can't grasp all of it at the moment. Appologies if my message seems rather incoherent. I thought about not sending it but I also thought there was enough useful info (for somebody) that it might just be worth posting. I am not a researcher, so take this message with usual dosage of salt. Cheers, Jay Cox
I watched with interest the discussion about the ravages of `seq`. In the old days, we protected uses of `seq` with a type class, to keep it at bay. There was no function instance (so no problem with the state monads, or lifting of functions in general), and the type class prevented interference with foldr/build. However... In defining Haskell 98 we made a conscious decision not to guard `seq` with a type class. The reasoning was as follows: + Space control is an important phase of programming, and `seq` provides a powerful mechanism for tweaking a program, to improve its space behavior. It should therefore be as easy as possible to experiment with adding `seq` in various places, including on function closures. - Haskell already had somewhat muddied semantics for types (both sums and products are lifted, and bottom is present in every type). It seemed as though a little more muddying was not a serious affair. Did we make the right decision? For Haskell 98: Yes. And I believe we made it with our eyes open. Will the next version of Haskell have something better. I hope so, but I fear not. First, I don't see much active research on what Haskell would look like with true unpointed types -- there are lots of practical issues to be addressed; second, the prevalence of things like unsafePerformIO (slogan: USPIO is NOT Haskell) seems to be growing, not diminishing, and again I don't see much active research on how to gain its benefits while containing its damage. True declarative programming is a delicate flower. Review the history of the 80's and early 90's. It was the conviction of the Lazy FP community to true declarativeness that led us all to reject proposal after proposal for state and efficient arrays, until finally Eugenio and Phil led us to the land of monads. Finally, as a result of the burning need we all felt, and of the high standards we all demanded, we could be as imperative as the best of them, without compromising the mathematical nature of the language. If this history teaches us anything, it should urge us all, and the new young blood in particular, not to go for quick fixes, or to compromise on the dream of a truly declarative language. Haskell 98 is a great language. The best on the planet today. But it's not perfection. Let's confront the problems face to face, and find the right way forward! John
And I'd really much rather we cleaned up the semantics of seq---or better yet, fixed the problems with lazy evaluation which make seq necessary in the first place.
A general question: What is seq useful for, other than efficiency?
seq can create a new, strict definition of a function from an existing non-strict function.
John Launchbury wrote:
I watched with interest the discussion about the ravages of `seq`.
In the old days, we protected uses of `seq` with a type class, to keep it at bay. There was no function instance (so no problem with the state monads, or lifting of functions in general), and the type class prevented interference with foldr/build. ...
Just a further remark: During discussion with Olaf about consequences of `seq` for foldr/build, respectively his type-inference based deforestation, I had the impression that there could very well be a function instance for `seq` not interfering with shortcut deforestation, provided this instance is restricted in the following way: class Eval a where seq :: a -> b -> b instance Eval d => Eval (c -> d) I have no idea what would be a semantic justification for this instance declaration, except that it allows use of `seq` on at least some function types, but seems to outlaw all the critical cases where use of `seq` falsifies the foldr/build-rule. -- Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de
Yes. Let me be clear. It is not the fact that `seq` operates on functions that breaks foldr/build: it is the fact that `seq` claims to be parametrically polymorphic when in fact it is not. The parametricity result is weakened to the point that the foldr/build proof no longer applies, and a counter example can be constructed, viz. head = foldr const undefined one = build (\c n -> n `seq` c 1 n) result = head one The one definition looks fine as the body to build is sufficiently polymorphic, but that only because `seq` is lying. John
I watched with interest the discussion about the ravages of `seq`.
In the old days, we protected uses of `seq` with a type class, to keep it at bay. There was no function instance (so no problem with the state monads, or lifting of functions in general), and the type class prevented interference with foldr/build. ...
Just a further remark: During discussion with Olaf about consequences of `seq` for foldr/build, respectively his type-inference based deforestation, I had the impression that there could very well be a function instance for `seq` not interfering with shortcut deforestation, provided this instance is restricted in the following way:
class Eval a where seq :: a -> b -> b
instance Eval d => Eval (c -> d)
I have no idea what would be a semantic justification for this instance declaration, except that it allows use of `seq` on at least some function types, but seems to outlaw all the critical cases where use of `seq` falsifies the foldr/build-rule.
-- Janis Voigtlaender
On Tue, May 14, 2002 at 12:32:30PM -0400, Jan-Willem Maessen wrote:
Chalk me up as someone in favor of laws without exceptions.
Do you ever use floating point addition? I rarely use floating point, but it is sometimes more useful than the alternatives, as long as you bear in mind its limitations. In general, programmers should be allowed to do unsafe things, as long as they explicitly ask for it (by, say, using floating point). I guess these monad laws are not such a case. I'm very interested by your ideas to make Haskell better behaved:
... That said, "seq" is a big wart on Haskell to begin with. I might be willing to allow "nice" rules like the monad laws to apply *as long as the results are not passed (directly or indirectly) to seq*. But I'm not willing to go from "the IO monad disobeys the laws in the presence of seq, and that might be OK" to "my monad disobeys the laws in code that never uses seq, and that's OK because even IO breaks the monad laws". And I'd really much rather we cleaned up the semantics of seq---or better yet, fixed the problems with lazy evaluation which make seq necessary in the first place. [Let me be clear: I believe hybrid eager/lazy evaluation, the subject of my dissertation, does eliminate the need for seq in most cases---so I'm a bit biased here.]
This sounds very interesting! Is your dissertation available? My main complaint about Haskell at the moment is that it seems remarkably difficult to avoid space leaks due to laziness issues; your approach seems like a promising way to avoid that. Best, Dylan Thurston
participants (10)
-
Alastair Reid -
Dylan Thurston -
Hal Daume III -
Iavor S. Diatchki -
Jan-Willem Maessen -
Janis Voigtlaender -
Jay Cox -
John Launchbury -
Jorge Adriano -
Ken Shan