ST and IO. Two problems. Some old some new?

[Koen Claessen]

Amr Sabry wrote:

 | unsafeIOtoST is documented as unsafe because
 | exceptions that would have been caught in the IO monad
 | are not caught in the ST monad but this is irrelevant
 | to the rest of the message.

I think it is unsafe because *all* IO-type side effects (not
only exceptions but also file reading and writing, and
changing IORef's) of the IO computation will be executed in
the ST monad.

Basically, one can write unsafePerformIO with unsafeIOtoST:

  unsafePerformIO :: IO a -> a
  unsafePerformIO m = runST (unsafeIOtoST m)

This is why unsafeIOtoST has the same status as
unsafePerformIO.

 | 2. Soundness of stToIO
 :
 | data Var a = Var { get :: () -> IO a,
 |                    set :: a -> IO ()}

(Why does get have this type?)

 | nloc :: Int -> Var Int
 | nloc a =
 |   runST
 |   (do x <- newSTRef a
 |       return
 |         (Var {get =
 |                 \() -> stToIO $ readSTRef x,
 |               set =
 |                 \a -> stToIO $ writeSTRef x a}))

Does this really type check? The type of stToIO is:

  stToIO :: ST RealWorld a -> IO a

Therefore, the type of the above x is

  x :: STRef RealWorld Int

And the type of the whole do{...} is:

  do{...} :: ST RealWorld (Var Int)

Which runST does not like! If this were possible, we could
do something scary like:

  globalPolyVar :: Var a
  globalPolyVar =
    runST (do x <- newSTRef undefined
              return (Var (stToIO (readSTRef x))
                          (\a -> stToIO (writeSTRef x a))))

  typeCastIO :: a -> IO b
  typeCastIO a =
    do set globalPolyVar a
       get globalPolyVar

Which would be a disaster!

 | gensym :: () -> Int
 | gensym = (...)

Of course, we knew this could be done with unsafePerformIO
already, no need to take in unsafeSTtoIO.

/Koen.

--
Koen Claessen
http://www.cs.chalmers.se/~koen
Chalmers University, Gothenburg, Sweden.