FixIO/ Tackling Awkward Squad
Levent Erkok
erkok@cse.ogi.edu
Fri, 16 Feb 2001 09:51:03 -0800
Marcin 'Qrczak' Kowalczyk wrote:
>
> Fri, 16 Feb 2001 04:14:26 -0800, Simon Peyton-Jones <simonpj@microsoft.com> pisze:
>
> > fixIO m = do { v <- newEmptyMVar
> > ; result <- m (unsafePerformIO (takeMVar v))
> > ; putMVar v result
> > ; return result }
>
> If we have unsafePerformIO, why not this?
>
> fixIO m = let x = unsafePerformIO (m x) in return $! x
Why the strict application?
You probably want:
do { fixIO (\x -> return (x+1)); return 2 }
to evaluate to (return 2). But the version with strict application
diverges.
By the way, we can prove that it should evaluate to (return 2) using the
monadic-fixpoint axiomatization:
do { fixIO (\x -> return (x+1)); return 2 }
= {expand do}
fixIO (\x -> return (x+1)) >>= \_ -> return 2
= {rewrite}
fixIO (return . (+1)) >>= \_ -> return 2
= {mfix (return . h) = return (fix h), mfix = fixIO for the IO monad}
return (fix (+1)) >>= \_ -> return 2
= {return x >>= f = f x}
return 2
So, it looks like:
fixIO m = let x = unsafePerformIO (m x) in return x
will do a better job.
-Levent.