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