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

Chaque fois que quelqu’un promet “d’expliquer les monades“, mon intérêt est piqué, pour être remplacé par la frustration lorsque la prétendue “explication” est une longue liste d’exemples terminés par une remarque désinvolte selon laquelle “la théorie mathématique” idées “est” trop compliqué à expliquer à ce stade “.

Maintenant, je demande le contraire. J’ai une solide connaissance de la théorie des catégories et je n’ai pas peur de la poursuite des diagrammes, du lemme de Yoneda ou des foncteurs dérivés (et même sur les monades et les adjonctions au sens catégorique).

Quelqu’un pourrait-il me donner une définition claire et concise de ce qu’est une monade dans la functional programming? Le moins d’exemples est le mieux: parfois, un concept clair dit plus de cent exemples timides. Haskell ferait bien un langage de démonstration, même si je ne suis pas difficile.

En complément de la réponse de Carl, une monade dans Haskell est (théoriquement) ceci:

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

Notez que “bind” ( >>= ) peut être défini comme

 x >>= f = join (fmap fx) 

Selon le wiki Haskell

Une monade dans une catégorie C est un sortingple ( F : C → C, η: IdF , μ: FFF )

… avec quelques axiomes. Pour Haskell, fmap , return et join alignés avec F , η et μ, respectivement. ( fmap dans Haskell définit un foncteur). Si je ne me trompe pas, Scala appelle ces map , pure et join respectivement. (Scala appelle bind “flatMap”)

Cette question a quelques bonnes réponses: les monades comme adjonctions

Plus précisément, l’article de Derek Elkins intitulé «Calculer les monades avec théorie des catégories» dans TMR # 13 devrait avoir le type de construction que vous recherchez: http://www.haskell.org/wikiupload/8/85/TMR- Issue13.pdf

Enfin, et peut-être est-ce vraiment le plus proche de ce que vous recherchez, vous pouvez aller directement à la source et consulter les articles fondateurs de Moggi sur le sujet de 1988 à 1991: http://www.disi.unige.it/ personne / MoggiE / publications.html

Voir notamment “Notions of Computation and Monads”.


Je suis sûr que je suis trop concentré / imprécis:

Commencez par une catégorie Hask dont les objects sont de type Haskell et dont les morphismes sont des fonctions. Les fonctions sont également des objects dans Hask , tout comme les produits. Donc Hask est cartésien fermé. Présentez maintenant une flèche mappant chaque object de Hask à MHask qui est un sous-ensemble des objects de Hask . Unité! Ensuite, introduisez une flèche mappant chaque flèche sur Hask à une flèche sur MHask . Cela nous donne la carte et fait de MHask un MHask covariant. Présentez maintenant une flèche mappant chaque object de MHask généré à partir d’un object dans MHask (via l’unité) vers l’object dans MHask qui le génère. Joindre! Et à partir de là, MHask est une monade (et un endofuncteur monoïdal pour être plus précis).

Je suis sûr qu’il y a une raison pour laquelle ce qui précède est déficient, c’est pourquoi je vous dirais vraiment, si vous êtes à la recherche de formalisme, aux journaux de Moggi en particulier.

Ok, en utilisant la terminologie Haskell et des exemples …

Une monade, en functional programming, est un modèle de composition pour les types de données du type * -> * .

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

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

Un type de données est un monad s’il peut implémenter cette interface tout en satisfaisant trois conditions dans l’implémentation. Ce sont les “lois de la monade”, et je m’en remettrai à ces longues explications pour l’explication complète. Je résume les lois comme ” (>>= return) est une fonction d’identité et (>>=) est associative.” Ce n’est vraiment pas plus que ça, même si cela peut être exprimé plus précisément.

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

Cette explication est probablement plus courte que prévu. C’est parce que l’interface monad est vraiment très abstraite. Le niveau incroyable d’abstraction fait partie de la raison pour laquelle tant de choses différentes peuvent être modélisées comme des monades.

Ce qui est moins évident, c’est que, aussi abstraite que soit l’interface, elle permet de modéliser de manière générique tout modèle de stream de contrôle, quelle que soit l’implémentation réelle de monade. C’est pourquoi le package Control.Monad dans la bibliothèque de base de GHC a des combinateurs comme when , forever , etc. Et c’est pourquoi la capacité d’abstraction explicite sur toute implémentation monad est puissante, en particulier avec la prise en charge d’un système de types.

Vous devriez lire l’article d’Eugenio Moggi “Notions of Computations and Monads”, qui explique le rôle alors proposé des monades pour structurer la sémantique dénotationnelle des langages efficaces.

