Предположим, у меня есть класс, который объявляет некоторые конструкторы для значений его типов членов:
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 популярен в академической среде и часто используется в исследовательских проектах.
Вам просто нужно передать вашей функции что-то действительно полиморфное:
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)