[Haskell-cafe] MonadMemory class

[Ryan Ingram]

On 3/27/08, Ariel J. Birnbaum <valgarv at gmx.net> wrote:
> > (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