893 votes

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

Qui a dit le premier ce qui suit ?

Une monade est juste 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, pouvez-vous donner une explication (en espérant qu'elle puisse être comprise par quelqu'un qui n'a pas beaucoup d'expérience en Haskell) ?

22 votes

Voir "Catégories pour le mathématicien qui travaille".

35 votes

Vous n'avez pas besoin de comprendre cela pour utiliser les monades en Haskell. D'un point de vue pratique, elles ne sont qu'un moyen astucieux de faire circuler un "état" par le biais d'une plomberie souterraine.

3 votes

J'aimerais ajouter cet excellent article de blog ici aussi : stephendiehl.com/posts/monades.html Il ne répond pas directement à la question, mais à mon avis, Stephen fait un superbe travail pour relier les catégories et les monades en Haskell. Si vous avez lu les réponses ci-dessus, cela devrait vous aider à unifier les deux façons de voir les choses.

947voto

pelotom Points 14817

Cette phrase particulière est de James Iry, tirée de son très divertissant ouvrage Une histoire brève, incomplète et surtout erronée des langages de programmation dans lequel il l'attribue fictivement à Philip Wadler.

La citation originale est de Saunders Mac Lane dans Catégories pour le mathématicien qui travaille un des textes fondateurs de la théorie des catégories. Le voici dans son contexte qui est probablement le meilleur endroit pour apprendre ce que cela signifie exactement.

Mais, je vais tenter le coup. La phrase originale est la suivante :

En somme, une monade dans X est simplement un monoïde dans la catégorie des endofoncteurs de X, le produit × étant remplacé par la composition d'endofoncteurs et l'ensemble unitaire par l'endofoncteur d'identité.

X voici une catégorie. Les endofoncteurs sont des foncteurs d'une catégorie vers elle-même (qui est habituellement tous Functor en ce qui concerne les programmeurs fonctionnels, puisqu'ils n'ont affaire qu'à une seule catégorie : la catégorie des types - mais je m'égare). Mais vous pouvez imaginer une autre catégorie qui est la catégorie des "endofoncteurs sur X ". C'est une catégorie dans laquelle les objets sont des endofoncteurs et les morphismes sont des transformations naturelles.

Et parmi ces endofoncteurs, certains peuvent être des monades. Lesquels sont des monades ? Exactement ceux qui sont monoidal dans un sens particulier. Au lieu d'expliquer le passage exact des monades aux monoïdes (Mac Lane le fait bien mieux que je ne pourrais le faire), je vais simplement 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 tous les a , b y c en S
  • e - a = a - e = a pour tous les a en S

Une monade est...

  • Un endofuncteur, T : X X (en Haskell, un constructeur de type de type * -> * avec un Functor instance)
  • Une transformation naturelle, : T × T T , donde × signifie la composition du foncteur ( est connu sous le nom de join en Haskell)
  • Une transformation naturelle, : I T , donde I est l'endofoncteur d'identité sur X ( est connu sous le nom de return en Haskell)

...satisfaisant à ces lois :

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

En plissant les yeux, vous pouvez voir que ces deux définitions sont des instances de la même concept abstrait .

24 votes

Merci pour l'explication et merci pour l'article Brief, Incomplete and Mostly Wrong History of Programming Languages. J'ai pensé que ça pouvait venir de là. C'est vraiment l'un des plus grands morceaux d'humour de programmation.

1 votes

Cette explication est fantastique, mais j'ai une question. J'ai compris que le produit monoïdal est de type S × S -> S mais c'est un autre exemple de ce que × est, en dehors du contexte de la composition de foncteurs ? Par exemple, pourrait être une multiplication ou une addition dans les nombres naturels ; ce qui est × dans ce contexte ?

9 votes

@Jonathan : Dans la formulation classique d'un monoïde, × désigne le produit cartésien d'ensembles. Vous pouvez en savoir plus à ce sujet ici : fr.wikipedia.org/wiki/Cartesian_product mais l'idée de base est qu'un élément de S × T est une paire (s, t) , donde s S y t T . Ainsi, la signature du produit monoïdal - : S × S -> S dans ce contexte, signifie simplement une fonction qui prend 2 éléments de S en entrée et produit un autre élément de S comme sortie.

527voto

misterbee Points 2523

