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

[Stefan O'Rear]

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 #))

evaluate x = GHC.Exception.evaluate x

Stefan