"Simon Peyton-Jones" <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell