### Re: The Proper Definition of (evaluate :: a -> IO a)

Stefan O'Rear <stefanor <at> cox.net>

2007-05-07 23:11:04 GMT

On Mon, May 07, 2007 at 06:57:51PM -0400, Isaac Dupree wrote:
> Malcolm Wallace wrote:
> > But I guess this semantics
> > accords with Isaac's suggested definition:
> > evaluate x = (x `seq` return x) >>= return
Let's try a little Equational Reasoning:
evaluate x = (x `seq` return x) >>= return
evaluate x = (>>=) (seq x (return x)) return
evaluate x = bindIO (seq x (returnIO x)) returnIO
evaluate x = IO (\st1 -> case unIO (seq x (returnIO x)) st1 of (# st2, a #) -> unIO (returnIO a) st2)
evaluate x = IO (\st1 -> case unIO (seq x (returnIO x)) st1 of (# st2, a #) -> (# st2, a #))
evaluate x = IO (\st1 -> case seq x (\st3 -> (# st3, x #)) st1 of (# st2, a #) -> (# st2, a #))
evaluate x = IO (\st1 -> case (case x of __DEFAULT -> (\st3 -> (# st3, x #))) st1 of (# st2, a #) -> (# st2, a #))
evaluate x = IO (\st1 -> case x of __DEFAULT -> case (\st3 -> (# st3, x #)) st1 of (# st2, a #) -> (# st2, a #))
evaluate x = IO (\st1 -> case x of __DEFAULT -> case (# st1, x #) of (# st2, a #) -> (# st2, a #))
evaluate x = IO (\st1 -> case x of __DEFAULT -> (# st1, x #))
evaluate x = IO (\st1 -> case x `seq` () of () -> (# st1, x #))

(Continue reading)