Oh bother, I forgot to add that you can of course insert a new value with an old key (suitably typed) and have it overwrite. Else, as you say, there would not be much point. Maybe it'd be better to have a separate key-construction function newKey :: k -> Key k a instead of having insert return a key. S | -----Original Message----- | From: Ralf Hinze [mailto:ralf@informatik.uni-bonn.de] | Sent: 06 June 2003 14:12 | To: Simon Peyton-Jones; Tim Sweeney; haskell@haskell.org; Ashley Yakeley | Subject: Re: Typesafe MRef with a regular monad | | > 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. | | Here is a Haskell 98 implementation: | | > module TypedFM | > where | | > data FM k = FM | > data Key k a = Key k a | | > empty = FM | > insert FM k a = (FM, Key k a) | > lookup FM (Key k a) = Just a | | Cheers, Ralf |