Suppose I've got a class, which declares some constructors for values of its member types:

class C t where
  fromInt :: Int -> t
  fromString :: String -> t

Further suppose, I want to create a bunch of values using these polymorphic constructors and put them in a Map from containers package. But importantly, I want the values to remain polymorphic and deferr the decision on their concrete type until they are extracted from the map.

newtype WrapC = WrapC (forall t . C t => t)

newtype MapC = MapC (Map String WrapC)

Using RankNTypes extension I can define such a map and the following definition witnesses the fact that polymorphic values indeed can be extracted from it:

get :: C t => String -> MapC -> Maybe t
get key (MapC m) = fmap (\(WrapC t) -> t) $ Map.lookup key m

However, when I want to add a value to the map, I'm facing a type error, because Haskell apparently cannot unify some hidden type variables. The definition:

add :: C t => String -> t -> MapC -> MapC
add key val (MapC m) = MapC $ Map.insert key (WrapC val) m

fails to compile with:

• Couldn't match expected type ‘t1’ with actual type ‘t’
  ‘t1’ is a rigid type variable bound by
    a type expected by the context:
      forall t1. C t1 => t1
    at src/PolyMap.hs:21:53-55
  ‘t’ is a rigid type variable bound by
    the type signature for:
      add :: forall t. C t => String -> t -> MapC -> MapC

Intuitively I'm guessing that's the type variable hidden inside WrapC that cannot be unified. What I don't understand is why it needs to be. Or how can I make this example work…

CodePudding user response：

You just need to hand your function something actually polymorphic:

add :: String -> (forall t. C t => t) -> MapC -> MapC

But I would propose something even dumber, maybe. Can you get away with this?

type MapC = Map String (Either Int String)

get :: C t => String -> MapC -> Maybe t
get k m = either fromInt fromString <$> Map.lookup k m

No type system extensions needed.

CodePudding user response：

Let me complement the existing answer by addressing the last point:

Intuitively I'm guessing that's the type variable hidden inside WrapC that cannot be unified. What I don't understand is why it needs to be.

You can see what is going wrong by looking at the type signatures for add and get:

add :: C t => String -> t -> MapC -> MapC
get :: C t => String -> MapC -> Maybe t

The question you need to ask is "who is choosing the type for t?".

The type signature for add says that whoever calls add can choose t to be anything (as long as C t holds), and that value will be inserted in the map.

Similarly, the type signature for get says that whoever calls get can choose t to be anything (as long as C t holds), and that value will be extracted from the map.

This, however, can not work: what if we call add choosing t=A, insert the value in a map, and then call get to extract the same value from the map choosing a different t=B? This would amount to changing the type of the value, hence must be disallowed.

Any solution must make the two callers agree on t in some way.

One solution is to make the caller of add deposit a polymorphic value, not just a value for some specific t they chose. The caller of get remains free to choose any t.

add :: String -> (forall t. C t => t) -> MapC -> MapC
get :: C t => String -> MapC -> Maybe t

Another solution is to keep the caller of add free to choose only one t of their liking. However, in such case, the caller of get must adapt to any such choice: the result type will only be existentially quantified instead of universally quantified.

add :: C t => String -> t -> MapC -> MapC
-- pseudo-code:
--   get ::  String -> MapC -> (exists t. C t => Maybe t)
-- Since Haskell has no "exists", we need to encode it somehow, e.g.:
get :: String -> MapC -> SomeC

data SomeC = forall t . C t => SomeC (Maybe t)