Les monades comme adjunctions

J'ai lu sur les monades dans la théorie des catégories. Une définition de monades utilise une paire de foncteurs adjoints. Une monade est définie par un aller-retour en utilisant ces foncteurs. Apparemment, les adjonctions sont très importantes dans la théorie des catégories, mais je n'ai vu aucune explication des monades Haskell en termes de foncteurs adjoints. Quelqu'un a donné une pensée?

70
demandé sur Bartosz Milewski 2011-01-15 03:31:01

5 réponses

Edit : juste pour le plaisir, je vais le faire correctement. Réponse originale conservée ci-dessous

Le code d'adjonction actuel pour category-extras se trouve maintenant dans le package adjunctions: http://hackage.haskell.org/package/adjunctions

Je vais juste travailler à travers la monade d'état explicitement et simplement. Ce code utilise Data.Functor.Compose du package transformers, mais est par ailleurs autonome.

Une adjonction entre f (D - > C) et g (C - > D), écrite f | / g, peut être caractérisé par un certain nombre de façons. Nous utiliserons la description counit / unit (epsilon/eta), qui donne deux transformations naturelles (morphismes entre foncteurs). 

class (Functor f, Functor g) => Adjoint f g where
     counit :: f (g a) -> a
     unit   :: a -> g (f a)

Notez que le "a" dans counit est vraiment l'identité foncteur de C, et la "une" de l'unité est vraiment le foncteur identité dans D.

Nous pouvons également récupérer la définition d'adjonction hom-set à partir de la définition counit/unit.

phiLeft :: Adjoint f g => (f a -> b) -> (a -> g b)
phiLeft f = fmap f . unit

phiRight :: Adjoint f g => (a -> g b) -> (f a -> b)
phiRight f = counit . fmap f

Dans tous les cas, nous pouvons maintenant définir une monade à partir de notre unité / counit comme ça: 

instance Adjoint f g => Monad (Compose g f) where
    return x = Compose $ unit x
    x >>= f  = Compose . fmap counit . getCompose $ fmap (getCompose . f) x

Maintenant, nous pouvons implémenter l'adjonction classique entre (A,) et (a ->): 

instance Adjoint ((,) a) ((->) a) where
    -- counit :: (a,a -> b) -> b
    counit (x, f) = f x
    -- unit :: b -> (a -> (a,b))
    unit x = \y -> (y, x)

Et maintenant un synonyme de type 

type State s = Compose ((->) s) ((,) s)

Et si nous chargeons cela dans ghci, nous pouvons confirmer que L'État est précisément notre monade d'état classique. Notez que nous pouvons prendre la composition opposée et obtenir le Costate Comonad (aka le magasin comonad).

Il y a un tas d'autres adjonctions que nous pouvons transformer en monades de cette manière (comme (Bool,) Pair), mais elles sont un peu étranges les monades. Malheureusement, nous ne pouvons pas faire les adjonctions qui induisent le lecteur et L'écrivain directement dans Haskell d'une manière agréable. Nous pouvons faire Cont, mais comme le décrit copumpkin, cela nécessite une adjonction d'une catégorie opposée, donc il utilise en fait une "forme" différente de la classe de type "Adjoint" qui inverse certaines flèches. Cette forme est également implémentée dans un module différent dans le package adjunctions.

Ce matériel est couvert d'une manière différente par L'article de Derek Elkins dans la Monade Lecteur 13 -- calcul des monades avec la théorie des catégories: http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

En outre, les récentes Extensions kan de Hinze pour le papier D'optimisation de programme parcourent la construction de la monade de liste à partir de l'adjonction entre Mon et Set: http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf

Ancienne réponse:

Deux références.

1) Category-extras offre, comme toujours, une représentation des adjonctions et comment les monades en découlent. Comme d'habitude, il est bon de penser avec, mais assez léger sur la documentation: http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html

2) - Cafe Livre également avec une discussion prometteuse mais brève sur le rôle de l'adjonction. Certains d'entre eux peuvent aider à interpréter category-extras: http://www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html

36
répondu sclv 2014-03-26 05:33:19

Derek Elkins me montrait récemment au cours du dîner comment la Monade Cont découle de la composition du foncteur (_ -> k) contravariant avec lui-même, car il se trouve être auto-adjoint. Voilà comment vous obtenez (a -> k) -> k hors de lui. Son counit, cependant, conduit à une double élimination de la négation, qui ne peut pas être écrite en Haskell.

