Haskell confusion avec ContT, callCC, quand

Question

Poursuite de la quête pour donner un sens à ContT et ses amis. Veuillez considérer le code (absurde mais illustratif) ci-dessous:

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 

Ce code ne compile pas. Toutefois, si le remplace le when avec l'appel k commenté ci-dessous, il compile. Que se passe-t-il?

Sinon, si je commente la ligne x2, il compile également. ???

De toute évidence, il s'agit d'une version distillée du code original et donc tous les éléments ont un but. Appréciez l'aide explicative sur ce qui se passe et comment y remédier. Merci.

Answer 1

Le problème a à voir avec les types de when et either, rien de particulier à ContT:

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

Le second argument doit être de type m() pour une monade m. La ligne when de votre code pourrait donc être modifié comme ceci:

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

pour faire la compilation de code. Ce n'est probablement pas ce que vous voulez faire, mais il nous donne un indice quant à ce qui pourrait être faux: le type de k a été déduit pour être quelque chose de désagréable à when.

Maintenant, pour la signature either: notez que les deux arguments à either doivent être des fonctions qui produisent des résultats du même type. Le type de return ici est déterminé par le type de x, qui est à son tour fixé par la signature explicite sur v. Ainsi, le bit (k . Left) doit avoir le même type; à son tour, fixe le type de k à (GHC déterminé)

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

Ceci est incompatible avec les attentes de when.

Lorsque vous commentez la ligne x2, cependant, son effet sur le point de vue du contrôleur de type du code est supprimé, si k n'est plus forcé dans un type pratique et est libre d'assumer le type

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

ce qui est bien dans when livre. Ainsi, le code compile. En guise de note finale, j'ai utilisé la fonction breakpoints de GHCi pour obtenir les types exacts de k dans les deux scénarios - je ne suis pas assez expert pour les écrire à la main et être certain de leur exactitude. :-) Utilisez :break ModuleName line-number column-number pour l'essayer.