On 3/27/08, Ariel J. Birnbaum
(write r x >>= read) == (write r x >> return x) You probably mean (write r x >> read r) == (write r x >> return x)?
Yes. Oops!
3) References are independent: If m does not refer to r, then: (read r >>= (\x -> m >> return x)) == m >> read r (write r x >> m) == m >>= (\v -> write r x >> return v) What if m writes to r' which is read by another thread, which in turn writes another value into r? What exactly does "does not refer to r" mean?
I was going for an intuitive definition, not quite a formal one. An approximation is: doesn't have a reference to "r" or to any other reference that refers to r (recursively). I was not considering parallelism; that does break this axiom. A weaker form of the axiom which doesn't break in the face of parallelism and is more formal: (new x >>= (\r -> m >> return r)) == (m >> new x)
It's possible without unsafeCoerce if you add a Typeable constraint or pass a GADT type representation to new. Care to develop?
Sure: http://ryani.freeshell.org/haskell/RefMonad.hs Here's the module header: {-# LANGUAGE GADTs, ExistentialQuantification, Rank2Types #-} module RefMonad ( TypRep(..), -- TypRep a, GADT reifying type representation of a Typeable, -- typeclass of types that have a TypRep typRep, -- :: TypRep a Dynamic(..), -- Dynamic (TypRep a) a castDyn, -- :: Typeable a => Dynamic -> Maybe a RefM, -- RefM s a. abstract, instance of Monad. -- s represents the "heap state" runRefM, -- :: (forall s. RefM s a) -> a -- "forall" forces us to not care about the initial state of the heap. Ref, -- Ref s a. abstract reference to objects of type a newRef, -- :: Typeable a => a -> RefM s (Ref a) readRef, -- :: Ref s a -> RefM s a writeRef -- :: Ref s a -> a -> RefM s () ) Things to notice: 1) RefM & Ref have to be abstract, otherwise we can break type safety by constructing invalid heaps or references, leading to "error" in one of the fromMaybe calls in readRef. 2) newRef has a Typeable constraint; this allows us to avoid unsafeCoerce by doing "dynamic" casts using a type equality check. 3) Check out the type of runRefM. 4) No garbage collection :(
To be truly safe you need higher-rank types and use the same trick that ST does. Here I was, naively thinking I could put off learning about that for now ;)
It's not that complicated; the trick is all in the type of runST (which I copy in runRefM) runRefM :: (forall s. RefM s a) -> a Now, references can't escape from runRefM; consider: runRefM (newRef (1 :: Integer)) newRef (1 :: Integer) has type forall s. RefM s (Ref s Integer) Trying to apply runRefM to this we get (forall s. RefM s (Ref s Integer)) -> Ref s Integer which won't typecheck because the type variable "s" escapes from quantification.
But there's not much point; you may as well use ST. Not much *practical* point, I agree. I mostly asked out of curiosity.
Of course, learning is its own reward :)
Handling garbage collection is tricky, though. Can it even be done without compiler support?
I'm not sure. I'm suspect not, but I can't prove it. -- ryan