Intuitivement, je pense que ce que le vocabulaire mathématique sophistiqué veut dire, c'est :

Monoïde

A monoïde est un ensemble d'objets, et une méthode pour les combiner. Les monoïdes les plus connus sont :

  • les chiffres que vous pouvez ajouter
  • vous pouvez concaténer des listes
  • sets you can union"

    Il existe également des exemples plus complexes.

De plus, chaque monoïde a un identité Il s'agit de l'élément "no-op" qui n'a aucun effet lorsque vous le combinez avec quelque chose d'autre :

  • 0 + 7 \== 7 + 0 \== 7
  • [] ++ [1,2,3] \== [1,2,3] ++ [] \== [1,2,3]
  • {} syndicat {pomme} \== {pomme} syndicat {} \== {pomme}

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 changez pas l'ordre gauche-droite des objets) L'addition est acceptable ((5+3)+1 == 5+(3+1)), mais pas la soustraction ((5-3)-1 != 5-(3-1)).

Monade

Considérons maintenant un type particulier d'ensemble et une façon particulière de combiner des objets.

Objets

Supposons que votre ensemble contienne des objets d'un type particulier : fonctions . Et ces fonctions ont une signature intéressante : Elles ne transportent pas les nombres vers les nombres, ni les chaînes de caractères vers les chaînes de caractères. Chaque fonction transporte un nombre vers une liste de nombres, selon un processus en deux étapes.

  1. Calculer 0 ou plusieurs résultats
  2. Combinez ces résultats en une seule réponse d'une manière ou d'une autre.

