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.