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 «s ожидания. не

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

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

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

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