Exemples :

  • 1 -> [1] (il suffit d'envelopper l'entrée)
  • 1 -> [] (rejette l'entrée, emballe le néant dans une liste)
  • 1 -> [2] (ajoute 1 à l'entrée, et enroule le résultat)
  • 3 -> [4, 6] (ajoutez 1 à l'entrée, multipliez l'entrée par 2 et enroulez la valeur résultats multiples )

Combinaison d'objets

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

  • 1 -> [1] -> [[1]] (enveloppe l'entrée, deux fois)
  • 1 -> [] -> [] (écarte l'entrée, enroule le néant dans une liste, deux fois)
  • 1 -> [2] -> [ UH-OH ! ] (on ne peut pas "ajouter 1" à une liste !")
  • 3 -> [4, 6] -> [ UH-OH ! ] (on ne peut pas ajouter 1 une liste !)

Sans entrer dans la théorie des types, le point 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. (Fonction de type a -> a va composer, mais a-> [a] ne le fera pas.)

Définissons donc une autre façon de combiner les fonctions. Lorsque nous combinons deux de ces fonctions, nous ne voulons pas que les résultats soient "doublement enveloppés".

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 en appliquant G à chacun des résultats de F séparément, ce qui donne une collection de collections 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" la fonction :

  • 1 -> [1] -> [1] (enveloppe l'entrée, deux fois)
  • 1 -> [] -> [] (écarte l'entrée, enroule le néant dans une liste, deux fois)
  • 1 -> [2] -> [ 3 ] (ajoutez 1, puis ajoutez encore 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 refaites tout cela aux deux résultats, et emballez les résultats finaux dans une liste).

Cette façon plus sophistiquée de combiner les fonctions es associatif (en suivant la façon dont la composition de fonctions est associative lorsque vous ne faites pas le truc d'enveloppement fantaisiste).

Lier tout ça ensemble,

  • une monade est une structure qui définit une manière de combiner (les résultats des) fonctions,
  • de la même manière qu'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 où il existe un "No-op" spécial qui peut être combiné avec n'importe quelle chose pour obtenir quelque chose d'inchangé.

Notes

Il existe de nombreuses façons d'"emballer" les résultats. Vous pouvez créer une liste, ou un ensemble, ou rejeter tous les résultats sauf le premier tout en notant s'il n'y a pas de résultats, attacher un sidecar d'état, imprimer un message de journal, etc, etc.

J'ai joué un peu avec les définitions, dans l'espoir de faire passer l'idée essentielle de manière intuitive.

J'ai simplifié un peu les choses en insistant sur le fait que notre monade opère sur des fonctions de type a -> [a] . En fait, les monades fonctionnent sur les fonctions de type a -> m b , mais la généralisation est une sorte de détail technique qui n'est pas l'idée principale.

104voto

Luis Casillas Points 11718

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

{-# LANGUAGE RankNTypes, TypeOperators #-}

import Control.Monad (join)

Parmi ceux-ci, RankNTypes est le seul qui soit absolument essentiel à ce qui suit. J'ai écrit une fois une explication de RankNTypes que certaines personnes semblent avoir trouvé utile Je vais donc m'y référer.

Citation : L'excellente réponse de Tom Crockett nous avons :

Une monade est...

  • Un endofuncteur, T : X -> X
  • Une transformation naturelle, : T × T -> T , donde × signifie la composition du foncteur
  • Une transformation naturelle, : I -> T , donde I est l'endofoncteur d'identité 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 la forme f :-> g est analogue à un type de fonction, mais au lieu d'y penser comme une fonction entre deux types (du genre * ), pensez-y comme un morphisme entre deux foncteurs (chacun de ces types * -> * ). 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, en Haskell, les transformations naturelles sont des fonctions d'un certain type f x à un autre type g x de sorte que le x La variable de type est "inaccessible" à l'appelant. Ainsi, par exemple, sort :: Ord a => [a] -> [a] ne peut pas être transformée en une transformation naturelle, parce qu'elle est "pointilleuse" sur les types que nous pouvons instancier pour a . Une façon intuitive que j'utilise souvent pour penser à cela est la suivante :

  • Un foncteur est un moyen d'opérer sur l'ensemble des éléments suivants contenido de quelque chose sans toucher le structure .
  • Une transformation naturelle est une manière d'opérer sur la structure de quelque chose sans le toucher ou le regarder contenido .

Maintenant que ce point est réglé, attaquons-nous aux clauses de la définition.

La première clause est "un endofuncteur", T : X -> X ." Eh bien, chaque Functor en Haskell est un endofoncteur dans ce qu'on appelle "la catégorie Hask", dont les objets sont des types Haskell (de type * ) et dont les morphismes sont des fonctions Haskell. Cela semble être une déclaration compliquée, mais c'est en fait une déclaration très triviale. Tout ce que cela signifie, c'est qu'un Functor f :: * -> * vous donne les moyens de construire un type f a :: * pour tout a :: * et une fonction fmap f :: f a -> f b de tout f :: a -> b et que ceux-ci obéissent aux lois des foncteurs.

Deuxième clause : le Identity en Haskell (qui est 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)

Donc la transformation naturelle : I -> T de la définition de Tom Crockett peut être écrite de cette façon pour n'importe quel Monad instance t :

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

Troisième clause : La composition de deux foncteurs en Haskell peut être définie de cette manière (qui est également fournie avec la plate-forme) :

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 s'écrire comme suit :

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ée à ses deux premiers paramètres) est associative, et que Identity est son élément d'identité. C'est-à-dire que les isomorphismes suivants existent :

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

Elles sont très faciles à prouver car Compose y Identity sont toutes deux définies comme newtype et les rapports Haskell définissent la sémantique de newtype comme un isomorphisme entre le type défini et le type de l'argument de la fonction newtype Le constructeur de données de l'entreprise. 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.

0 votes

Dans le Natural newtype, je n'arrive pas à comprendre ce que le (Functor f, Functor g) fait la contrainte. Pouvez-vous expliquer ?

0 votes

@dfeuer Il ne fait pas vraiment quelque chose d'essentiel.

1 votes

@LuisCasillas J'ai enlevé ceux-là. Functor contraintes puisqu'elles ne semblent pas nécessaires. Si vous n'êtes pas d'accord, n'hésitez pas à les rajouter.

26voto

Dmitri Zaitsev Points 1012

Les réponses données ici font un excellent travail de 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, pouvez-vous donner une explication (en espérant qu'elle puisse être comprise par quelqu'un qui n'a pas beaucoup d'expérience en Haskell) ?

Le point essentiel qui manque ici, c'est la notion différente de "monoïde", le soi-disant catégorisation plus précisément -- celui de monoïde dans une catégorie monoïde. Malheureusement, le livre de Mac Lane lui-même rend la situation très confuse :

Au total, une monade en X est juste un monoïde dans la catégorie des endofoncteurs de X avec le produit × remplacé par la composition d'endofoncteurs et l'ensemble unitaire par l'endofoncteur d'identité.

Confusion principale

Pourquoi est-ce que cela prête à confusion ? Parce que cela ne définit pas ce qu'est un "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 ainsi que le foncteur composition comme opération binaire et le foncteur identité comme unité monoïdale. Ce qui fonctionne parfaitement bien et transforme en monoïde tout sous-ensemble d'endofoncteurs qui contient le foncteur identité et est fermé par la composition de foncteurs.

Pourtant, ce n'est pas l'interprétation correcte, ce que le livre omet de préciser à ce stade. Une monade f est un Correction de endofuncteur, et non un sous-ensemble d'endofuncteurs fermés par composition. Une construction courante consiste à utiliser f a générer un monoïde en prenant l'ensemble de tous les k -compositions doubles f^k = f(f(...)) de f avec lui-même, y compris k=0 qui correspond à l'identité f^0 = id . Et maintenant l'ensemble S de tous ces pouvoirs pour tous k>=0 est en effet un monoïde "avec le produit × remplacé par la composition d'endofoncteurs et l'ensemble unitaire par l'endofoncteur identité".

Et pourtant :

  • Ce monoïde S peut être défini pour tout foncteur f ou même littéralement pour toute auto-carte de X . C'est le monoïde généré par f .
  • La structure monoidale de S donné par le foncteur composition et le foncteur identité n'a rien à voir avec f être ou ne pas être une monade.

Et pour rendre les choses encore plus confuses, la définition de "monoïde dans une catégorie monoïdale" vient plus tard dans le livre, comme vous pouvez le voir dans le document table des matières . Et pourtant, la compréhension de cette notion est absolument essentielle pour comprendre le lien avec les monades.

Catégories monoïdiennes (strictes)

En passant au chapitre VII sur les monoïdes (qui vient plus tard que le chapitre VI sur les monades), nous trouvons la définition de ce que l'on appelle les catégorie monoïdienne stricte comme triple (B, *, e) , donde B est une catégorie, *: B x B-> B a bifuncteur (foncteur par rapport à chaque composant avec l'autre composant fixé) et e est un objet unitaire dans B , satisfaisant les lois d'associativité et d'unité :

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

pour tout objet a,b,c de B et les mêmes identités pour tout morphisme a,b,c avec e remplacé par id_e le morphisme d'identité de e . Il est maintenant instructif d'observer que dans notre cas d'intérêt, où B est la catégorie des endofoncteurs de X avec des transformations naturelles comme morphismes, * la composition du foncteur et e le foncteur d'identité, toutes ces lois sont satisfaites, comme on peut le vérifier directement.

Ce qui vient après dans le livre, c'est la définition du "relaxé". catégorie monoïdienne où les lois ne sont valables que modulo certaines transformations naturelles fixes satisfaisant à ce que l'on nomme relations de cohérence ce qui n'est cependant pas important pour nos cas de catégories endofonctionnelles.

Monoïdes dans les catégories monoïdiennes

Enfin, dans la section 3 "Monoïdes" du chapitre VII, la définition proprement dite est donnée :

Un monoïde c dans une catégorie monoïdienne (B, *, e) est un objet de B avec deux flèches (morphismes)

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

ce qui rend 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 à join y return pour une monade. Le lien devient encore plus clair lorsque nous faisons la composition * plus explicite, en remplaçant c * c par c^2 , donde c est notre monade.

Enfin, remarquez que les 3 diagrammes commutatifs (dans la définition d'un monoïde dans une catégorie monoïdale) sont écrits pour des catégories monoïdales générales (non strictes), alors que dans notre cas, toutes les transformations naturelles faisant partie 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 endofoncteur, donc un objet dans la catégorie des endofoncteurs, où la monade join y return Les opérateurs satisfont à la définition de un monoïde dans cette catégorie monoïdale (stricte) particulière . Vice versa, tout monoïde dans la catégorie monoïdale des endofoncteurs est par définition un triplet (c, mu, nu) constitué d'un objet et de deux flèches, par exemple des transformations naturelles dans notre cas, satisfaisant les mêmes lois qu'une monade.

Enfin, notons la différence essentielle entre les monoïdes (classiques) et les monoïdes plus généraux des catégories monoïdales. Les deux flèches mu y nu ci-dessus ne sont plus une opération binaire et une unité dans un ensemble. Au lieu de cela, vous avez un endofuncteur fixe c . Le foncteur composition * 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 consisterait à comparer avec le monoïde standard C de toutes les auto-cartes d'un ensemble A où l'opération binaire est la composition, que l'on peut considérer comme une correspondance du produit cartésien standard C x C en C . En passant au monoïde catégorisé, nous remplaçons le produit cartésien x avec la composition du foncteur * et l'opération binaire est remplacée par la transformation naturelle mu de c * c a c qui est une collection des join opérateurs

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

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

return: T->c(T) 

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

0 votes

Alors quelle est votre réponse à la partie "est-ce vrai" de la question ? Est-il vrai qu'une monade est un monoïde dans la catégorie des endofoncteurs ? Et si oui, quelle est la relation entre la notion de monoïde de la théorie des catégories et un monoïde algébrique (un ensemble avec une multiplication associative et une unité) ?

2 votes

@AlexanderBelopolsky, techniquement, une monade est un monoïde dans la catégorie monoïdienne des endofoncteurs équipée de la composition du foncteur comme son produit. En revanche, les "monoïdes algébriques" classiques sont des monoïdes dans la catégorie monoïdale des ensembles équipés du produit cartésien comme produit. Ainsi, les deux sont des cas spécifiques de la même définition catégorielle générale du monoïde.

9voto

Edmund's Echo Points 124

Je suis venu à ce post pour mieux comprendre la déduction de la fameuse citation de Mac Lane. La théorie des catégories pour le mathématicien de terrain .

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

Le fait que Mac Lane utilise cette description pour décrire un monade, on pourrait en déduire qu'elle décrit quelque chose d'unique aux monades. Soyez indulgent avec moi. Pour développer une compréhension plus large de l'énoncé, je crois qu'il faut préciser qu'il est no décrivant quelque chose qui est unique aux monades ; l'énoncé décrit également les Applicatifs et les Flèches parmi d'autres. Pour la même raison que nous pouvons avoir deux monoïdes sur Int (Somme et Produit), nous pouvons avoir plusieurs monoïdes sur X dans la catégorie des endofoncteurs. Mais les similitudes ne s'arrêtent pas là.

Monad et Applicative répondent tous deux à ces critères :

  • endo => toute flèche, ou morphisme qui commence et se termine au même endroit

  • foncteur => toute 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 ; ainsi, nous ne pouvons pas avoir Tree -> List seulement List -> List .

La déclaration utilise "Catégorie de..." Cela définit la portée de l'énoncé. Par exemple, le foncteur Category décrit la portée de f * -> g * c'est-à-dire, Any functor -> Any functor par exemple, Tree * -> List * o Tree * -> Tree * .

Ce qu'une déclaration catégorique ne spécifie pas décrit où tout et n'importe quoi est permis .

Dans ce cas, à l'intérieur des foncteurs, * -> * alias a -> b n'est pas spécifié, ce qui signifie que Anything -> Anything including Anything else . Comme mon imagination saute à Int -> String, elle comprend aussi Integer -> Maybe Int ou encore Maybe Double -> Either String Int donde a :: Maybe Double; b :: Either String Int .

La déclaration se résume donc comme suit :

  • champ d'application du foncteur :: f a -> g b (c'est-à-dire de tout type paramétré à tout type paramétré)
  • endo + foncteur :: f a -> f b (c'est-à-dire d'un type paramétré au même type paramétré) ... dit autrement,
  • un monoïde dans la catégorie des endofoncteurs

Alors, où est la puissance 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 ), n'illustre pas que je suis autorisé à utiliser une flèche paramétrée avec tout nombre de valeurs monoïdes, de la un type d'objet autorisé dans Monoid. La définition endo, ~ flèche d'identité de l'équivalence ignore la fonction du foncteur valeur du type et à la fois le type et la valeur de la couche la plus interne, la couche "charge utile". Ainsi, l'équivalence renvoie true dans toute situation où les types functoriels correspondent (par ex, Nothing -> Just * -> Nothing est équivalent à Just * -> Just * -> Just * parce qu'ils sont tous deux Maybe -> Maybe -> Maybe ).

Sidebar : ~ outside est conceptuel, mais est le symbole le plus à gauche dans f a . Il décrit également ce que "Haskell" lit en premier (grande image) ; ainsi, Type est "extérieur" par rapport à un Type Value. La relation entre les couches (une chaîne de références) en programmation n'est pas facile à mettre en relation dans la catégorie. La catégorie des ensembles est utilisée pour décrire les types (Int, Strings, Maybe Int, etc.), qui inclut la catégorie des foncteurs (types paramétrés). La chaîne de référence : Type de foncteur, valeurs de foncteur (éléments de l'ensemble de ce foncteur, par exemple, Nothing, Just), et à leur tour, tout ce vers quoi chaque valeur de foncteur pointe. Dans les catégories, la relation est décrite différemment, par exemple, return :: a -> m a est considérée comme une transformation naturelle d'un foncteur à un autre foncteur, différente de tout ce qui a été mentionné jusqu'à présent.

Pour en revenir au fil conducteur, en somme, 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 ex, :: List ) ; statique
  • mais à l'intérieur, permet beaucoup de dynamique
    • un nombre quelconque de valeurs du même type (par exemple, Empty | ~NonEmpty) pour alimenter des fonctions de toute arité. Le produit tensoriel réduira n'importe quel nombre d'entrées à une seule valeur... pour la couche extérieure (~ fold qui ne dit rien sur la charge utile)
    • une gamme infinie de les deux le type et les valeurs de la couche la plus interne

En 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 l'on cherche à savoir s'il faut construire du code avec un contexte partagé pour supporter des calculs qui dépendent les uns des autres, ou des calculs qui peuvent être exécutés en parallèle, cette déclaration infâme, avec tout ce qu'elle décrit, n'est pas un contraste entre le choix des Applicatifs, des Flèches et des Monades, mais plutôt une description de combien ils sont identiques. Pour la décision à prendre, l'affirmation est discutable.

Ce point est souvent mal compris. La déclaration poursuit en décrivant join :: m (m a) -> m a comme produit tensoriel pour l'endofuncteur monoïdien. Cependant, il ne précise pas comment, dans le contexte de cet énoncé, (<*>) aurait également pu être choisi. Il s'agit véritablement d'un exemple de six/douzaine. La logique de combinaison des valeurs est exactement la même ; la même entrée génère la même sortie pour chacune d'entre elles (contrairement aux monoïdes Somme et Produit pour Int, qui génèrent des résultats différents lorsqu'ils combinent des 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 *

(<*>) y (>>=) les deux offrent un accès simultané aux deux m afin de calculer la valeur de retour unique. La logique utilisée pour calculer la valeur de retour est exactement la même. Si ce n'était de la forme différente des fonctions qu'ils paramètrent ( f :: a -> b contre k :: a -> m b ) et la position du paramètre avec le même type de retour du calcul (c'est-à-dire, a -> b -> b contre b -> a -> b pour chacun respectivement), je soupçonne que nous aurions pu paramétrer la logique monoïdale, le produit tensoriel, pour une réutilisation dans les deux définitions. Comme exercice pour faire le point, essayez d'implémenter ~t et vous obtenez (<*>) y (>>=) selon la façon dont vous décidez de le définir forall a b .

Si mon dernier point est au moins conceptuellement vrai, il explique alors la précise, et seule différence computationnelle 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, d'après ma propre expérience, la fameuse citation de Mac Lane m'a fourni un excellent mème "goto", une balise à laquelle je pouvais me référer tout en naviguant dans la catégorie pour mieux comprendre les idiomes utilisés en Haskell. Elle réussit à capturer l'étendue d'une puissante capacité de calcul rendue merveilleusement accessible en 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 transmettre ici. Tout ce qu'elle décrit s'avère être ce qui est similaire entre Applicative et Monads (et Arrows parmi d'autres). Ce qu'il ne dit pas est précisément la petite mais utile distinction entre eux.

- E

Prograide.com

Prograide est une communauté de développeurs qui cherche à élargir la connaissance de la programmation au-delà de l'anglais.
Pour cela nous avons les plus grands doutes résolus en français et vous pouvez aussi poser vos propres questions ou résoudre celles des autres.

Powered by:

X