Путаница в Haskell с ContT, callCC, когда

Question

Продолжаем поиски понимания ContT и друзей.Пожалуйста, рассмотрите (абсурдный, но наглядный) код ниже:

v :: IO (Either String [String])
v = return $ Left "Error message"

doit :: IO (Either String ())
doit = (flip runContT return) $ callCC $ \k -> do
    x <- liftIO $ v
    x2 <- either (k . Left) return x
    when True $ k (Left "Error message 2")
    -- k (Left "Error message 3")
    return $ Right () -- success

Этот код не компилируется.Однако если заменить when с прокомментированным вызовом k под ним он компилируется.Что происходит?

Альтернативно, если я закомментирую строку x2, она также скомпилируется.???

Очевидно, что это очищенная версия исходного кода, поэтому все элементы служат определенной цели.Цените пояснительную помощь о том, что происходит и как это исправить.Спасибо.

Answer 1

Проблема здесь связана с типами when и either, ничего особенного для ContT:

when :: forall (m :: * -> *). (Monad m) => Bool -> m () -> m ()
either :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c

Второй аргумент должен иметь тип m () для какой-то монады m.А when Таким образом, строка вашего кода может быть изменена следующим образом:

when True $ k (Left "Error message 2") >> return ()

чтобы код скомпилировался.Вероятно, это не то, что вы хотите сделать, но это дает нам подсказку о том, что может быть не так: kбыл сделан вывод, что этот тип является чем-то неприятным для when.

Теперь о either подпись:обратите внимание, что два аргумента either должны быть функциями, которые выдают результаты одного и того же типа.Тип return здесь определяется типом x, что, в свою очередь, фиксируется явной подписью на v.Таким образом (k . Left) бит должен иметь тот же тип;это, в свою очередь, фиксирует тип k при (определяется GHC)

k :: Either String () -> ContT (Either String ()) IO [String]

Это несовместимо с whenожидания.

Когда вы закомментируете x2 строка, однако ее влияние на представление кода средством проверки типов удаляется, поэтому k больше не принуждается к неудобному типу и может свободно принимать тип

k :: Either [Char] () -> ContT (Either [Char] ()) IO ()

что хорошо в whenкнига.Таким образом, код компилируется.

В заключение я использовал функцию точек останова GHCi, чтобы получить точные типы k по двум сценариям - я далеко не настолько эксперт, чтобы записать их от руки и быть каким-либо образом уверенным в их правильности.:-) Использовать :break ModuleName line-number column-number чтобы попробовать это.