Qu'est-ce qu'une monade en PF, en termes catégoriques?

Question

Chaque fois que quelqu'un promet "d'expliquer monades", mon intérêt est piqué, pour être remplacés par de la frustration lorsque la prétendue "explication" est une longue liste d'exemples dénoncé par certains de la main gauche remarque que la "théorie mathématique" derrière le "ésotérique idées", "trop compliqué à expliquer à ce stade".

Maintenant je pose la question pour le contraire. J'ai une connaissance solide de la catégorie théorie, et je n'ai pas peur de diagramme de chasser, le lemme de Yoneda ou aux foncteurs dérivés (et même sur les monades et adjunctions dans les catégorique sens).

Quelqu'un pourrait-il me donner une claire et concise définition de ce qu'est une monade est dans la programmation fonctionnelle? Le moins d'exemples les mieux: parfois, un concept clair, dit plus d'une centaine de timides exemples. Haskell ferait bien comme une langue à des fins de démonstration si je ne suis pas pointilleux.

Answer 1

Cette question a quelques bonnes réponses: les Monades comme adjunctions

Plus au point, Derek Elkins "Calcul des Monades avec la Théorie de la Catégorie" article dans la RTM n ° 13 devrait avoir le genre de constructions que vous cherchez: http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

Enfin, et c'est peut-être vraiment la plus proche de ce que vous cherchez, vous pouvez aller directement à la source et de regarder Moggi séminal d'articles sur le thème de 1988-91: http://www.disi.unige.it/person/MoggiE/publications.html

Voir notamment "les Notions de calcul et de monades".

---

La mienne, je suis sûr que trop condensé/imprécis prendre:

Commencer avec une catégorie Hask dont les objets sont Haskell types, et dont morphisms sont des fonctions. Les fonctions sont aussi des objets en Hask, que sont produits. Donc, Hask est Cartésienne fermée. Maintenant introduire une flèche de mappage de chaque objet en Hask de MHask qui est un sous-ensemble des objets en Hask. L'unité de! Prochaine introduire une flèche de mappage de chaque flèche Hask d'une flèche MHask. Cela nous donne la carte, et fait MHask un covariant endofunctor. Maintenant introduire une flèche de mappage de chaque objet en MHask qui est généré à partir d'un objet en MHask (par unité) à l'objet en MHask qui le génère. Nous rejoindre! Et à partir de la que la, MHask est une monade (et un monoidal endofunctor pour être plus précis).

Pour être encore plus précis, MHask est une forte lax monoidal endofunctor, mais je n'ai pas envie de travailler, par le biais pourquoi ces deux premiers adjectifs sont importants pour le moment.

Je suis sûr qu'il ya une raison pourquoi les ci-dessus est insuffisante, c'est pourquoi j'aimerais vraiment directe-vous, si vous êtes à la recherche pour le formalisme, à la Moggi papiers en particulier.

Answer 2

Comme un compliment à Carl réponse, une Monade en Haskell est (théoriquement) ce:

class Monad m where
  join :: m (m a) -> m a
  return :: a -> m a
  fmap :: (a -> b) -> m a -> m b

Notez que "lier" (>>=) peut être définie comme

x >>= f = join (fmap f x)

Selon le Haskell Wiki

Une monade dans une catégorie C est une chambre triple (F : C → C, η : Id → F, m : F ∘ F → F)

...avec quelques axiomes. Pour Haskell, fmap, join, et return ligne avec F, η, et m, respectivement. (fmap en Haskell définit un Foncteur). Si je ne me trompe pas, Scala appelle ces map, join, et pure respectivement. (Scala appelle bind "flatMap")

Answer 3

Ok, à l'aide de Haskell terminologie et des exemples...

Une monade, dans la programmation fonctionnelle, est un modèle de composition pour les types de données avec l'aimable * -> *.

class Monad (m :: * -> *) where
    return :: a -> m a
    (>>=)  :: m a -> (a -> m b) -> m b

(Il y a plus de classe que dans Haskell, mais ce sont les parties importantes.)

Un type de données est une monade si elle peut implémenter cette interface, tout en satisfaisant les trois conditions de la mise en œuvre. Ce sont les "monade lois", et je vais le laisser à ceux de longue haleine explications pour l'explication complète. Je résume les lois "(>>= return) est une fonction d'identification, et (>>=) est associative." C'est vraiment pas plus que ça, même si elle peut être exprimée de manière plus précise.

Et c'est toute une monade est. Si vous pouvez implémenter cette interface, tout en préservant ces propriétés comportementales, vous avez une monade.

Cette explication est sans doute plus court que prévu. C'est parce que la monade de l'interface est vraiment très abstrait. L'incroyable niveau d'abstraction est une des raisons pour lesquelles beaucoup de choses différentes peuvent être modélisés comme des monades.

Ce qui est moins évident, c'est que, aussi abstrait que l'interface est, il permet de façon générique de modélisation de tout contrôle du flux, quel que soit l'effectif de l'errance de mise en œuvre. C'est pourquoi l' Control.Monad package dans GHC l' base bibliothèque a combinators comme when, forever, etc. Et c'est pourquoi explicitement la capacité de l'abstrait sur toute monade mise en œuvre est puissante, surtout avec l'appui d'un système de type.

Answer 4

Vous devriez lire le livre par Eugenio Moggi "Notions de calculs et des monades", qui permettent d'expliquer le rôle proposé de monades de structure denotational sémantique de effectful langues.

Il y a aussi une question connexe:

Références pour l'apprentissage de la théorie pure fonctionnels langages comme Haskell?

Comme vous ne voulez pas à la main en agitant, vous avez à lire des articles scientifiques, pas du forum des réponses ou des tutoriels.

Answer 5

Je ne sais pas vraiment de quoi je parle, mais voici mon point de vue:

Les monades sont utilisés pour représenter les calculs. Vous pouvez penser à une normale de procédure du programme, qui est en fait une liste de déclarations, comme un bouquet composé de calculs. Les monades sont une généralisation de ce concept, vous permettant de définir la façon dont les instructions composé. Chaque calcul a une valeur (il pourrait juste être ()); la monade juste détermine la valeur enfilées à travers une série de calculs se comporte.

Faire de la notation est vraiment ce qui fait de cette claire: il s'agit essentiellement d'un genre spécial de déclaration de base de la langue qui permet de définir ce qui se passe entre les états. C'est comme si vous pouviez définir comment ";" travaillé en C-comme les langues.

Dans cette lumière de toutes les monades j'ai utilisé jusqu'à présent fait sens: State n'affecte pas la valeur, mais les mises à jour une deuxième valeur qui est transmis de calcul pour le calcul en arrière-plan; Maybe court-circuits de la valeur que si elle rencontre jamais une Nothing; List vous permet d'avoir un nombre variable de valeurs transmises à travers; IO vous permet d'avoir impur des valeurs transmises par le biais de manière sûre. Le plus spécialisé monades j'ai utilisé comme Gen et Parsec analyseurs sont également similaires.

J'espère que c'est une explication claire qui n'est pas complètement hors de la base.