Pourquoi les effets secondaires sont-ils modélisés comme des monades dans Haskell?

Quelqu'un pourrait-il expliquer pourquoi les calculs impurs dans Haskell sont modélisés comme des monades?

Je veux dire que la monade est juste une interface avec 4 opérations, alors quel était le raisonnement pour modéliser les effets secondaires?

Supposons qu'une fonction ait des effets secondaires. Si nous prenons tous les effets qu'elle produit comme paramètres d'entrée et de sortie, alors la fonction est pure pour le monde extérieur.

Donc, pour une fonction impure

f' :: Int -> Int

nous ajoutons le RealWorld à la considération

f :: Int -> RealWorld -> (Int, RealWorld)
-- input some states of the whole world,
-- modify the whole world because of the side effects,
-- then return the new world.

puis fest de nouveau pur. Nous définissons un type de données paramétré type IO a = RealWorld -> (a, RealWorld), nous n'avons donc pas besoin de taper RealWorld autant de fois, et pouvons simplement écrire

f :: Int -> IO Int

Pour le programmeur, manipuler directement un RealWorld est trop dangereux - en particulier, si un programmeur met la main sur une valeur de type RealWorld, il peut essayer de la copier , ce qui est fondamentalement impossible. (Pensez à essayer de copier tout le système de fichiers, par exemple. Où le mettrez-vous?) Par conséquent, notre définition d'E / S encapsule également les états du monde entier.

Composition des fonctions "impures"

Ces fonctions impures sont inutiles si nous ne pouvons pas les enchaîner. Considérer

getLine     :: IO String            ~            RealWorld -> (String, RealWorld)
getContents :: String -> IO String  ~  String -> RealWorld -> (String, RealWorld)
putStrLn    :: String -> IO ()      ~  String -> RealWorld -> ((),     RealWorld)

Nous voulons

• obtenir un nom de fichier depuis la console,
• lire ce fichier, et
• imprimer le contenu de ce fichier sur la console.

Comment le ferions-nous si nous pouvions accéder aux états du monde réel?

printFile :: RealWorld -> ((), RealWorld)
printFile world0 = let (filename, world1) = getLine world0
                       (contents, world2) = (getContents filename) world1 
                   in  (putStrLn contents) world2 -- results in ((), world3)

Nous voyons un modèle ici. Les fonctions sont appelées comme ceci:

...
(<result-of-f>, worldY) = f               worldX
(<result-of-g>, worldZ) = g <result-of-f> worldY
...

Nous pourrions donc définir un opérateur ~~~pour les lier:

(~~~) :: (IO b) -> (b -> IO c) -> IO c

(~~~) ::      (RealWorld -> (b,   RealWorld))
      ->                    (b -> RealWorld -> (c, RealWorld))
      ->      (RealWorld                    -> (c, RealWorld))
(f ~~~ g) worldX = let (resF, worldY) = f worldX
                   in g resF worldY

alors nous pourrions simplement écrire

printFile = getLine ~~~ getContents ~~~ putStrLn

sans toucher au monde réel.

"Impurification"

Supposons maintenant que nous voulions également mettre le contenu du fichier en majuscules. Les majuscules sont une fonction pure

upperCase :: String -> String

Mais pour entrer dans le monde réel, il doit renvoyer un fichier IO String. Il est facile de lever une telle fonction:

impureUpperCase :: String -> RealWorld -> (String, RealWorld)
impureUpperCase str world = (upperCase str, world)

Cela peut être généralisé:

impurify :: a -> IO a

impurify :: a -> RealWorld -> (a, RealWorld)
impurify a world = (a, world)

pour que impureUpperCase = impurify . upperCase, et nous pouvons écrire

printUpperCaseFile = 
    getLine ~~~ getContents ~~~ (impurify . upperCase) ~~~ putStrLn

_{(Remarque: normalement, nous écrivons getLine ~~~ getContents ~~~ (putStrLn . upperCase))}

