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


Qui a d'abord dit ce qui suit?

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

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


619
2017-10-06 06:55


origine


Réponses:


Ce phrasé particulier est par James Iry, de son très divertissant Brève, incomplète et surtout fausse histoire des langages de programmation, dans lequel il attribue fictivement à Philip Wadler.

La citation originale est de Saunders Mac Lane dans 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, qui est probablement le meilleur endroit pour apprendre exactement ce que cela signifie.

Mais, je vais prendre un coup de couteau. La phrase originale est la suivante:

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

X voici une catégorie. Endofunctors sont des foncteurs d'une catégorie à lui-même (qui est habituellement tout  Functors en ce qui concerne les programmeurs fonctionnels, puisqu'ils traitent principalement d'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 XC'est une catégorie dans laquelle les objets sont endofoncteurs et les morphismes sont des transformations naturelles.

Et de ces endofoncteurs, certains d'entre eux pourraient être des monades. Lesquels sont des monades? Juste ceux qui sont monoidal dans un sens particulier. Au lieu d'énoncer le mappage exact 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 permettre de 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 une, b et c dans S
  • e • a = a • e = a, pour tous une dans S

Une monade est ...

  • Un endofunctor, T: X → X (dans Haskell, un constructeur de type de type * -> * avec un Functor exemple)
  • Une transformation naturelle, μ: T × T → T, où × signifie la composition foncteur (également connu sous le nom join à Haskell)
  • Une transformation naturelle, η: I → T, où je est l'identité endofunctor sur X (aussi connu sous le nom return à Haskell)

... satisfaisant ces lois:

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

Avec un peu de strabisme, vous pourriez être en mesure de voir que ces deux définitions sont des instances de la même concept abstrait.


680
2017-10-06 07:35



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

Monoïde

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

  • numéros que vous pouvez ajouter
  • listes que vous pouvez concaténer
  • définit vous pouvez union

Il y a aussi des exemples plus complexes.

Plus loin, chaque Monoid a un 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]
  • {} syndicat {Pomme} == {Pomme} syndicat {} == {Pomme}

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

Monade

