State monads don't respect the monad laws in Haskell
Simon Marlow
wondering about issues to do with exceptions in the IO monad (see
discussion on glasgow-ha...@haskell.org if you're interested).
The question we were considering was whether the following should hold
in the IO monad:
(return () >>= \_ -> undefined) `seq` 42 == undefined
as we understand the IO monad it certainly shouldn't be the case. But
according to the monad laws:
(law) return a >>= k == k a
so (return () >>= \_ -> undefined) `seq` 42
=> ((\_ -> undefined) ()) `seq` 42
=> undefined `seq` 42
=> undefined
So the IO monad in Haskell, at least as we understand it, doesn't
satisfy the monad laws (or, depending on your point of view, seq breaks
the monad laws).
This discrepancy applies to any state monad. Suppose we define
return a = \s -> (s, a)
m >>= k = \s -> case m s of (s', a) -> k a s'
now
return a >>= k
=> \s -> case (return a) s of (s', a') -> k a' s'
=> \s -> case (s, a) of (s', a') -> k a' s'
=> \s -> k a s
but (\s -> k a s) /= (k a) in Haskell, because seq can
tell the difference.
What should the report say about this?
Cheers,
Simon
_______________________________________________
Haskell mailing list
Has...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
David Feuer
> An interesting revelation just occurred to Simon P.J. and myself while
> wondering about issues to do with exceptions in the IO monad (see
> discussion on glasgow-ha...@haskell.org if you're interested).
>
> The question we were considering was whether the following should hold
> in the IO monad:
>
> (return () >>= \_ -> undefined) `seq` 42 == undefined
>
> as we understand the IO monad it certainly shouldn't be the case. But
Why shouldn't this be the case? It seems kind of obvious.
> So the IO monad in Haskell, at least as we understand it, doesn't
> satisfy the monad laws (or, depending on your point of view, seq breaks
> the monad laws).
>
> This discrepancy applies to any state monad. Suppose we define
>
> return a = \s -> (s, a)
> m >>= k = \s -> case m s of (s', a) -> k a s'
>
> now
> return a >>= k
> => \s -> case (return a) s of (s', a') -> k a' s'
> => \s -> case (s, a) of (s', a') -> k a' s'
> => \s -> k a s
>
> but (\s -> k a s) /= (k a) in Haskell, because seq can
> tell the difference.
>
> What should the report say about this?
"Changes from Haskell 98: removed the seq primitive."
Well, maybe not. But it would be really nice to find an alternative
that didn't screw up so many different things. It seems that general
cleanliness is more important for understanding programs than being able
to use functions in all the same ways as datatypes (yes, I am aware that
there are loads of issues regarding this that I don't understand, but
the whole seq thing smells really funny. \a->\b->e should really equal
\a b->e, \x->f x should equal f, etc. etc. Sometimes it seems as though
every rule in Haskell has a list of exceptions relating to seq, and that
sucks.)
--
Night. An owl flies o'er rooftops. The moon sheds its soft light upon
the trees.
David Feuer
Ross Paterson
> The question we were considering was whether the following should hold
> in the IO monad:
>
> (return () >>= \_ -> undefined) `seq` 42 == undefined
>
>
> This discrepancy applies to any state monad.
It also fails for the reader, writer and continuation monads, also thanks
to lifted functions and tuples. The right-identity law also fails for
these monads:
(undefined >>= return) `seq` 42 /= undefined `seq` 42
George Russell
[snip]
> So the IO monad in Haskell, at least as we understand it, doesn't
> satisfy the monad laws (or, depending on your point of view, seq breaks
> the monad laws).
Cheers Simon. One of the awkward things about the Haskell events I implemented
is that although I make them an instance of Monad, they don't actually satisfy
left identity. Now I can say that "Yes, Event isn't really a Monad, but neither is IO".
According to the report
> Instances of Monad should satisfy the following laws:
>
> return a >>= k = k a
> m >>= return = m
> m >>= (\x -> k x >>= h) = (m >>= k) >>= h
so neither IO nor my events satisfy this. Up to now I haven't had any problems
with this.
Does GHC or any other Haskell compiler actually rely on instances of Monad
satisfying left identity? If not, I would suggest dropping the requirement, if it
can be done without upsetting category theorists. (What the hell, they stole the
term "Monad" from philosophy and changed its meaning, so why shouldn't we?)
I presume it would not in fact be difficult to synthesise a left identity at
the cost of making things slower, thus (forgive any syntax errors, I'm not going to
test this).
data MonadIO a = Action (IO a) | Return a
instance Monad (MonadIO a) where
return a = Return a
(>>=) (Return a) k = k a
(>>=) (Action act) f =
Action (act >>= (\ a -> case f a of {Return a -> return a;Action act -> act}))
(I considered doing something similar to turn Events into a real monad, but decided to
choose efficiency over category theory. For events its slightly more complicated as
you need to handle the choice operator as well.)
Dylan Thurston
> According to the report
> > Instances of Monad should satisfy the following laws:
> >
> > return a >>= k = k
> > m >>= (\x -> k x >>= h) = (m >>= k) >>= h
> so neither IO nor my events satisfy this. Up to now I haven't had
> any problems with this.
> Does GHC or any other Haskell compiler actually rely on instances of
> Monad satisfying left identity? If not, I would suggest dropping
> the requirement, if it can be done without upsetting category
> theorists. (What the hell, they stole the term "Monad" from
> philosophy and changed its meaning, so why shouldn't we?)
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.
--Dylan
George Russell
[snip]
> 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.
Even the quot/rem and div/mod laws are not always true, for example if you
divide by zero, or (for div/mod, where overflows cause an error) where
you get an overflow with (x `div` y) * y. Perhaps we need something in the
report to state that these laws like these and the Monad laws are only intended
as aspirations rather than promises.
S.M.Kahrs
[snip]
> I presume it would not in fact be difficult to synthesise a left identi=
ty at
> the cost of making things slower, thus (forgive any syntax errors, I'm =
not going to
> test this).
> data MonadIO a = Action (IO a) | Return a
> instance Monad (MonadIO a) where
> return a = Return a
> (>>=) (Return a) k = k a
> (>>=) (Action act) f = =
> Action (act >>= (\ a -> case f a of {Return a -> return a;Actio=
n act -> act}))
Or, more general:
data MonadWrap m a = M (m a) | R a
instance Monad m => Monad (MonadWrap m) where
return = R
R x >>= f = f x
M x >>= f = M (x >>= \a->case f a of
R b -> return b
M c -> c)
I don't think this really solves the problem with the left unit
(not in general, and not for IO either),
it merely pushes it to a different place.
I think you need the left-unit law for monad m
to prove the 'associativity' law for monad (MonadWrap m)
The 'associativity' law:
m >>= (\x -> k x >>= h) = (m >>= k) >>= h
The case in which the situation occurs is m=(M x) with (k x)=(R b).
Stefan Kahrs
Jan-Willem Maessen
> 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.
>
> 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
George Russell
[snip]
> I don't think this really solves the problem with the left unit
> (not in general, and not for IO either),
> it merely pushes it to a different place.
Not being a category theorist I find this all a bit confusing. Can you
give an example where with GHC and the fix I suggested you can show that
the associative law has been broken?
S.M.Kahrs
> [snip]
> > I don't think this really solves the problem with the left unit
> > (not in general, and not for IO either),
> > it merely pushes it to a different place.
> [snip]
> Not being a category theorist I find this all a bit confusing.
Nothing to do with category theory.
I took the law you cited and checked it out.
> Can you
> give an example where with GHC and the fix I suggested you can show tha=
t
> the associative law has been broken?
I didn't try to find a counter example.
I tried to prove the result and got stuck:
This is the law I was stuck with:
m >>= (\x -> k x >>= h) === (m >>= k) >>= h =
There were two cases to consider, m=R a, and m=M a - the former works=
out nicely,
but with the latter you get:
m >>= (\x -> k x >>= h)
= M a >>= (\x -> k x >>= h)
= M (a >>= \a'->case (\x -> k x >>= h) a' of
R b -> return b
M c -> c)
= M (a >>= \a'->case (k a' >>= h) of
R b -> return b
M c -> c)
and on the other side:
(m >>= k) >>= h =
= (M a >>= k) >>= h
= M (a >>= \a'->case k a' of
R b -> return b
M c -> c) >>= h
= M ((a >>= \a'->case k a' of
R b -> return b
M c -> c) >>= \a''->case h a'' of
R b -> return b
M c -> c)
Assuming that the associativity law holds for the original monad
(the one we try to fix for its dodgy left unit) then this can be changed =
to:
M (a >>= \a' -> (\a'->case k a' of
R b -> return b
M c -> c) a' >>= \a''->case h a'' of
R b -> return b
M c -> c)
= M ((a >>= \a' -> case k a' of
R b -> return b
M c -> c) >>= \a''->case h a'' of
R b -> return b
M c -> c)
Using associativity again:
= M (a >>= \x->(\a' -> case k a' of
R b -> return b
M c -> c)x>>=(\a''->case h a'' of
R b -> return b
M c -> c))
= M (a >>= \a' -> (case k a' of
R b -> return b
M c -> c) >>= \a''->case h a'' of
R b -> return b
M c -> c)
Assuming further that >>= is left-strict we can change that to:
= M (a >>= \a' -> (case k a' of
R b -> return b >>= \a''->...
M c -> c >>= \a''->...))
where the ... is twice the old case h a'' expression.
Now, this is the expression why I claimed the left-unit property of
the underlying monad would still show: if (return b>>=f) is the same
as f b (in the monad we try to fix) then the first part of this case
expression simplifies to exactly the same thing as we had derived from th=
e
other side of the equation.
But if it does not hold, we should be able to construct a counter example=
using the left-unit counter example from the underlying monad together
with, say, k=R. This all under the assumptions that the original monad=
m
satisfied the assoc law and that its >>= is left-strict.
Stefan Kahrs
Ken Shan
> 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?
Hal Daume III
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 | hda...@isi.edu
than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume
Jorge Adriano
> One may ask the question: what is seq useful for not in conjunction wit=
h
> 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.
Iavor S. Diatchki
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
> Has...@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 |
==================================================
Hal Daume III
you're from), which isn't misleading in this way.
--
Hal Daume III
"Computer science is no more about computers | hda...@isi.edu
than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume
Alastair Reid
Hal Daume <hda...@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
Jay Cox
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
Dylan Thurston
> 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
Jan-Willem Maessen
> 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.
Yep, floating point is by necessity a bit of a mess. On the other
hand, I don't think we ought to be claiming that addition of Nums is
associative, because it just isn't true. (Indeed, if we trap overflow
then even Int addition is non-associative; I'm agin overflow trapping
on Int for this among other reasons.)
I see four "solutions" to the problem of non-associativity of
floating point, in approximate order of flexibility:
1) Declare that Num is never associative. Compilers may re-associate
(+) only if the types involved can be shown to be associative.
Programmers may of course re-associate (+) in other cases as well,
if they know what they are doing.
2) Provide a compiler flag which indicates that the compiler can
assume assocativity of Num and optimize accordingly. Similar flags
exist for other compilers (gcc's -ffast-math comes to mind).
3) Provide an associative floating-point hierarchy, to be used with
the knowledge that "associativity" of such a type is only an
approximate notion.
4) Provide a way of annotating Num instances to indicate the
associativity property. I have no idea what form such an
annotation would take.
I therefore suspect (1) or (2) is good enough. (3) is way more
trouble than it's worth, I bet; (4) is a nifty research problem with
(so I hear) a certain amount of related research already out there.
The real problem of course is things like this: "Solve y = x + b for x
given y and b". We can't technically even *solve* the equation if
addition is non-associative. But this is, of course, a problem in
*every* language with limited-precision floating point. We
probably need to be forthright about this when educating new
programmers. I'm less clear how to couch this when presenting Num to
the experienced programmer.
Note that non-associativity is only one difficulty in working with
floating point. Instability caused by different register and memory
precision on x86 has proven to be a very noticable problem for me
during compiler development. The -fforce-mem option on gcc addresses
this issue at the cost of performance; my (limited) understanding of
the problem indicates that this flag sacrifices (false) extra
precision for predictability and thus for better accuracy (if you know
what you are doing). This has nothing to do with declared semantics
and everything to do with implementation hackery.
> This sounds very interesting! Is your dissertation available?
I'm making the last few fixes; it will be signed at the end of the
week and I'll gladly send out a link to the Haskell mailing list when
it's done.
-Jan-Willem Maessen
John Launchbury
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.
_______________________________________________
Ashley Yakeley
>Will the next version of Haskell have something better. I hope so, but I
>fear not.
Rename it "unsafeSeq"? No puns please...
But I think breaking Monad laws etc. is a different kind of unsafeness
from usPIO etc.
--
Ashley Yakeley, Seattle WA
unsafePerformIO is NOT Haskell!
Janis Voigtlaender
>
> 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:vo...@tcs.inf.tu-dresden.de
John Launchbury
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
_______________________________________________