Nous avons toujours travaillé avec des monades

Voyons maintenant ce que nous avons fait:

1. Nous avons défini un opérateur (~~~) :: IO b -> (b -> IO c) -> IO cqui enchaîne deux fonctions impures ensemble
2. Nous avons défini une fonction impurify :: a -> IO aqui convertit une valeur pure en valeur impure.

Maintenant nous faisons l'identification (>>=) = (~~~)et return = impurify, et voyons? Nous avons une monade.

Note technique

Pour s'assurer que c'est vraiment une monade, il y a encore quelques axiomes qui doivent également être vérifiés:

1. return a >>= f = f a

    impurify a                =  (\world -> (a, world))
   (impurify a ~~~ f) worldX  =  let (resF, worldY) = (\world -> (a, world )) worldX 
                                 in f resF worldY
                              =  let (resF, worldY) =            (a, worldX)       
                                 in f resF worldY
                              =  f a worldX

2. f >>= return = f

   (f ~~~ impurify) worldX  =  let (resF, worldY) = f worldX 
                               in impurify resF worldY
                            =  let (resF, worldY) = f worldX      
                               in (resF, worldY)
                            =  f worldX

3. f >>= (\x -> g x >>= h) = (f >>= g) >>= h

   Laissé comme exercice.

Quelqu'un pourrait-il expliquer pourquoi les calculs impurs dans Haskell sont modélisés comme des monades?

Cette question contient un malentendu généralisé. L'impureté et la Monade sont des notions indépendantes. L'impureté n'est pas modélisée par Monad. Au contraire, il existe quelques types de données, tels que IO, qui représentent un calcul impératif. Et pour certains de ces types, une infime fraction de leur interface correspond au modèle d'interface appelé "Monad". De plus, il n'y a pas d'explication pure / fonctionnelle / dénotative connue de IO(et il est peu probable qu'il y en ait une, compte tenu du but de "sin bin" de IO), bien qu'il y ait l'histoire communément racontée sur le fait d' World -> (a, World)être le sens de IO a. Cette histoire ne peut pas décrire avec vérité IO, carIOprend en charge la concurrence et le non-déterminisme. L'histoire ne fonctionne même pas pour les calculs déterministes qui permettent une interaction à mi-calcul avec le monde.

Pour plus d'explications, consultez cette réponse .

Edit : En relisant la question, je ne pense pas que ma réponse soit tout à fait sur la bonne voie. Les modèles de calcul impératif s'avèrent souvent être des monades, comme le disait la question. Le demandeur pourrait ne pas vraiment supposer que la monadicité permet en aucune façon la modélisation du calcul impératif.

Si je comprends bien, quelqu'un du nom d' Eugenio Moggi a d' abord remarqué qu'une construction mathématique auparavant obscure appelée «monade» pouvait être utilisée pour modéliser les effets secondaires dans les langages informatiques, et donc spécifier leur sémantique à l'aide du calcul Lambda. Lors du développement de Haskell, les calculs impurs étaient modélisés de diverses manières (voir l'article «hair shirt» de Simon Peyton Jones pour plus de détails), mais lorsque Phil Wadler a introduit les monades, il est rapidement devenu évident que c'était la réponse. Et le reste est de l'histoire.

Quelqu'un pourrait-il expliquer pourquoi les calculs impurs dans Haskell sont modélisés comme des monades?

Eh bien, parce que Haskell est pur . Vous avez besoin d'un concept mathématique pour faire la distinction entre les calculs impurs et les calculs purs au niveau du type et pour modéliser les flux de programme respectivement.

Cela signifie que vous devrez vous retrouver avec un type IO aqui modélise un calcul impur. Ensuite, vous devez savoir comment combiner ces calculs, qui s'appliquent en séquence ( >>=) et soulevez une valeur ( return) sont les plus évidents et les plus élémentaires.

Avec ces deux, vous avez déjà défini une monade (sans même y penser);)