Pour un code Agda qui illustre et prouve cela, veuillez consulter http://hpaste.org/68257 .

10
répondu copumpkin 2012-05-09 17:41:28

C'est un vieux fil, mais j'ai trouvé la question intéressante, j'ai donc fait quelques calculs moi-même. Espérons que Bartosz est toujours là et peut lire ce qui suit..

En fait, la construction Eilenberg-Moore donne une image très claire dans ce cas. (Je vais utiliser la notation CWM avec la syntaxe de type Haskell)

Soit {[0] } la monade de liste< T,eta,mu > (eta = return et mu = concat) et considérons une algèbre T h:T a -> a.

(Notez que T a = [a] est un monoïde libre <[a],[],(++)>, qui est, de l'identité [] et la multiplication (++).)

, Par définition, h doit satisfaire h.T h == h.mu a et h.eta a== id.

Maintenant, une simple poursuite de diagramme prouve que h induit en fait une structure monoïde sur a (définie par x*y = h[x,y] ), et que h devient un homomorphisme monoïde pour cette structure.

Inversement, toute structure monoïde < a,a0,* > définie dans Haskell est naturellement définie comme une t-algèbre.

De cette façon (h = foldr ( * ) a0, une fonction qui "remplace" (:) avec (*),et les cartes [] à a0, identité).

Donc, dans ce cas, la catégorie des algèbres T est juste la catégorie des structures monoïdes définissables dans Haskell, HaskMon.

(veuillez vérifier que les morphismes des algèbres T sont en fait des homomorphismes monoïdes.)

Il caractérise également les listes comme des objets universels dans HaskMon, tout comme les produits libres dans Grp, les anneaux polynomiaux dans CRng, etc.

L'adjonction correspondant à la construction ci-dessus est < F,G,eta,epsilon >

Où

  • F:Hask -> HaskMon, qui prend un type a au 'monoïde libre généré par a',c'est-à-dire, [a],
  • G:HaskMon -> Hask, le foncteur oublieux (oublier la multiplication),
  • eta:1 -> GF , la transformation naturelle définie par \x::a -> [x],
  • epsilon: FG -> 1 , la transformation naturelle définie par la fonction de pliage ci-dessus (la "surjection canonique" d'un monoïde libre à son monoïde quotient)

Ensuite, il y a un autre ' Kleisli catégorie' et l'adjonction correspondante. Vous pouvez vérifier que c'est juste la catégorie des types Haskell avec des morphismes a -> T b, où ses compositions sont données par la "composition Kleisli" (>=>). Un programmeur Haskell typique trouvera cette catégorie plus familière.

Enfin, comme L'illustre le MCG, la catégorie des T-algèbres (resp. Catégorie Kleisli) devient le terminal (resp. initial) objet dans la catégorie des adjuctions qui définissent la monade de liste T dans un approprié sens.

Je suggère de faire des calculs similaires pour le foncteur d'arbre binaire T a = L a | B (T a) (T a) pour vérifier votre compréhension.

8
répondu takosuke 2012-02-14 09:19:26

J'ai trouvé une construction standard de foncteurs auxiliaires pour n'importe quelle monade par Eilenberg-Moore, mais je ne suis pas sûr si cela ajoute un aperçu au problème. La deuxième catégorie dans la construction est une catégorie D'algèbres T. Une algèbre T ajoute un "produit" à la catégorie initiale.

Alors, comment cela fonctionnerait-il pour une monade de liste? Le foncteur de la monade list se compose d'un constructeur de type, par exemple Int->[Int] et d'un mappage de fonctions (par exemple, application standard de map aux listes). Une algèbre ajoute un mappage des listes aux éléments. Un exemple serait d'ajouter (ou de se multiplier) tous les éléments d'une liste d'entiers. Le foncteur F prend n'importe quel type, par exemple Int, et le mappe dans l'algèbre définie sur les listes de Int, où le produit est défini par join monadique (ou vice versa, join est défini comme le produit). Le foncteur oublieux G prend une algèbre et oublie le produit. La paire F, G, des foncteurs adjoints est ensuite utilisé pour construire la monade de la manière habituelle.

Je je dois dire que je ne suis pas plus sage.

2
répondu Bartosz Milewski 2012-02-14 09:56:11

Si vous êtes intéressé, voici quelques pensées d'un non-expert sur le rôle des monades et des adjonctions dans les langages de programmation:

Tout d'Abord, il existe pour une monade T unique contiguïté pour la catégorie de Kleisli T. Dans Haskell, l'utilisation des monades se limite principalement aux opérations de cette catégorie (qui est essentiellement une catégorie d'algèbres Libres, pas de quotients). En fait, tout ce que l'on peut faire avec une monade Haskell est de composer des morphismes Kleisli de type a->T b grâce à l'utilisation d'expressions, (>>=), etc. pour en créer un nouveau morphism. Dans ce contexte, le rôle des monades se limite à l'économie de notation.On exploite l'associativité des morphismes pour pouvoir écrire (disons) [0,1,2] au lieu de (Cons 0 (Cons 1 (Cons 2 Nil))), c'est-à-dire, vous pouvez écrire sequence comme sequence, pas comme un arbre.

Même l'utilisation de monades IO n'est pas essentielle, car le système de type Haskell actuel est puissant assez pour réaliser l'encapsulation de données (types existentiels).

C'est mon réponse à votre question initiale, mais je suis curieux de savoir ce que les experts Haskell ont à dire à ce sujet.

D'autre part, comme nous l'avons noté, il y a aussi une correspondance 1-1 entre les monades et adjunctions aux algèbres (T -). Les Adjoints, selon les termes de MacLane, sont "un moyen exprimer des équivalences de catégories.' Dans un cadre typique d'adjunctions <F,G>:X->A Où F est une sorte de 'générateur d'algèbre libre' et G un 'foncteur oublieux', la monade correspondante sera (grâce à l'utilisation de T-algèbres) décrire comment (et quand) la structure algébrique de A est construit sur les objets de X.

Dans le cas de Hask et de la liste Monade T, la structure que T introduit est la suivante de monoïde, et cela peut nous aider à établir des propriétés (y compris l'exactitude) du code à travers algébrique méthodes que la théorie des monoïdes fournit. Par exemple, la fonction foldr (*) e::[a]->a peut être facilement considéré comme une opération associative tant que <a,(*),e> est un monoïde, un fait qui pourrait être exploité par le compilateur d'optimiser le calcul (par exemple, par parallélisme). Une autre application consiste à identifier et classer les "modèles de récursivité" dans la programmation fonctionnelle en utilisant catégorique méthodes dans l'espoir de disposer (partiellement) de 'le goto de la programmation fonctionnelle', Y (le combinateur de récursivité arbitraire).

Apparemment, ce genre d'applications est L'une des principales motivations des créateurs de la théorie des catégories (MacLane, Eilenberg, etc.), à savoir, pour établir l'équivalence naturelle de catégories, et transférer une méthode bien connue dans une catégorie à l'autre (par exemple méthodes homologiques aux espaces topologiques, méthodes algébriques à la programmation, etc.). Ici, les adjoints et les monades sont des outils indispensables pour exploiter cette connexion de catégories. (Incidemment, la notion de monades (et son dual, comonades) est si générale qu'on peut même aller jusqu'à définir des "cohomologies" de Types Haskell.Mais je n'ai pas une pensée encore.)

Quant aux fonctions non-determistic vous mentionné, j'ai beaucoup moins à dire... Mais notez que; si une adjonction <F,G>:Hask->A pour une catégorie A définit la monade de liste T, il doit y avoir un 'foncteur de comparaison' unique K:A->MonHask (la catégorie de monoïdes définissable dans Haskell), voir mcg. Cela signifie, en effet, que votre catégorie d'intérêt doit être une catégorie de monoïdes sous une forme restreinte (par exemple, elle peut manquer de quotients mais pas d'algèbres libres) afin de définir la monade de liste.

Enfin,quelques remarques:

Le binaire le foncteur d'arbre que j'ai mentionné dans ma dernière publication se généralise facilement au type de données arbitraire T a1 .. an = T1 T11 .. T1m | .... A savoir, tout type de données dans Haskell définit naturellement une monade (avec la catégorie correspondante des algèbres et la catégorie Kleisli), ce qui est juste le résultat de tout constructeur de données dans Haskell étant total. C'est une autre raison pour laquelle je considère que la classe Monad de Haskell n'est pas beaucoup plus qu'un sucre de syntaxe (ce qui est assez important dans la pratique,bien sûr).

1
répondu tokosuke 2012-02-14 09:56:02