MonadMemory class
Two questions came to mind while thinking of memory references in Haskell: 1. Is there a "standard" equivalent of the following: class (Monad m) => MonadMemory m r | m -> r where new :: a -> m (r a) read :: r a -> m a write :: r a -> a -> m () What kind of axioms should an instance of this class satisfy? 2. How would a "pure" instance of this class look like (obvious unsafePerformIO-based solutions aside)? Is it even possible in pure Haskell? Thanks much! -- Ariel J. Birnbaum
Hello Ariel, Friday, March 28, 2008, 1:02:39 AM, you wrote: class (Monad m) =>> MonadMemory m r | m -> r where there are more than one way to define such class. look at http://haskell.org/haskellwiki/Library/ArrayRef for examples -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
look at http://haskell.org/haskellwiki/Library/ArrayRef for examples
Thanks, Data.Ref.Universal looks just like it! One question though. In: class (Monad m) => Ref m r | m->r, r->m where Why is the second fundep necessary? -- Ariel J. Birnbaum
On Fri, 2008-03-28 at 00:02 +0200, Ariel J. Birnbaum wrote:
Two questions came to mind while thinking of memory references in Haskell:
1. Is there a "standard" equivalent of the following:
class (Monad m) => MonadMemory m r | m -> r where new :: a -> m (r a) read :: r a -> m a write :: r a -> a -> m ()
This has come up a few times and been written by many Haskellers (usually called MonadRef.) The problem is the functional dependencies. Any choice you make is either too limiting or too annoying to use and it was never agreed which would be best.
What kind of axioms should an instance of this class satisfy?
There are quite a few obvious ones, but I'm not sure it's particularly necessary.
2. How would a "pure" instance of this class look like (obvious unsafePerformIO-based solutions aside)? Is it even possible in pure Haskell?
The issue here is a type one, not a semantics one. I believe the only way to purely get such an interface (in current Haskell) is to use unsafeCoerce. Other than that, it's a straightforward state monad.
This has come up a few times and been written by many Haskellers I was quite certain of that, hence my puzzlement at being unable to find it =)
What kind of axioms should an instance of this class satisfy? There are quite a few obvious ones, but I'm not sure it's particularly necessary. I'm still curious, though. In general I think it's a GoodThing (TM) if stuff (especially the sort of typeclasses) come with a semantic base we can use for reasoning about it; in the sort of way the Monad class comes with the monad laws.
The issue here is a type one, not a semantics one. An issue nevertheless, IMHO
I believe the only way to purely get such an interface (in current Haskell) is to use unsafeCoerce. I'm not so sure about calling unsafeCoerce 'pure' ;)
-- Ariel
On 3/27/08, Ariel J. Birnbaum <valgarv@gmx.net> wrote:
class (Monad m) => MonadMemory m r | m -> r where new :: a -> m (r a) read :: r a -> m a write :: r a -> a -> m ()
What kind of axioms should an instance of this class satisfy?
Here's some thoughts: (~=) means "equivalent excluding allocation effects". (==) means "equivalent" 1) Unreferenced allocations do nothing: (new a >> m) ~= m 2) Read+Write laws: (read r >>= write r) == return () (new x >>= read) ~= return x (write r x >>= read) == (write r x >> return x) 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)
2. How would a "pure" instance of this class look like (obvious unsafePerformIO-based solutions aside)? Is it even possible in pure Haskell?
Yes, it is possible with unsafeCoerce. It's possible without unsafeCoerce if you add a Typeable constraint or pass a GADT type representation to new. To be truly safe you need higher-rank types and use the same trick that ST does. But there's not much point; you may as well use ST. At that point, it's actually a pretty simple state monad: data HeapItem = forall a. HeapItem a newtype Ref s a = Ref Integer newtype RefM s = RefM (State (Integer, Map Integer HeapItem)) -- use unsafeCoerce to extract elements in read. Handling garbage collection is tricky, though. -- ryan
(write r x >>= read) == (write r x >> return x) You probably mean (write r x >> read r) == (write r x >> return x)?
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?
It's possible without unsafeCoerce if you add a Typeable constraint or pass a GADT type representation to new. Care to develop?
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 ;)
But there's not much point; you may as well use ST. Not much *practical* point, I agree. I mostly asked out of curiosity.
Handling garbage collection is tricky, though. Can it even be done without compiler support?
-- Ariel J. Birnbaum
On 3/27/08, Ariel J. Birnbaum <valgarv@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
Hi Ariel J. Birnbaum wrote:
Two questions came to mind while thinking of memory references in Haskell:
1. Is there a "standard" equivalent of the following:
class (Monad m) => MonadMemory m r | m -> r where new :: a -> m (r a) read :: r a -> m a write :: r a -> a -> m ()
I do not think you can call it standard, but TypeCompose http://hackage.haskell.org/cgi-bin/hackage-scripts/package/TypeCompose-0.5 do implement Data.RefMonad, which does what you are describing. Greetings, Mads Lindstrøm
What kind of axioms should an instance of this class satisfy?
2. How would a "pure" instance of this class look like (obvious unsafePerformIO-based solutions aside)? Is it even possible in pure Haskell?
Thanks much!
participants (5)
-
Ariel J. Birnbaum -
Bulat Ziganshin -
Derek Elkins -
Mads Lindstrøm -
Ryan Ingram