Goto in Haskell: Quelqu'un peut-il expliquer cet effet apparemment insensé de l'utilisation continue de la monade?

Question

À partir de ce fil (de Contrôle.Monade.Suite plaisir, 2005), Tomasz Zielonka introduit une fonction (a commenté dans un style clair et agréable manière de Thomas Jäger). Tomasz prend l'argument (une fonction) d'un callCC corps et la retourne pour une utilisation ultérieure avec les deux définitions suivantes:

import Control.Monad.Cont
...
getCC :: MonadCont m => m (m a)
getCC = callCC (\c -> let x = c x in return x)

getCC' :: MonadCont m => a -> m (a, a -> m b)
getCC' x0 = callCC (\c -> let f x = c (x, f) in return (x0, f))

Ceux-ci sont également mentionnés dans Haskellwiki. En les utilisant, vous pouvez ressembler à goto sémantique en haskell qui a l'air vraiment cool:

import Control.Monad.Cont

getCC' :: MonadCont m => a -> m (a, a -> m b)
getCC' x0 = callCC (\c -> let f x = c (x, f) in return (x0, f))

main :: IO ()
main = (`runContT` return) $ do
    (x, loopBack) <- getCC' 0
    lift (print x)
    when (x < 10) (loopBack (x + 1))
    lift (putStrLn "finish")

Ce imprime les numéros de 0 à 10.

Voici le point intéressant. J'ai utilisé cette collaboration avec l'Écrivain Monade résoudre un certain problème. Mon code ressemble à ce qui suit:

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}

import Control.Monad.Cont
import Control.Monad.Writer

getCC :: MonadCont m => m (m a)
getCC = callCC (\c -> let x = c x in return x)

getCC' :: MonadCont m => a -> m (a, a -> m b)
getCC' x0 = callCC (\c -> let f x = c (x, f) in return (x0, f))

-- a simple monad transformer stack involving MonadCont and MonadWriter
type APP= WriterT [String] (ContT () IO)

runAPP :: APP a -> IO ()
runAPP a= runContT (runWriterT a) process
      where process (_,w)= do
               putStrLn $ unlines w
               return ()

driver :: Int -> APP ()
driver k = do
   tell [ "The quick brown fox ..." ]
   (x,loop) <- getCC' 0
   collect x
   when (x<k) $ loop (x+1) 

collect :: Int -> APP ()
collect n= tell [ (show n) ] 

main :: IO ()
main = do
   runAPP $ driver 4

Lorsque vous compilez et exécutez ce code, le résultat est:

The quick brown fox ...
4

Les chiffres de zéro à trois en cas d'ingestion de quelque part dans l'obscurité profonde de cet exemple.

Maintenant, dans le "Monde Réel Haskell" O'Sullivan, Goerzen et Stewart unis

"L'empilage monade transformateurs est analogue à la composition de fonctions. Si on change l'ordre dans lequel on applique des fonctions et ensuite obtenir des résultats différents, nous ne serons pas surpris. C'est donc avec une monade transformateurs, trop." (Real World Haskell, 2008, P. 442)

Je suis venu avec l'idée d'intervertir les transformateurs ci-dessus:

--replace in the above example
type APP= ContT () (WriterT [String] IO)
...
runAPP a = do
    (_,w) <- runWriterT $ runContT a (return . const ())
    putStrLn $ unlines w

Toutefois, cela ne compile pas car il n'existe pas de définition d'instance pour MonadWriter dans le Contrôle.Monade.Suite (c'est pourquoi j'ai récemment demandé à cette question.)

Nous avons ajouter une instance laissant écouter et passer undefined:

instance (MonadWriter w m) => MonadWriter w (ContT r m) where
  tell = lift . tell
  listen = undefined
  pass = undefined

Ajouter ces lignes, le compiler et l'exécuter. Tous les numéros sont imprimés.

Ce qui s'est passé dans l'exemple précédent?

