MonadRef pure implementation

Question

I am researching on this problem which related to MonadRef. When look at the definition

class MonadRef r m | m -> r where
    newRef :: a -> m (r a)
    readRef :: r a -> m a
    writeRef :: r a -> a -> m ()

I was thinking how to implement this with pure data structure but failed to find an answer. Actually, all the known standalone implementations (which does not depend on another MonadRef)

instance TVar STM
instance IORef IO
instance (STRef s) (ST s)

require RealWorld in pratise. Is that means we can only have MonadRefs that are not pure?

When I tried to resolve this, I first figure out that Maybe cannot implement MonadRef simply because it is too simple and there is no space for it to record the required information. As a generalise of this I conclude that for any implementation the Monad must be able to contain arbitrary number of information, simply because you can call newRef as many times as you can.

So I considered [] but it is still a fail because the data stored within the Monad can be of any type. I don't know how to construct a container in Haskell that can store any type of data whilst still have the ability to extract the data back with proper type (maybe existential quantification can help? But I still don't know how to do so).

Couldn't a State with a container and a counter for keys work? — András Kovács, Jun 23 '14 at 13:52
@DanielWagner This depands how would you define "pure". According to the document it says "The s parameter is either an uninstantiated type variable (inside invocations of runST), or RealWorld (inside invocations of Control.Monad.ST.stToIO)", so it seems either options require some sort of "magic". — Earth Engine, Jun 23 '14 at 23:03
@EarthEngine Uninstantiated type variables aren't magic. And yes, you need some compiler support somewhere, but `ST` *is* that support. — Daniel Wagner, Jun 23 '14 at 23:19
@DanielWagner No... Uninstantiated type means you cannot specify what the actual type it should use, and the implementation select this for you. And if you read the implementation of `runST` you can see it uses `RealWorld` inside... — Earth Engine, Jun 23 '14 at 23:59

score 3 · Accepted Answer · answered Jun 23 '14 at 15:28

You can nearly get there (implementing the equivalent of ST purely) by using a State monad with a state that is a Map dictionary from reference IDs to the value inside that reference.

But Haskell's type system lacks dependent types, in which the type of a value depends on the value of another term of fixed type. Because of this, it cannot express that the type inside the reference depends on the reference's ID, in such a way that all types are allowed.

You can get around this by letting the values stored be of type GHC.Exts.Any and use Unsafe.Coerce.unsafeCoerce to convert to the correct type internally.

But unsafeCoerce is, as advertised, unsafe. This again means that Haskell's type system cannot give you any guarantees that you are using the references in a type safe way, and if you make an error you can get GHC to crash this way. (If MonadRef had had a Data.Typeable.Typeable constraint on its reference contents, that could have been used to do this, but it doesn't. (And you could then have put Data.Dynamic.Dynamic instead of Any inside the map.))

However, if you do use unsafeCoerce in this way nevertheless, taking care to hide the ID type used, and to implement the same API as ST does, including the s parameter which prevents different ST "threads" from confusing each other's references, then this should actually work safely as a library. I found at least one attempt on GitHub. (It also tries to work as a transformer, although I am suspicious of whether that is safe.)

For me, use `unsafeXXX` is cheating, just like that use `unsafePerformIO` and claim the function to be "pure". But if this is the only way to do things then we have to accept. — Earth Engine, Jun 24 '14 at 10:32
Sounds like the lack of a Typeable constraint and the lack of a functional dependency in the other direction are both important weaknesses with MonadRef. Perhaps a variation is called for? — Barend Venter, Jun 29 '15 at 01:02

MonadRef pure implementation

1 Answers1