Typesafe MRef with a regular monad

[Carl R. Witty]

"Simon Peyton-Jones" <simonpj@microsoft.com> writes:

> | 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
>  
> 	empty :: FM k
> 	insert :: Ord k => FM k -> k -> a -> (FM k, Key k a)
> 	lookup :: Ord k => 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.

Here's a hand-waving argument that you need either Typeable (or
something else that has a run-time concrete representation of types)
or ST/STRef (or something else, probably monadic, that can track
unique objects) to do this.  (Warning: there may be Haskell syntax
errors in the following; I haven't written Haskell for a while.)

Consider the following:

  let (m, _) = insert empty "key" "val"
      (_, k1) = insert empty "key" 'V'
      (_, k2) = insert empty "key" "val"
  in (lookup m k1, lookup m k2)

This gives a value of type (Maybe Char, Maybe String); I think the
intended semantics are that the value should be (Nothing, Just "val").
(Maybe the first lookup should throw an exception instead of returning
Nothing?  Surely it should not return (Just 'V') or 
(Just ((unsafeCoerce# 'V') :: String)).  (The second lookup must
return (Just "val"); otherwise, you're breaking referential
transparency.)

Now, imagine what the map looks like in memory.  Suppose it is just a
standard association list.  The key cannot be just the string "key",
or the pair ("key",1) (where 1 means it's the first thing inserted
into the map); it must somehow depend on the type of the value.
Hence, you need to use Typeable or some other run-time representation
of types.

The above argument convinces me that you need run-time types to
program TypedFM.  The problem in the above example is that you can
create a key in one map and attempt to use it in another map.  If you
could prohibit such an attempt (or even detect it), then you wouldn't
need Typeable.

But what does it mean to use a key in "the same map"?  In

  let (m1, k) = insert empty "key" "val"
      (m2, _) = insert m1 "key2" "val2"
  in lookup m2 k

you must allow the lookup of k in m2, even though m1 and m2 are
different maps (one has a key "key2" and the other doesn't).  Somehow,
a key must be usable with the map it was created in, and with
"descendents" of that map, but not with siblings of that map.  In an
impure language, this could be done with some sort of tag on the map,
but I don't see how to do so in a pure language.

Following the above chain of reasoning, we could create an version of
TypedFM that was based in the IO monad.  There would be a global
variable that you could use to dole out TypedFM tags; each map that
you created (in the IO monad, of course) would have a unique tag, and
keys of a map would have the same tag.  You could only use the maps in
a single-threaded fashion (i.e., within the IO monad); otherwise there
would be "sibling" maps and we would be back to needing Typeable.

We could try to associate keys with their maps in some other way.  For
instance, we could use the "ST" approach, and give keys and their maps
a dummy type parameter that would have to match.  Even then, we would
need something monad-like to single-thread the maps.

To summarize, I believe that you need either a run-time representation
of types (like Typeable) or some way to single-thread access to your
map objects (like the ST monad) to implement something like TypedFM.
We've seen an implementation using Typeable/Dynamic.  An
implementation in the ST monad might be more difficult, depending on
the intended semantics of TypedFM (what's supposed to happen if you
insert the same key with values of different types?); but for my
imagined uses of TypedFM, you could just use the ST monad with STRef's
directly.

If Typeable is necessary (and Dynamic is sufficient), or the ST monad
is necessary (and the ST monad is sufficient), then that doesn't leave
a lot of room for nice new language extensions (unless somebody can
come up with some way to single-thread objects that's even more clever
than the ST monad).

Carl Witty