Typesafe MRef with a regular monad

Simon Peyton-Jones simonpj@microsoft.com
Fri, 6 Jun 2003 13:51:44 +0100


| 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).

A more concrete way to formulate a problem that I believe to be
equivalent is this.  Implement the following interface

   module TypedFM where
	data FM k		-- Abstract; finite map indexed by keys
of type k
	data Key k a		-- Abstract; a key of type k, indexing a
value of type a
=20
	empty :: FM k
	insert :: Ord k =3D> FM k -> k -> a -> (FM k, Key k a)
	lookup :: Ord k =3D> FM k -> Key k a -> Maybe a

The point is that the keys are typed, like Refs are.  But the finite map
FM is only parameterised on k, not a, so it can contain (key,value)
pairs of many different types.

I don't think this can be implemented in Haskell, even with
existentials.  But the interface above is completely well typed, and can
be used to implement lots of things.  What I *don't* like about it is
that it embodies the finite-map implementation, and there are too many
different kinds of finite maps.

There is, I guess, some nice language extension that would enable one to
program TypedFM, rather than provide it as primitive; but I don't know
what it is.

Simon