Answer 1

Voici un peu informel réponse, mais je l'espère utile. getCC' renvoie une continuation au point en cours d'exécution; vous pouvez penser que l'enregistrement d'un cadre de pile. La poursuite retourné par getCC' a non seulement ContTs'etat au moment de l'appel, mais aussi l'état de monade ci-dessus ContT sur la pile. Lors de la restauration de cet état par l'appel de la poursuite, de toutes les monades construite au-dessus d' ContT de retour à leur état au moment de l' getCC' appel.

Dans le premier exemple, vous utilisez type APP= WriterT [String] (ContT () IO), avec IO de la base de l'errance, alors ContT, et, enfin, WriterT. Ainsi, lorsque vous appelez loop, l'état de l'écrivain est déroulé à ce qu'elle était à l' getCC' appel, car l'écrivain est au-dessus de ContT sur la monade de la pile. Lorsque vous passez ContT et WriterT, maintenant la suite seulement se déroule à l' ContT monade parce que c'est plus haut que l'écrivain.

ContT n'est pas la seule monade transformateur qui peuvent provoquer des problèmes de ce genre. Voici un exemple d'une situation similaire avec ErrorT

func :: Int -> WriterT [String] (ErrorT String IO) Int
func x = do
  liftIO $ print "start loop"
  tell [show x]
  if x < 4 then func (x+1)
    else throwError "aborted..."

*Main> runErrorT $ runWriterT $ func 0
"start loop"
"start loop"
"start loop"
"start loop"
"start loop"
Left "aborted..."

Même si l'écrivain monade disait valeurs, ils sont tous jetés quand l'intérieure ErrorT monade est exécuté. Mais si nous changer l'ordre de la transformers:

switch :: Int -> ErrorT String (WriterT [String] IO) () 
switch x = do
  liftIO $ print "start loop"
  tell [show x]
  if x < 4 then switch (x+1)
    else throwError "aborted..."

*Main> runWriterT $ runErrorT $ switch 0
"start loop"
"start loop"
"start loop"
"start loop"
"start loop"
(Left "aborted...",["0","1","2","3","4"])

Ici, l'état interne de l'écrivain monade est conservée, car il est inférieur ErrorT sur la monade de la pile. La grande différence entre ErrorT et ContT que ErrorTs'type indique clairement que tous les calculs partiels seront rejetées si une erreur est renvoyée.

Il est certainement plus simple de raisonner sur ContT quand il est au sommet de la pile, mais il est parfois utile d'être en mesure de se détendre une monade à un point connu. Un type d'opération peut être mise en œuvre de cette manière, par exemple.

Answer 2

J'ai passé un certain temps à suivre ce dans le λ calcul. Il a généré des pages et des pages de calculs que je ne reproduirai pas ici, mais je n'ai gagner un peu d'un aperçu sur la façon dont la monade pile fonctionne. Votre type se développe comme suit:

type APP a = WriterT [String] (ContT () IO) a
           = ContT () IO (a,[String])
           = ((a,[String]) -> IO()) -> IO()

Vous pouvez même étendre l'Écrivain return, >>=, et tell, avec Suite de l' return, >>=, et callCC. Traçage, il est extrêmement fastidieux mais.

L'effet de l'appel loop dans le pilote est à abandonner la poursuite normale et au lieu de retour, à nouveau, à partir de l'appel à getCC'. Qui a abandonné la poursuite contenait le code qui aurait ajouté l'actuel x à la liste. Donc, au lieu de cela, on répète la boucle, mais maintenant, x est le numéro suivant, et seulement lorsque nous avons atteint le dernier numéro (et donc de ne pas abandonner la poursuite) ne nous rassembler la liste d' ["The quick brown fox"] et ["4"].

Tout comme le "Real World Haskell", souligne que la IO monade doit rester sur le bas de la pile, il semble également important que la continuation de la monade reste sur le dessus.