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
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.
4 votes
Plus précisément "Pour toute catégorie C, la catégorie [C,C] de ses endofoncteurs a une structure monoïde induite par la composition. Un objet monoïde dans [C,C] est une monade sur C." - extrait de en.wikipedia.org/wiki/Monoid_%28category_theory%29. Voir en.wikipedia.org/wiki/Monad_%28category_theory%29 pour la définition de monade dans la théorie des catégories.
1 votes
J'ai passé plus d'un an à réfléchir à Haskell et je n'arrive toujours pas à comprendre avec certitude ce qu'est un foncteur (est-ce un objet de fonction ? un objet sur lequel on peut mapper ? une fonction prenant a et retournant M a ? Une fonction binaire prenant a et retournant M a ? Comment peut-on mapper sur une fonction si elle n'a pas d'éléments sur lesquels itérer...) Sans parler de ce qu'est un endofuncteur. Je comprends que fmap vous permet d'appliquer une fonction sur un objet boxé, et >>= vous permet de pousser un objet boxé de M dans une fonction a -> M a, mais quoi maintenant ?
2 votes
@Dmitry A foncteur est une fonction entre catégories, avec certaines contraintes pour être bienveillant. Un endofoncteur sur une catégorie C est juste un foncteur de C vers elle-même. Functeur de données est une classe de type pour les endofoncteurs sur le modèle Catégorie Hask . Puisqu'une catégorie est constituée d'objets et de morphismes, un foncteur doit mettre en correspondance les deux. Pour une instance f de Data.Functor, la carte sur les objets (types haskell) est f lui-même et la carte sur les morphismes (fonctions haskell) est fmap.
1 votes
Voir ici pour une explication précise mais humaine : stackoverflow.com/questions/2704652/
1 votes
Voir la brillante série de conférences de Bartosz Milewski La théorie des catégories pour les programmeurs pour l'histoire complète. Tout au long de cet ouvrage, Bartosz établit les conditions préalables requises en théorie des catégories, en faisant toujours le lien avec Haskell. La dernière partie s'appelle en fait Monoïde dans la catégorie des endofoncteurs et répond pleinement à la question.
0 votes
On a l'impression que les mathématiciens, qui ont inventé ce terme, n'ont jamais pensé aux concepts qui se cachent derrière ces termes au départ. Ils ont pensé à un problème particulier et lui ont donné un nom. Les définitions de ce type reflètent rarement les idées sous-jacentes. Je crois qu'une bonne définition est toujours précédée d'un contexte et de termes liés.