State monads don't respect the monad laws in Haskell

[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