Typesafe MRef with a regular monad

[Tim Sweeney]

Conjecture: It's impossible to implement RefMonad directly in Haskell
without making use of built-in ST or IO functionality and without unsafe or
potentially diverging code (such as unsafeCoerce).

Any takers?

If this is true or suspected to be true, any thoughts on whether a structure
besides Monad could encapsulate safe references in Haskell without core
language changes? My intuition is that no such structure exists in Haskell
with power and flexibility equivalant to RefMonad (support for references of
arbitrary types not limited by their context.)

If this is generally thought to be impossible in Haskell, what sort of
language extensions would be needed to make this work safely, meaning
without unsafe coercions?  This seems like a hairy problem.  Yet it gets to
the core question of whether Haskell's monads can really implement
imperative features (such as references) in a purely functional way, or are
just a means of sequentializing those imperative constructs that are built
into the runtime.

Any solutions I can think of require a dependent-typed heap structure, and
that all references be parameterized by the heap in which they exist.

-Tim

----- Original Message -----
From: "Ashley Yakeley" <ashley@semantic.org>
To: <haskell@haskell.org>
Sent: Wednesday, June 04, 2003 5:19 PM
Subject: Re: Typesafe MRef with a regular monad


> In article <200306042005.h54K5mG0014203@adric.fnmoc.navy.mil>,
>  oleg@pobox.com wrote:
>
> > Ashley Yakeley wrote:
> > ] ] Is it possible to actually implement a working instance of RefMonad
in
> > ] ] Haskell, without making use of a built-in monad like IO or ST?
> >
> > ] You certainly wouldn't be able to do this for any monad M which had:
> >
> > ]   performM :: forall a. M a -> a;
> >
> > ] ...because it wouldn't be type-safe: you'd be able to construct coerce
> > ] :: a -> b just as you can with unsafePerformIO.
> >
> > Fortunately, that doesn't seem to be the case.
>
> That's only because you've failed to do the difficult part: implement
> newRef. Your monadic solution has a statically typed/sized store: I'd
> say it doesn't properly count as a "heap" since you can't heap new stuff
> on it.
>
> The original problem was to create an instance of
>
>   class Monad m => RefMonad m r | m -> r where
>      newRef :: a -> m (r a)
>      readRef :: r a -> m a
>      writeRef :: r a -> a -> m ()
>
> without making use of IO or ST. Given some M and R that have
>
>   instance RefMonad M R
>   performM :: forall a. M a -> a
>
> one can write this:
>
>   coerce :: forall a b. a -> b;
>   coerce a = let
>     {
>     ref = performM (newRef Nothing);
>     } in performM (do
>     {
>     writeRef ref (Just a);
>     mb <- readRef ref;
>     case mb of {Just b -> return b;};
>     });
>
> --
> Ashley Yakeley, Seattle WA
>
> _______________________________________________
> Haskell mailing list
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
>