Карта полиморфных значений в Haskell

Предположим, у меня есть класс, который объявляет некоторые конструкторы для значений его типов членов:

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

Далее предположим, что я хочу создать набор значений с помощью этих полиморфных конструкторов и поместить их в пакет Map from containers. Но что важно, я хочу, чтобы значения оставались полиморфными и откладывали решение об их конкретном типе до тех пор, пока они не будут извлечены из карты.

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

newtype MapC = MapC (Map String WrapC)

Используя расширение RankNTypes, я могу определить такую ​​карту, и следующее определение свидетельствует о том, что из нее действительно можно извлечь полиморфные значения:

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

Однако, когда я хочу добавить значение на карту, я сталкиваюсь с ошибкой типа, потому что Haskell, по-видимому, не может унифицировать некоторые переменные скрытого типа. Определение:

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

не скомпилируется с:

• 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

Интуитивно я предполагаю, что внутри WrapC скрыта переменная типа, которую нельзя унифицировать. Чего я не понимаю, так это зачем это нужно. Или как я могу заставить этот пример работать…

🤔 А знаете ли вы, что...
Haskell популярен в академической среде и часто используется в исследовательских проектах.


5
101
2

Ответы:

Решено

Вам просто нужно передать вашей функции что-то действительно полиморфное:

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

Но я бы предложил что-то еще глупее, может быть. Можете ли вы уйти с этим?

type MapC = Map String (Either Int String)

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

Никаких расширений системы типов не требуется.


Позвольте мне дополнить существующий ответ, обратившись к последнему пункту:

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.

Вы можете увидеть, что происходит не так, посмотрев на подписи типов для add и get:

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

Вопрос, который вам нужно задать: «Кто выбирает шрифт для t?».

Подпись типа для add говорит, что тот, кто вызывает add, может выбрать t как угодно (до тех пор, пока C t сохраняется), и это значение будет вставлено в карту.

Точно так же сигнатура типа для get говорит, что любой, кто вызывает get, может выбрать t что угодно (до тех пор, пока C t сохраняется), и это значение будет извлечено из карты.

Это, однако, не может работать: что, если мы вызовем add, выбрав t=A, вставим значение в карту, а затем вызовем get, чтобы извлечь то же значение из карты, выбрав другой t=B? Это равнозначно изменению типа значения, поэтому должно быть запрещено.

Любое решение должно каким-то образом заставить двух абонентов договориться о t.

Одно из решений — заставить вызывающего add вносить полиморфное значение, а не просто значение для какого-то конкретного t, которое он выбрал. Вызывающий get остается свободным в выборе любого t.

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

Другое решение состоит в том, чтобы позволить звонящему add выбрать только один t по своему вкусу. Однако в таком случае вызывающая сторона get должна адаптироваться к любому такому выбору: тип результата будет иметь количественную оценку только экзистенциально вместо количественной оценки повсеместно.

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)