[Haskell] Re: ST/STRef vs. IO/IORef

[Remi Turk]

On Fri, Aug 05, 2005 at 08:04:53AM +0200, Till Mossakowski wrote:
> Sebastian Sylvan wrote:
> >Hmmm... Wasn't that what he said?
> 
> I disagree with the equation "primitives = unsafe" that
> is implicit in sentence
>
>  to be implemented _efficiently_, also needs
>  something like unsafePerformIO (or even lower-level unsafe
>  mutable state primitives).
> 
> The point is that ST uses *safe* primitives, and not "something
> like unsafePerformIO".

Ah, I think I understand what we're disagreeing about exactly
now. We're understanding "primitive" to mean different things :)

You're seeing runST, newSTRef, writeSTRef etc as primitives, is
that correct? I see them as the public interface to something
which is implemented in something else. That is, just like
the "memo" function (deprecated, from the package util) is a safe
interface (memo is nicely referentially transparant) to a piece
of functionality implemented using unsafe primitives
(unsafePerformIO), the ST monad a perfectly safe abstraction
built on top of not-so-safe primitives. And with primitives I
mean unsafePerformIO in my previously attached implementation. In
GHC's implementation, this is even more clear:

  writeSTRef :: STRef s a -> a -> ST s ()
  writeSTRef (STRef var#) val = ST $ \s1# ->
      case writeMutVar# var# val s1#      of { s2# ->
          (# s2#, () #) }
    (fptools/libraries/base/GHC/STRef.lhs)
  
  {-# INLINE runST #-}
  runST :: (forall s. ST s a) -> a
  runST st = runSTRep (case st of { ST st_rep -> st_rep })
  
  {-# NOINLINE runSTRep #-}
  runSTRep :: (forall s. STRep s a) -> a
  runSTRep st_rep = case st_rep realWorld# of (# _, r #) -> r
    (fptools/libraries/base/GHC/ST.lhs)

There is a lot of messing around with state here. Actually,
runST(Rep) is remarkably similiar to unsafePerformIO:

  {-# NOINLINE unsafePerformIO #-}
  unsafePerformIO	:: IO a -> a
  unsafePerformIO (IO m) = case m realWorld# of (# _, r #)   -> r
    (fptools/libraries/base/GHC/IOBase.lhs)

On Fri, Aug 05, 2005 at 08:12:36AM +0200, Till Mossakowski wrote:
> Remi Turk wrote:
> 
> >In a final attempt to convince someone of I'm not exactly sure
> >what, I attached a simple implementation of the ST monad in
> >terms of unsafePerformIO + IORef + IOArray.
> 
> OK, but you have to reason about this implementation to show that
> it is safe (which may be difficult because unsafePerformIO makes
> reasoning extremely difficult), while the primitives of ST are
> more easily proved to be safe.

Though it's certainly not a formal proof, it seems to be ok by
both the "can you imagine an alternative, possibly horribly slow,
but pure implementation" and by the "does it perform no observable
side-effects and does it always yield the same value" criteria.

However, this is almost what I meant: Assume you'd really like to
have (1) the efficient histogram function from my previous message
and (2) an efficient implementation of ixmap.

You could implement both using unsafePerformIO + IOArray's and
still be perfectly safe. However, you'd have to prove it's safe
_twice_, both for (1) and for (2).

The superior alternative is to first implement the ST monad using
unsafePerformIO + IOArray's, proof that to be safe, and then
implement (1) and (2) using ST without having to think about
safety anymore.

Happy hacking,

Remi "We're probably agreeing 99.9% anyway" Turk

-- 
Nobody can be exactly like me. Even I have trouble doing it.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/haskell/attachments/20050805/6a5bed2e/attachment.bin