De plus, les monades fournissent des abstractions très générales et puissantes , de sorte que de nombreux types de flux de contrôle peuvent être généralisés de manière pratique dans des fonctions monadiques telles que sequence, liftMou une syntaxe spéciale, ce qui fait que l'impureté n'est pas un cas si particulier.

Voir les monades dans la programmation fonctionnelle et le typage d'unicité (la seule alternative que je connaisse) pour plus d'informations.

Comme vous le dites, Monadc'est une structure très simple. La moitié de la réponse est: Monadest la structure la plus simple que nous pourrions éventuellement donner aux fonctions à effet secondaire et pouvoir les utiliser. Avec Monadnous pouvons faire deux choses: nous pouvons traiter une valeur pure comme une valeur à effet secondaire ( return), et nous pouvons appliquer une fonction à effet secondaire à une valeur à effet secondaire pour obtenir une nouvelle valeur à effet secondaire ( >>=). Perdre la capacité de faire l'une ou l'autre de ces choses serait paralysant, donc notre type d'effet secondaire doit être "au moins" Monad, et il s'avère que Monadc'est suffisant pour implémenter tout ce dont nous avons besoin jusqu'à présent.

L'autre moitié est: quelle est la structure la plus détaillée que nous pourrions donner aux «effets secondaires possibles»? On peut certainement penser à l'espace de tous les effets secondaires possibles comme un ensemble (la seule opération qui nécessite est l'appartenance). Nous pouvons combiner deux effets secondaires en les faisant l'un après l'autre, et cela donnera lieu à un effet secondaire différent (ou peut-être le même - si le premier était "éteindre l'ordinateur" et le second était "écrire un fichier", alors le résultat de la composition de ceux-ci est juste «ordinateur d'arrêt»).

Ok, alors que dire de cette opération? C'est associatif; c'est-à-dire que si nous combinons trois effets secondaires, l'ordre dans lequel nous effectuons la combinaison n'a pas d'importance. Si nous le faisons (écrire un fichier puis lire la socket) puis arrêter l'ordinateur, c'est la même chose que d'écrire un fichier alors (lire socket puis arrêter ordinateur). Mais ce n'est pas commutatif: ("write file" puis "delete file") est un effet secondaire différent de ("delete file" puis "write file"). Et nous avons une identité: l'effet secondaire spécial "pas d'effets secondaires" fonctionne ("pas d'effets secondaires" puis "supprimer le fichier" est le même effet secondaire que simplement "supprimer le fichier"). A ce stade, tout mathématicien pense "Groupe!" Mais les groupes ont des inverses, et il n'y a aucun moyen d'inverser un effet secondaire en général; "supprimer le fichier" est irréversible. Donc, la structure que nous avons laissée est celle d'un monoïde, ce qui signifie que nos fonctions à effet secondaire devraient être des monades.

Existe-t-il une structure plus complexe? Sûr! Nous pourrions diviser les effets secondaires possibles en effets basés sur le système de fichiers, effets basés sur le réseau et plus, et nous pourrions proposer des règles de composition plus élaborées qui préservent ces détails. Mais encore une fois, cela revient à: Monadest très simple et pourtant assez puissant pour exprimer la plupart des propriétés qui nous intéressent. (En particulier, l'associativité et les autres axiomes nous permettent de tester notre application par petits morceaux, avec la certitude que les effets secondaires de l'application combinée seront les mêmes que la combinaison des effets secondaires des pièces).

C'est en fait une manière assez claire de penser les E / S de manière fonctionnelle.

Dans la plupart des langages de programmation, vous effectuez des opérations d'entrée / sortie. Dans Haskell, imaginez écrire du code non pas pour effectuer les opérations, mais pour générer une liste des opérations que vous aimeriez faire.

Les monades sont juste une jolie syntaxe pour exactement cela.

Si vous voulez savoir pourquoi les monades par rapport à autre chose, je suppose que la réponse est que c'est le meilleur moyen fonctionnel de représenter les E / S auquel les gens pourraient penser lorsqu'ils fabriquaient Haskell.

AFAIK, la raison est de pouvoir inclure des contrôles d'effets secondaires dans le système de type. Si vous voulez en savoir plus, écoutez ces épisodes de SE-Radio : Episode 108: Simon Peyton Jones sur la programmation fonctionnelle et Haskell Episode 72: Erik Meijer sur LINQ

Ci-dessus, il y a de très bonnes réponses détaillées avec un fond théorique. Mais je veux donner mon avis sur la monade IO. Je ne suis pas programmeur de haskell expérimenté, donc peut-être est-ce assez naïf ou même faux. Mais je m'a aidé à gérer la monade IO dans une certaine mesure (notez que cela ne concerne pas d'autres monades).

