Haskell confusion avec ContT, callcc, quand

Question

quête continue de donner un sens ContT et les amis. S'il vous plaît considérer le code (mais absurde illustration) 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 remplacement du when à l'appel k commenté ci-dessous, il compile. Que se passe-t-il?

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

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

Answer 1

Le problème est ici à 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 certains m monade. La ligne de when de votre code pourrait ainsi être modifié comme ceci:

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

pour faire la compilation de code. Ceci est probablement pas ce que vous voulez faire, mais il nous donne une indication quant à ce qui pourrait se tromper. Le type de k a été inférée être quelque chose à un goût désagréable when

Maintenant, pour la signature de either: avis 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é, de sorte k ne soit plus contraint à un type peu pratique et est libre de prendre le type

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

ce qui est bien dans le livre de when. Ainsi, le code compile.

Comme note finale, je l'installation de points d'arrêt de GHCi pour obtenir les types exacts de k selon les deux scénarios - je suis loin d'être suffisant d'experts pour les écrire à la main et être en aucune façon assurée de leur exactitude. :-) Utilisez :break ModuleName line-number column-number pour l'essayer.