Il y a aussi une question connexe:

Références pour apprendre la théorie derrière les langages fonctionnels purs tels que Haskell?

Comme vous ne voulez pas de la main, vous devez lire des articles scientifiques, pas des réponses au forum ou des tutoriels.

Je ne sais pas vraiment de quoi je parle, mais voici ma prise:

Les monades sont utilisées pour représenter des calculs. Vous pouvez penser à un programme procédural normal, qui est essentiellement une liste d’instructions, en tant que groupe de calculs composés. Les monades sont une généralisation de ce concept, vous permettant de définir comment les déclarations sont composées. Chaque calcul a une valeur (il pourrait simplement être () ); la monade détermine simplement comment se comporte la valeur dans une série de calculs.

Est-ce que la notation est vraiment ce qui rend cela clair: il s’agit essentiellement d’un type spécial de langage basé sur des instructions qui vous permet de définir ce qui se passe entre les instructions. C’est comme si vous pouviez définir comment “;” travaillé en C-like languages.

Dans cette optique, toutes les monades que j’ai utilisées jusqu’à présent ont du sens: l’ State n’affecte pas la valeur mais met à jour une seconde valeur qui est transmise du calcul au calcul en arrière-plan; MaybeMaybe court-circuite la valeur si elle rencontre un Nothing ; List vous permet de faire passer un nombre variable de valeurs; IO vous permet de faire passer des valeurs impures de manière sûre. Les monades les plus spécialisées que j’ai utilisées comme les parsingurs Gen et Parsec sont également similaires.

J’espère que c’est une explication claire qui n’est pas complètement hors-base.

Une monade est un monoïde dans la catégorie des endofuncteurs, quel est le problème? .

Mis à part l’humour, je crois personnellement que les monades, telles qu’elles sont utilisées dans Haskell et la functional programming, sont mieux comsockets du sharepoint vue des monads-as-a-interface (comme dans les réponses de Carl et Dan) plutôt que des monads-as le sharepoint vue du terme-de-catégorie-théorie . Je dois avouer que je n’ai vraiment intériorisé toute la monade que lorsque je devais utiliser une bibliothèque monadique d’une autre langue dans un projet réel.

Vous mentionnez que vous n’avez pas aimé tous les tutoriels “beaucoup d’exemples”. Quelqu’un vous a-t-il déjà orienté vers le journal de l’ équipe Awkward ? Il se concentre sur la monade des OI, mais l’introduction donne une bonne explication technique et historique des raisons pour lesquelles le concept de monade a été adopté par Haskell.

Puisque vous comprenez les monades dans le sens de la théorie des catégories, j’interprète votre question comme concernant la présentation des monades dans la functional programming. Ainsi, ma réponse évite toute explication sur ce qu’est une monade, ou toute intuition sur sa signification ou son utilisation.

Réponse : Dans Haskell, une monade est présentée, dans une langue interne pour certaines catégories, comme des cartes (internalisées) d’un sortingple Kleisli.

Explication : Il est difficile d’être précis sur les propriétés de la “catégorie Hask “, et ces propriétés sont largement hors de propos pour comprendre la présentation des monades par Haskell. Au lieu de cela, pour cette discussion, il est plus utile de comprendre Haskell comme un langage interne pour certaines catégories C. Les fonctions de Haskell définissent les morphismes dans les types C et Haskell sont des objects dans C , mais la catégorie particulière dans laquelle ces définitions sont faites est sans importance.

Les types de données paramésortingques, par exemple les data F a = ... , sont des mappages d’objects , p.ex. F : | C | -> | | -> | C | .

La description habituelle d’une monade dans Haskell est sous la forme sortingple de Kleisli (ou extension de Kleisli ):

 class Monad m where return :: a -> ma (>>=) :: ma -> (a -> mb) -> mb 

où:

  • m est le mappage d’object m :| C | -> | | -> | C |
  • return est l’opération unitaire sur les objects
  • >>= (prononcé “bind” par Haskellers) est l’opération d’ extension sur les morphismes mais avec ses deux premiers parameters échangés (cf. signature habituelle de l’extension (-)* : (a -> mb) -> ma -> mb )

(Ces cartes sont elles-mêmes internalisées en tant que familles de morphismes en C , ce qui est possible puisque m :| C | -> | C | ).

Haskell’s do -notation (si vous l’avez rencontré) est donc un langage interne pour les catégories Kleisli.

La page wikibook Haskell a une bonne explication de base.