Tout d'abord, je tiens à dire que cet exemple avec "le monde réel" n'est pas trop clair pour moi car nous ne pouvons pas accéder à ses états précédents (du monde réel). Peut-être que cela ne concerne pas du tout les calculs monades, mais cela est souhaité dans le sens de la transparence référentielle, qui est généralement présente dans le code haskell.

Nous voulons donc que notre langage (haskell) soit pur. Mais nous avons besoin d'opérations d'entrée / sortie car sans elles, notre programme ne peut pas être utile. Et ces opérations ne peuvent pas être pures de par leur nature. Donc, la seule façon de gérer cela, nous devons séparer les opérations impures du reste du code.

Ici la monade arrive. En fait, je ne suis pas sûr qu'il ne puisse exister d'autre construction avec des propriétés nécessaires similaires, mais le fait est que la monade a ces propriétés, donc elle peut être utilisée (et elle est utilisée avec succès). La principale propriété est que nous ne pouvons pas y échapper. L'interface Monad n'a pas d'opérations pour se débarrasser de la monade autour de notre valeur. D'autres monades (non IO) fournissent de telles opérations et permettent la correspondance de modèle (par exemple, Maybe), mais ces opérations ne sont pas dans l'interface monade. Une autre propriété requise est la capacité d'enchaîner les opérations.

Si nous réfléchissons à ce dont nous avons besoin en termes de système de types, nous arrivons au fait que nous avons besoin de type avec constructeur, qui peut être enroulé autour de n'importe quelle vallée. Le constructeur doit être privé, car nous interdisons de s'en échapper (c'est-à-dire la correspondance de motifs). Mais nous avons besoin d'une fonction pour mettre de la valeur dans ce constructeur (ici le retour vient à l'esprit). Et nous avons besoin du moyen d'enchaîner les opérations. Si nous y réfléchissons pendant un certain temps, nous arriverons au fait que l'opération de chaînage doit avoir le type >> = a. Donc, nous arrivons à quelque chose de très similaire à la monade. Je pense que si nous analysons maintenant des situations contradictoires possibles avec cette construction, nous arriverons à des axiomes monades.

Notez que cette construction développée n'a rien de commun avec l'impureté. Il n'a que des propriétés, que nous souhaitons avoir pour pouvoir faire face à des opérations impures, à savoir le non-échappement, le chaînage et un moyen d'entrer.

Maintenant, un certain ensemble d'opérations impures est prédéfini par la langue dans cette monade IO sélectionnée. Nous pouvons combiner ces opérations pour créer de nouvelles opérations impures. Et toutes ces opérations devront avoir IO dans leur type. Notez cependant que la présence d'E / S dans le type de certaines fonctions ne rend pas cette fonction impure. Mais si je comprends bien, c'est une mauvaise idée d'écrire des fonctions pures avec IO dans leur type, car c'était initialement notre idée de séparer les fonctions pures et impures.

Enfin, je veux dire que la monade ne transforme pas les opérations impures en opérations pures. Cela permet seulement de les séparer efficacement. (Je répète, que ce n'est que ma compréhension)