Maintenant, considérons 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 spécial: les fonctions. Et ces fonctions ont une signature intéressante: elles ne portent pas de nombres aux nombres ou de chaînes aux chaînes. Au lieu de cela, chaque fonction porte un nombre à une liste de nombres dans un processus en deux étapes.

  1. Calculer 0 ou plusieurs résultats
  2. Combinez ces résultats à 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] (ajouter 1 à l'entrée, et envelopper le résultat)
  • 3 -> [4, 6] (ajouter 1 à l'entrée, multiplier l'entrée par 2 et placer plusieurs résultats)

Combinaison d'objets

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

  • 1 -> [1] -> [[1]] (envelopper l'entrée, deux fois)
  • 1 -> [] -> [] (rejeter 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 une liste!)

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

Alors, définissons une autre façon de combiner les fonctions. Lorsque nous combinons deux de ces fonctions, nous ne voulons pas "doubler" les résultats.

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

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

Revenons à nos exemples, combinons (lions) une fonction avec elle-même en utilisant cette nouvelle manière de fonctions "binding":

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

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

L'attacher tous ensemble,

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

Remarques

Il y a beaucoup de façons de «boucler» les résultats. Vous pouvez faire une liste, ou un ensemble, ou jeter tout sauf le premier résultat 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 d'obtenir intuitivement l'idée essentielle.

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


463
2018-05-02 00:07



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 est absolument essentiel à la ci-dessous. J'ai écrit une fois une explication de RankNTypes que certaines personnes semblent avoir trouvé utile, donc je vais me référer à cela.

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

Une monade est ...

  • Un endofunctor, T: X -> X
  • Une transformation naturelle, μ: T × T -> T, où × signifie la composition foncteur
  • Une transformation naturelle, η: I -> T, où je est l'identité endofunctor sur X

... satisfaisant ces lois:

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

Comment traduisons-nous cela au code Haskell? Eh bien, commençons avec la notion d'un 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 :-> g est analogue à un type de fonction, mais au lieu d'y penser en tant que fonction entre deux les types (de genre *), pensez-y comme morphisme entre deux foncteurs (chacun de genre * -> *). 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 g x tel que le x type variable 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" sur quels types nous pouvons instancier pour a. Une façon intuitive que j'utilise souvent pour penser à ceci est la suivante:

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

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

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

Deuxième clause: la Identity fonctor dans Haskell (qui vient avec la plate-forme, donc vous pouvez 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 écrit de cette façon pour tout Monad exemple 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 vient aussi 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 être écrit comme ceci:

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

L'affirmation que c'est un monoïde dans la catégorie des endofoncteurs signifie alors que Compose (partiellement appliqué à seulement ses deux premiers paramètres) est associative, et que Identity est son é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

Ce sont très faciles à prouver parce que Compose et Identity sont définis comme newtype, et les rapports Haskell définissent la sémantique de newtype comme un isomorphisme entre le type étant défini et le type de l'argument à la newtypeLe constructeur de données. 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.

76
2017-09-16 06:58



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

Voici ma réponse originale.


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


5
2018-04-20 22:53



Je suis venu à ce poste pour mieux comprendre l'inférence de la citation infâme de Mac Lane Catégorie Théorie Pour le mathématicien de travail.

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

Le fait que Mac Lane utilise la description pour décrire une Monade, pourrait laisser entendre qu'il décrit quelque chose d'unique aux monades. Ours avec moi. Pour développer une compréhension plus large de la déclaration, je crois qu'il doit être clair qu'il est ne pas décrire quelque chose qui est unique aux monades; la déclaration décrit également Applicative et Arrows entre autres. Pour la même raison on peut avoir deux monoides sur Int (Somme et Produit), on peut avoir plusieurs monoides sur X dans la catégorie des endofoncteurs. Mais il y a encore plus de similitudes.

Monad et Applicative répondent aux critères:

  • endo => toute flèche, ou morphisme qui commence et se termine au même endroit
  • fonctor => 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; 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 permis.

Dans ce cas, à l'intérieur des foncteurs, * -> * alias a -> b n'est pas spécifié ce qui signifie Anything -> Anything including Anything else. Comme mon imagination saute à Int -> String, il comprend également Integer -> Maybe Int, ou même Maybe Double -> Either String Int où a :: Maybe Double; b :: Either String Int.

Donc, la déclaration se présente comme suit:

  • champ de foncteurs :: f a -> g b (c'est-à-dire, n'importe quel type paramétré vers n'importe quel type paramétré)
  • endo + foncteur :: f a -> f b (c'est-à-dire, n'importe quel type paramétré au même type paramétré) ... dit différemment,
  • un monoid dans la catégorie des endofunctor

Alors, où est la puissance de cette construction? Pour apprécier la dynamique complète, 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 montre pas que je suis autorisé à utiliser une flèche paramétrée avec n'importe quel chiffre des valeurs monoïdes, de la un type objet autorisé dans Monoid. L'endo, ~ définition de l'identité de l'équivalence ne tient pas compte le foncteur type valeur et à la fois le type et la valeur de la couche "charge utile" la plus interne. Ainsi, l'équivalence revient true dans toute situation où les types fonctoriaux correspondent (par exemple, Nothing -> Just * -> Nothing est équivalent à Just * -> Just * -> Just * parce qu'ils sont tous les 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); Le type est donc "extérieur" par rapport à une valeur de type. La relation entre les couches (une chaîne de références) dans la programmation n'est pas facile à relier dans la catégorie. La catégorie d'ensemble est utilisée pour décrire les types (Int, Strings, Maybe Int etc.) qui incluent la catégorie de Functor (Types paramétrés). La chaîne de référence: Type de Functor, Valeurs de Functor (éléments de cet ensemble de Functor, par exemple, Rien, Juste), et à leur tour, tout le reste de chaque valeur de foncteur. Dans la catégorie, la relation est décrite différemment, par exemple, return :: a -> m a est considéré comme une transformation naturelle d'un Functor à un autre Functor, différent de tout ce qui a été mentionné jusqu'ici.

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

  • à l'extérieur, il apparaît comme un objet unique (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 aux fonctions de n'importe quelle arité. Le produit tensoriel va réduire n'importe quel nombre d'entrées à une seule valeur ... pour la couche externe (~fold cela ne dit rien sur la charge utile)
    • gamme infinie de tous les deux le type et les valeurs de la couche la plus interne

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

En essayant de déterminer s'il faut construire du code avec un contexte partagé pour supporter des calculs qui dépendent les uns des autres, par rapport à des calculs qui peuvent être exécutés en parallèle, cette déclaration infâme, avec autant qu'elle décrit, n'est pas un contraste entre le choix de Applicative, Flèches et Monades, mais plutôt une description de combien ils sont identiques. Pour la décision en cours, la déclaration est discutable.

Ceci est souvent mal compris. La déclaration continue à décrire join :: m (m a) -> m a en tant que produit tensoriel pour l'endofoncteur monoïdal. Cependant, il n'indique pas comment, dans le contexte de cette déclaration, (<*>) pourrait aussi avoir été choisi. C'est vraiment un exemple de six / six douzaines. 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 en combinant 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 m valeurs 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 de 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.-à-d. a -> b -> b contre b -> a -> b pour chacun respectivement), je suppose que nous aurions pu paramétrer la logique monoïdale, le produit tensoriel, pour la réutiliser dans les deux définitions. Comme un exercice pour faire le point, essayez et implémentez ~tet vous vous retrouvez avec (<*>) et (>>=) en fonction de 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 à la mise en œuvre de ces classes de types.

En conclusion, dans ma propre expérience, la citation infâme de Mac Lane a fourni un grand mème "goto", un guide pour moi de référence tout en naviguant à travers la catégorie pour mieux comprendre les idiomes utilisés dans Haskell. Il réussit à capturer la portée d'une puissante capacité de calcul rendue merveilleusement accessible à 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'il décrit s'avère être ce qui est similaire entre Applicative et Monades (et Arrows entre autres). Ce qu'il ne dit pas, c'est précisément la distinction petite mais utile entre eux.

- E


2