[tim@epicgames.com: Fw: Typesafe MRef with a regular monad]

[Andrew J Bromage]

G'day all.

On Wed, Jun 04, 2003 at 07:31:03PM -0500, Tim Sweeney wrote:

> 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?

WARNING: This is not rigorous.

Take a prototypical simple state monad:

type MyRefMon a = SomeState -> (a. SomeState)

type MyRef a = Int	-- Could be anything other than Int, but
			-- the important point is that "a" is not
			-- mentioned on the RHS anywhere.

where SomeState is abstract but concrete.  Note that it has no
type parameters.

Let's also assume the existence of this function:

myDeref :: MyRef a -> MyRefMon a

Again, we know nothing about its implementation (yet).

Without loss of generality, and because a has no type constraints,
myDeref is equivalent to a function of this type:

myDeref' :: Int -> SomeState -> (a, SomeState)

(This step I believe to be far too handwavy.  I have no justification
for the ability to drop the "a" parameter here except that Haskell
semantics state that if a is not constrained, you can't do anything
with it.)

Intuitively, there is nothing in the above type signature which gives
you any way to construct something of type a, therefore it must be
bottom.  The parametricity theorem (i.e. "free theorem") can probaly
be used to show this formally.

The only ways I can think of to get over this within Haskell is to:

  - change the definition of MyRef so that it contains
    enough information to extract something of type a
    from SomeState, or

  - constrain the type (e.g. using Typeable).

Cheers,
Andrew Bromage