Qui a d'abord dit ce qui suit?

Une monade n'est qu'un monoïde dans la catégorie des endofoncteurs, quel est le problème?

Et sur une note moins importante, est-ce vrai et si oui, pourriez-vous donner une explication (si tout va bien une qui peut être comprise par quelqu'un qui n'a pas beaucoup d'expérience Haskell)?

Cette formulation particulière est de James Iry, tirée de son très divertissante brève, incomplète et surtout mauvaise histoire des langages de programmation , dans laquelle il l'attribue fictivement à Philip Wadler.

La citation originale est de Saunders Mac Lane dans les catégories pour le mathématicien de travail , l'un des textes fondamentaux de la théorie des catégories. Ici, c'est dans le contexte , ce qui est probablement le meilleur endroit pour apprendre exactement ce que cela signifie.

Mais je vais essayer. La phrase originale est la suivante:

Tout compte fait, une monade en X n'est qu'un monoïde dans la catégorie des endofoncteurs de X, avec le produit × remplacé par la composition des endofuncteurs et l'unité définie par l'identité endofuncteur.

X voici une catégorie. Endofunctors sont foncteurs d'une catégorie à lui - même (qui est habituellement tous Functor s pour autant que les programmeurs fonctionnels sont concernés, car ils sont la plupart du temps face à une seule catégorie, la catégorie des types - mais je me éloigne du sujet). Mais vous pourriez imaginer une autre catégorie qui est la catégorie des "endofoncteurs sur X ". Il s'agit d'une catégorie dans laquelle les objets sont des endofoncteurs et les morphismes sont des transformations naturelles.

Et parmi ces endofuncteurs, certains pourraient être des monades. Quelles sont les monades? Exactement ceux qui sont monoïdaux dans un sens particulier. Au lieu de préciser la correspondance exacte des monades aux monoïdes (puisque Mac Lane fait bien mieux que ce que je pouvais espérer), je vais juste mettre leurs définitions respectives côte à côte et vous laisser comparer:

Un monoïde est ...

• Un ensemble, S
• Une opération, •: S × S → S
• Un élément de S , e: 1 → S

... satisfaisant à ces lois:

• (a • b) • c = a • (b • c) , pour tout a , b et c dans S
• e • a = a • e = a , pour tout a dans S

Une monade c'est ...

• Un endofoncteur, T: X → X (dans Haskell, un constructeur de type de type * -> *avec une Functorinstance)
• Une transformation naturelle, μ: T × T → T , où × signifie la composition du foncteur ( μ est connu comme joindans Haskell)
• Une transformation naturelle, η: I → T , où I est l'endofoncteur d'identité sur X ( η est connu comme returndans Haskell)

... satisfaisant à ces lois:

• μ ∘ Tμ = μ ∘ μT
• μ ∘ Tη = μ ∘ ηT = 1 (la transformation naturelle de l'identité)

Avec un peu de strabisme, vous pourrez peut-être voir que ces deux définitions sont des instances du même concept abstrait .

Intuitivement, je pense que ce que le vocabulaire mathématique sophistiqué dit est que:

Monoïde

Un monoïde est un ensemble d'objets et une méthode pour les combiner. Les monoides bien connus sont:

• numéros que vous pouvez ajouter
• listes que vous pouvez concaténer
• ensembles que vous pouvez joindre

Il existe également des exemples plus complexes.

De plus, chaque monoïde a une identité , qui est cet élément "no-op" qui n'a aucun effet lorsque vous le combinez avec autre chose:

• 0 + 7 == 7 + 0 == 7
• [] ++ [1,2,3] == [1,2,3] ++ [] == [1,2,3]
• {} union {apple} == {apple} union {} == {apple}

Enfin, un monoïde doit être associatif . (vous pouvez réduire une longue chaîne de combinaisons comme vous le souhaitez, tant que vous ne modifiez pas l'ordre de gauche à droite des objets) L'addition est OK ((5 + 3) +1 == 5+ (3+ 1)), mais la soustraction ne l'est pas ((5-3) -1! = 5- (3-1)).

Monade

Maintenant, considérons un type spécial d'ensemble et une manière spéciale de combiner des objets.

Objets

Supposons que votre ensemble contienne des objets d'un type spécial: les fonctions . Et ces fonctions ont une signature intéressante: elles ne portent pas des nombres aux nombres ou des chaînes aux chaînes. Au lieu de cela, chaque fonction porte un numéro à une liste de numéros dans un processus en deux étapes.

1. Calculer 0 résultat ou plus
2. Combinez ces résultats en une seule réponse en quelque sorte.

Exemples:

• 1 -> [1] (juste envelopper l'entrée)
• 1 -> [] (ignorer l'entrée, envelopper le néant dans une liste)
• 1 -> [2] (ajoutez 1 à l'entrée et encapsulez le résultat)
• 3 -> [4, 6] (ajoutez 1 à l'entrée et multipliez l'entrée par 2 et encapsulez les résultats multiples )

Combiner des objets

De plus, notre façon de combiner les fonctions est spéciale. Un moyen simple de combiner une fonction est la composition : prenons nos exemples ci-dessus et composons chaque fonction avec elle-même:

• 1 -> [1] -> [[1]] (envelopper l'entrée, deux fois)
• 1 -> [] -> [] (jeter l'entrée, envelopper le néant dans une liste, deux fois)
• 1 -> [2] -> [UH-OH! ] (nous ne pouvons pas "ajouter 1" à une liste! ")
• 3 -> [4, 6] -> [UH-OH! ] (nous ne pouvons pas ajouter 1 liste!)

Sans trop entrer dans la théorie des types, le fait est que vous pouvez combiner deux entiers pour obtenir un entier, mais vous ne pouvez pas toujours composer deux fonctions et obtenir une fonction du même type. (Les fonctions de type a -> a composeront, mais pas a-> [a] .)

Définissons donc une manière différente de combiner les fonctions. Lorsque nous combinons deux de ces fonctions, nous ne voulons pas "envelopper" les résultats.

Voici ce que nous faisons. Lorsque nous voulons combiner deux fonctions F et G, nous suivons ce processus (appelé liaison ):

1. Calculez les "résultats" de F mais ne les combinez pas.
2. Calculez les résultats de l'application de G à chacun des résultats de F séparément, ce qui donne une collection de collection de résultats.
3. Aplatissez la collection à 2 niveaux et combinez tous les résultats.

Revenons à nos exemples, combinons (lions) une fonction avec elle-même en utilisant cette nouvelle façon de "lier" les fonctions:

• 1 -> [1] -> [1] (envelopper l'entrée, deux fois)
• 1 -> [] -> [] (jeter l'entrée, envelopper le néant dans une liste, deux fois)
• 1 -> [2] -> [3] (ajoutez 1, puis ajoutez à nouveau 1 et enveloppez le résultat.)
• 3 -> [4,6] -> [5,8,7,12] (ajoutez 1 à l'entrée et multipliez également l'entrée par 2, en conservant les deux résultats, puis recommencez avec les deux résultats, puis encapsulez la finale donne une liste.)

Cette façon plus sophistiquée de combiner des fonctions est associative (à la suite de la façon dont la composition des fonctions est associative lorsque vous ne faites pas de trucs sophistiqués).

Lier tout cela ensemble,

• une monade est une structure qui définit un moyen de combiner (les résultats de) fonctions,
• de façon analogue à la façon dont un monoïde est une structure qui définit une façon de combiner des objets,
• où la méthode de combinaison est associative,
• et là où il y a un "No-op" spécial qui peut être combiné avec n'importe quoi pour que quelque chose reste inchangé.

Remarques

Il existe de nombreuses façons de "boucler" les résultats. Vous pouvez faire une liste, ou un ensemble, ou supprimer tout sauf le premier résultat tout en notant s'il n'y a pas de résultats, attacher un side-car d'état, imprimer un message de journal, etc., etc.

J'ai joué un peu avec les définitions dans l'espoir de faire passer intuitivement l'idée essentielle.

J'ai un peu simplifié les choses en insistant pour que notre monade fonctionne sur des fonctions de type a -> [a] . En fait, les monades fonctionnent sur des fonctions de type a -> mb , mais la généralisation est une sorte de détail technique qui n'est pas le principal aperçu.

Tout d'abord, les extensions et bibliothèques que nous allons utiliser:

{-# LANGUAGE RankNTypes, TypeOperators #-}

import Control.Monad (join)

Parmi ceux-ci, RankNTypesc'est le seul qui est absolument essentiel à ce qui suit. J'ai écrit une fois une explication RankNTypesque certaines personnes semblent avoir trouvé utile , je vais donc y faire référence.

Citant l'excellente réponse de Tom Crockett , nous avons:

Une monade c'est ...

• Un endofuncteur, T: X -> X
• Une transformation naturelle, μ: T × T -> T , où × signifie la composition du foncteur
• Une transformation naturelle, η: I -> T , où I est l'endofoncteur identitaire sur X

... satisfaisant à ces lois:

• μ (μ (T × T) × T)) = μ (T × μ (T × T))
• μ (η (T)) = T = μ (T (η))

Comment traduire cela en code Haskell? Eh bien, commençons par la notion de transformation naturelle :

-- | A natural transformations between two 'Functor' instances.  Law:
--
-- > fmap f . eta g == eta g . fmap f
--
-- Neat fact: the type system actually guarantees this law.
--
newtype f :-> g =
    Natural { eta :: forall x. f x -> g x }

Un type de formulaire f :-> gest analogue à un type de fonction, mais au lieu de le considérer comme une fonction entre deux types (de type *), pensez-y comme un morphisme entre deux foncteurs (chacun de type * -> *). Exemples:

listToMaybe :: [] :-> Maybe
listToMaybe = Natural go
    where go [] = Nothing
          go (x:_) = Just x

maybeToList :: Maybe :-> []
maybeToList = Natural go
    where go Nothing = []
          go (Just x) = [x]

reverse' :: [] :-> []
reverse' = Natural reverse

Fondamentalement, dans Haskell, les transformations naturelles sont des fonctions d'un certain type f xà un autre type de g xsorte que la xvariable de type est "inaccessible" à l'appelant. Ainsi, par exemple, sort :: Ord a => [a] -> [a]ne peut pas être transformé en une transformation naturelle, car il est «difficile» de déterminer les types pour lesquels nous pouvons instancier a. Une manière intuitive que j'utilise souvent pour y penser est la suivante:

• Un foncteur est une façon d'opérer sur le contenu de quelque chose sans toucher à la structure .
• Une transformation naturelle est une façon d'opérer sur la structure de quelque chose sans toucher ni regarder le contenu .

Maintenant, avec cela à l'écart, abordons les clauses de la définition.

La première clause est «un endofoncteur, T: X -> X ». Eh bien, chacun Functordans Haskell est un endofoncteur dans ce que les gens appellent «la catégorie Hask», dont les objets sont des types Haskell (en quelque sorte *) et dont les morphismes sont des fonctions Haskell. Cela ressemble à une déclaration compliquée, mais elle est en fait très banale. Tout ce que cela signifie, c'est que cela Functor f :: * -> *vous donne les moyens de construire un type f a :: *pour tout a :: *et une fonction à fmap f :: f a -> f bpartir de tout f :: a -> b, et que ceux-ci obéissent aux lois du foncteur.

Deuxième clause: le Identityfoncteur dans Haskell (fourni avec la plate-forme, vous pouvez donc simplement l'importer) est défini de cette façon:

newtype Identity a = Identity { runIdentity :: a }

instance Functor Identity where
    fmap f (Identity a) = Identity (f a)

Ainsi, la transformation naturelle η: I -> T de la définition de Tom Crockett peut être écrite de cette façon pour n'importe quelle Monadinstance t:

return' :: Monad t => Identity :-> t
return' = Natural (return . runIdentity)

Troisième clause: La composition de deux foncteurs dans Haskell peut être définie de cette façon (qui est également fournie avec la plateforme):

newtype Compose f g a = Compose { getCompose :: f (g a) }

-- | The composition of two 'Functor's is also a 'Functor'.
instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose fga) = Compose (fmap (fmap f) fga)

Donc la transformation naturelle μ: T × T -> T de la définition de Tom Crockett peut être écrite comme ceci:

join' :: Monad t => Compose t t :-> t
join' = Natural (join . getCompose)

L'affirmation selon laquelle il s'agit d'un monoïde dans la catégorie des endofoncteurs signifie alors que Compose(partiellement appliqué uniquement à ses deux premiers paramètres) est associatif, et c'est Identityson élément d'identité. C'est-à-dire que les isomorphismes suivants sont valables:

• Compose f (Compose g h) ~= Compose (Compose f g) h
• Compose f Identity ~= f
• Compose Identity g ~= g

Ceux-ci sont très faciles à prouver car Composeet Identitysont tous deux définis comme newtype, et les rapports Haskell définissent la sémantique de newtypecomme un isomorphisme entre le type défini et le type de l'argument du newtypeconstructeur de données du. Ainsi, par exemple, prouvons Compose f Identity ~= f:

Compose f Identity a
    ~= f (Identity a)                 -- newtype Compose f g a = Compose (f (g a))
    ~= f a                            -- newtype Identity a = Identity a
Q.E.D.

Remarque: Non, ce n'est pas vrai. À un moment donné, il y avait un commentaire sur cette réponse de Dan Piponi lui-même disant que la cause et l'effet ici étaient exactement le contraire, qu'il avait écrit son article en réponse à la plaisanterie de James Iry. Mais il semble avoir été supprimé, peut-être par un ordre plus compulsif.

Voici ma réponse originale.

Il est tout à fait possible qu'Iry ait lu From Monoids to Monads , un article dans lequel Dan Piponi (sigfpe) dérive des monades de monoids à Haskell, avec beaucoup de discussions sur la théorie des catégories et une mention explicite de "la catégorie des endofoncteurs sur Hask ". Dans tous les cas, quiconque se demande ce que signifie pour une monade être un monoïde dans la catégorie des endofoncteurs pourrait bénéficier de la lecture de cette dérivation.

Je suis venu à ce poste pour mieux comprendre l'inférence de la citation infâme de la théorie des catégories de Mac Lane pour le mathématicien de travail .

Pour décrire ce qu'est quelque chose, il est souvent tout aussi utile de décrire ce qu'il n'est pas.

Le fait que Mac Lane utilise la description pour décrire une monade, cela pourrait impliquer qu'elle décrit quelque chose d'unique aux monades. Restez avec moi. Pour développer une compréhension plus large de la déclaration, je pense qu'il doit être clair qu'il ne décrit pas quelque chose qui est unique aux monades; la déclaration décrit également Applicative et Flèches entre autres. Pour la même raison, nous pouvons avoir deux monoïdes sur Int (Sum et Product), nous pouvons avoir plusieurs monoïdes sur X dans la catégorie des endofoncteurs. Mais il y a encore plus aux similitudes.

Monade et Applicative répondent aux critères:

• endo => n'importe quelle flèche ou morphisme qui commence et se termine au même endroit
• functor => n'importe quelle flèche ou morphisme entre deux catégories

  (par exemple, au jour le jour Tree a -> List b, mais dans la catégorie Tree -> List)

• monoïde => objet unique; c'est-à-dire, un seul type, mais dans ce contexte, uniquement en ce qui concerne la couche externe; donc, nous ne pouvons pas avoir Tree -> List, seulement List -> List.

L'instruction utilise "Category of ..." Ceci définit la portée de l'instruction. À titre d'exemple, la catégorie Functor décrit la portée de f * -> g *, c'est-à-dire Any functor -> Any functor, par exemple, Tree * -> List *ou Tree * -> Tree *.

Ce qu'un énoncé catégorique ne précise pas décrit où tout et n'importe quoi est autorisé .

Dans ce cas, à l'intérieur des foncteurs, * -> *aka a -> bn'est pas spécifié ce qui signifie Anything -> Anything including Anything else. Alors que mon imagination passe à Int -> String, il inclut également Integer -> Maybe Int, ou même Maybe Double -> Either String Intoù a :: Maybe Double; b :: Either String Int.

Donc, la déclaration se rassemble comme suit:

• portée du foncteur :: f a -> g b(c.-à-d. n'importe quel type paramétré vers n'importe quel type paramétré)
• endo + functor :: f a -> f b(c'est-à-dire n'importe quel type paramétré pour le même type paramétré) ... dit différemment,
• un monoïde dans la catégorie des endofoncteurs

Alors, où est le pouvoir de cette construction? Pour apprécier toute la dynamique, j'avais besoin de voir que les dessins typiques d'un monoïde (objet unique avec ce qui ressemble à une flèche d'identité, :: single object -> single object), ne parviennent pas à illustrer que je suis autorisé à utiliser une flèche paramétrée avec un certain nombre de valeurs monoïdes, à partir d' un objet de type autorisé dans Monoid. La définition de l'équivalence de la flèche d'identité endo, ~ ignore la valeur de type du foncteur ainsi que le type et la valeur de la couche la plus interne de "charge utile". Ainsi, l'équivalence revient truedans toute situation où les types fonctoriels correspondent (par exemple, Nothing -> Just * -> Nothingest équivalent à Just * -> Just * -> Just *parce qu'ils sont les deux Maybe -> Maybe -> Maybe).

Encadré: ~ l'extérieur est conceptuel, mais est le symbole le plus à gauche f a. Il décrit également ce que "Haskell" lit en premier (vue d'ensemble); donc Type est "extérieur" par rapport à une valeur de type. La relation entre les couches (une chaîne de références) en programmation n'est pas facile à relier dans Category. La catégorie d'ensemble est utilisée pour décrire les types (int, chaînes, peut-être int, etc.) qui inclut la catégorie de foncteur (types paramétrés). La chaîne de référence: type de foncteur, valeurs du foncteur (éléments de l'ensemble de ce foncteur, par exemple, rien, juste), et à son tour, tout le reste auquel chaque valeur du foncteur pointe. Dans la catégorie, la relation est décrite différemment, par exemple, return :: a -> m aest considérée comme une transformation naturelle d'un Functor à un autre Functor, différente de tout ce qui a été mentionné jusqu'à présent.

Revenant au fil principal, dans l'ensemble, pour tout produit tensoriel défini et une valeur neutre, l'énoncé finit par décrire une construction informatique étonnamment puissante née de sa structure paradoxale:

• à l'extérieur, il apparaît comme un seul objet (par exemple, :: List); statique
• mais à l'intérieur, permet beaucoup de dynamique
  • n'importe quel nombre de valeurs du même type (par exemple, Empty | ~ NonEmpty) comme fourrage à des fonctions de n'importe quelle arité. Le produit tensoriel réduira n'importe quel nombre d'entrées à une seule valeur ... pour la couche externe (~ foldqui ne dit rien sur la charge utile)
  • gamme infinie de fois le type et les valeurs pour la couche la plus intérieure

À Haskell, il est important de clarifier l'applicabilité de la déclaration. La puissance et la polyvalence de cette construction n'ont absolument rien à voir avec une monade en soi . En d'autres termes, la construction ne repose pas sur ce qui rend une monade unique.

Lorsque vous essayez de déterminer s'il faut créer du code avec un contexte partagé pour prendre en charge des calculs qui dépendent les uns des autres, par rapport aux calculs qui peuvent être exécutés en parallèle, cette infâme déclaration, avec autant qu'elle décrit, n'est pas un contraste entre le choix de Applicative, Flèches et Monades, mais est plutôt une description de combien ils sont les mêmes. Pour la décision à prendre, la déclaration est sans objet.

C'est souvent mal compris. La déclaration continue en décrivant join :: m (m a) -> m acomme le produit tensoriel pour l'endofoncteur monoïdal. Cependant, il ne précise pas comment, dans le contexte de cette déclaration, (<*>)aurait également pu être choisi. C'est vraiment un exemple de six / demi-douzaine. La logique de combinaison des valeurs est exactement la même; la même entrée génère la même sortie de chacun (contrairement aux monoïdes Sum et Product pour Int car ils génèrent des résultats différents lors de la combinaison Ints).

Donc, pour récapituler: Un monoïde dans la catégorie des endofoncteurs décrit:

   ~t :: m * -> m * -> m *
   and a neutral value for m *

(<*>)et les (>>=)deux fournissent un accès simultané aux deux mvaleurs afin de calculer la valeur de retour unique. La logique utilisée pour calculer la valeur de retour est exactement la même. S'il n'y avait pas les différentes formes des fonctions qu'ils paramètrent ( f :: a -> bcontre k :: a -> m b) et la position du paramètre avec le même type de retour du calcul (c'est-à-dire a -> b -> bcontre b -> a -> bpour chacun respectivement), je soupçonne que nous aurions pu paramétrer la logique monoïdale, la produit tensoriel, à réutiliser dans les deux définitions. Comme exercice pour faire le point, essayez de mettre en œuvre ~t, et vous vous retrouvez avec (<*>)et (>>=)selon la façon dont vous décidez de le définir forall a b.

Si mon dernier point est au minimum conceptuellement vrai, il explique alors la différence précise et unique de calcul entre Applicative et Monad: les fonctions qu'ils paramètrent. En d'autres termes, la différence est externe à l'implémentation de ces classes de type.

En conclusion, dans ma propre expérience, la citation infâme de Mac Lane a fourni un grand meme "goto", un poteau indicateur pour moi de référence tout en naviguant dans la catégorie pour mieux comprendre les idiomes utilisés dans Haskell. Il réussit à saisir l'étendue d'une puissante capacité de calcul rendue merveilleusement accessible dans Haskell.

Cependant, il y a de l'ironie dans la façon dont j'ai d'abord mal compris l'applicabilité de la déclaration en dehors de la monade, et ce que j'espère véhiculé ici. Tout ce qu'il décrit s'avère être ce qui est similaire entre Applicative et Monads (et Arrows entre autres). Ce qu'il ne dit pas, c'est précisément la petite mais utile distinction entre eux.

- E

Les réponses ici font un excellent travail dans la définition des monoïdes et des monades, mais elles ne semblent toujours pas répondre à la question:

Et sur une note moins importante, est-ce vrai et si oui, pourriez-vous donner une explication (si tout va bien une qui peut être comprise par quelqu'un qui n'a pas beaucoup d'expérience Haskell)?

Le nœud du problème qui manque ici est la notion différente de "monoïde", la soi-disant catégorisation plus précisément - celle de monoïde dans une catégorie monoïdale. Malheureusement, le livre de Mac Lane lui-même le rend très déroutant :

Tout compte fait, une monade Xest juste un monoïde dans la catégorie des endofuncteurs X, le produit étant ×remplacé par la composition des endofuncteurs et l'unité définie par l'identité endofuncteur.

Confusion principale

Pourquoi est-ce déroutant? Parce qu'il ne définit pas ce qui est "monoïde dans la catégorie des endofoncteurs" de X. Au lieu de cela, cette phrase suggère de prendre un monoïde à l' intérieur de l'ensemble de tous les endofoncteurs avec la composition du foncteur comme opération binaire et le foncteur d'identité comme unité monoïdale. Ce qui fonctionne parfaitement bien et transforme en monoïde tout sous-ensemble d'endofoncteurs contenant le foncteur d'identité et fermé sous la composition du foncteur.

Pourtant, ce n'est pas la bonne interprétation, que le livre ne précise pas à ce stade. Une Monade fest un endofoncteur fixe , pas un sous-ensemble d'endofoncteurs fermés sous composition. Une construction courante consiste à utiliser fpour générer un monoid en prenant l'ensemble des kcompositions -fold f^k = f(f(...))d' favec elle - même, y compris k=0qui correspond à l'identité f^0 = id. Et maintenant l'ensemble Sde tous ces pouvoirs pour tous k>=0est en effet un monoïde "avec le produit × remplacé par la composition des endofuncteurs et l'unité fixée par l'identité endofuncteur".

Et pourtant:

• Ce monoïde Speut être défini pour n'importe quel foncteur fou même littéralement pour toute auto-carte de X. C'est le monoïde généré par f.
• La structure monoïdale Sdonnée par la composition du foncteur et le foncteur d'identité n'a rien à voir avec le fait d' fêtre ou non une monade.

Et pour rendre les choses plus confuses, la définition de «monoïde dans la catégorie monoïdale» vient plus loin dans le livre comme vous pouvez le voir dans la table des matières . Et pourtant, comprendre cette notion est absolument essentiel pour comprendre le lien avec les monades.

Catégories (strictes) monoïdales

En allant au chapitre VII sur les monoïdes (qui vient après le chapitre VI sur les monades), nous trouvons la définition de la catégorie dite monoïdale stricte comme triple (B, *, e), où se Btrouve une catégorie, *: B x B-> Bun bifoncteur (foncteur par rapport à chaque composant avec un autre composant fixe) ) et eest un objet unité dans B, satisfaisant les lois d'associativité et d'unité:

(a * b) * c = a * (b * c)
a * e = e * a = a

pour tous les objets a,b,cde B, et les mêmes identités pour les morphismes a,b,cavec eremplacé par id_ele morphisme d'identité e. Il est maintenant instructif d'observer que dans notre cas d'intérêt, où Best la catégorie des endofoncteurs Xavec des transformations naturelles comme morphismes, *la composition du foncteur et ele foncteur identitaire, toutes ces lois sont satisfaites, comme on peut le vérifier directement.

Ce qui vient après dans le livre est la définition de la catégorie monoïdale "relaxée" , où les lois ne contiennent que des transformations naturelles fixes modulo satisfaisant les relations dites de cohérence , ce qui n'est cependant pas important pour nos cas des catégories d'endofoncteurs.

Monoïdes dans les catégories monoïdales

Enfin, dans la section 3 «Monoïdes» du chapitre VII, la définition actuelle est donnée:

Un monoïde cdans une catégorie monoïdale (B, *, e)est un objet Bà deux flèches (morphismes)

mu: c * c -> c
nu: e -> c

rendant 3 diagrammes commutatifs. Rappelons que dans notre cas, ce sont des morphismes dans la catégorie des endofoncteurs, qui sont des transformations naturelles correspondant précisément joinet returnpour une monade. La connexion devient encore plus claire lorsque nous rendons la composition *plus explicite, en la remplaçant c * cpar c^2, où cest notre monade.

Enfin, notez que les 3 diagrammes commutatifs (dans la définition d'un monoïde dans la catégorie monoïdale) sont écrits pour les catégories monoïdales générales (non strictes), alors que dans notre cas, toutes les transformations naturelles résultant de la catégorie monoïdale sont en fait des identités. Cela rendra les diagrammes exactement les mêmes que ceux de la définition d'une monade, rendant la correspondance complète.

Conclusion

En résumé, toute monade est par définition un endofuncteur, donc un objet dans la catégorie des endofuncteurs, où le monadique joinet les returnopérateurs satisfont à la définition d' un monoïde dans cette catégorie monoïdale particulière (stricte) . Réciproquement, tout monoïde de la catégorie des endofoncteurs monoïdes est par définition un triple (c, mu, nu)composé d'un objet et de deux flèches, par exemple des transformations naturelles dans notre cas, satisfaisant aux mêmes lois qu'une monade.

Enfin, notez la différence clé entre les monoïdes (classiques) et les monoïdes plus généraux dans les catégories monoïdales. Les deux flèches muet nuplus ne sont plus une opération binaire et une unité dans un ensemble. Au lieu de cela, vous avez un endofoncteur fixe c. La composition du foncteur *et le foncteur d'identité seuls ne fournissent pas la structure complète nécessaire à la monade, malgré cette remarque déroutante dans le livre.

Une autre approche serait de comparer avec la monoid norme Cde toutes les auto-cartes d'un jeu A, où l'opération binaire est la composition, qui peut être vu pour cartographier le produit standard cartésienne C x Cdans C. En passant au monoïde catégorisé, nous remplaçons le produit cartésien xpar la composition du foncteur *, et l'opération binaire est remplacée par la transformation naturelle mude c * cà c, c'est-à-dire un ensemble d' joinopérateurs

join: c(c(T))->c(T)

pour chaque objet T(taper en programmation). Et les éléments d'identité dans les monoïdes classiques, qui peuvent être identifiés avec des images de cartes à partir d'un ensemble fixe à un point, sont remplacés par la collection des returnopérateurs

return: T->c(T) 

Mais maintenant, il n'y a plus de produits cartésiens, donc pas de paires d'éléments et donc pas d'opérations binaires.