Monades comme adjonctions

Question

J'ai lu des articles sur les monades dans la théorie des catégories. Une définition des monades utilise une paire de foncteurs adjoints. Une monade est définie par un aller-retour 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 de Haskell en termes de foncteurs adjoints. Quelqu'un a-t-il pensé à cela?

Answer 1

Edit: Juste pour le fun, je vais faire de ce droit. Réponse originale à cette question conservé ci-dessous

Le courant de contiguïté code de catégorie-les extras est maintenant dans le adjunctions paquet: http://hackage.haskell.org/package/adjunctions

Je vais juste travailler par le biais de l'état monade explicitement et simplement. Ce code utilise Data.Functor.Compose des transformateurs du package, mais sinon autonome.

Une contiguïté entre f (D -> C) et g (C -> D), écrit-f| g, peut être caractérisé par un certain nombre de façons. Nous allons utiliser le counit/unité (epsilon/eta) description, ce qui donne deux les transformations naturelles (morphisms 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 l'identité foncteur en D.

Nous pouvons également récupérer les hom-jeu de contiguïté définition de la counit/définition de l'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 de notre unité/counit contiguïté comme suit:

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 mettre en œuvre le classique de contiguïté 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 type synonyme

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

Et si nous charger de cette opération dans ghci, nous pouvons confirmer que l'État est précisément notre classique de l'état de monade. Notez que nous pouvons prendre à l'opposé de la composition et obtenir le Costate Comonad (aka le magasin comonad).

Il y a un tas d'autres adjunctions nous pouvons faire dans les monades dans ce mode (comme (Bool) Paire), mais ils sont une sorte d'étrange monades. Malheureusement nous ne pouvons pas faire la adjunctions qui induisent le Lecteur et l'Écrivain directement en Haskell d'une manière agréable. Nous pouvons faire de Suite, mais comme copumpkin décrit, qui nécessite une contiguïté à partir d'une face de la catégorie, de sorte qu'il utilise en fait une autre "forme" de la "Adjoint" typeclass qui renverse quelques flèches. Ce formulaire est également mis en œuvre dans un autre module dans le adjunctions paquet.

ce matériau est recouvert d'une manière différente par Derek Elkins article dans La Monade Lecteur 13 -- Calcul des Monades avec la Catégorie de la Théorie: http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

Aussi, Hinze récentes Extensions de Kan pour l'Optimisation du Programme de papier promenades à travers la construction de la liste monade de la contiguïté entre Mon et Set: http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf

---

Vieille réponse:

Deux références.

1) la Catégorie extras offre, comme toujours, avec une représentation de adjunctions et comment les monades en découlent. Comme d'habitude, il est bon de penser, mais jolie lumière sur la documentation: http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html

2) -Café offre également prometteurs, mais une brève discussion sur le rôle de la contiguïté. Qui peut l'aider dans l'interprétation de catégorie-les extras: http://www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html

Answer 2

Derek Elkins me montrait récemment au dîner comment la Cont Monad découle de la composition du foncteur contravariant (_ -> k) avec lui-même, puisqu'il se trouve qu'il est auto-adjoint. C'est comme ça que vous obtenez (a -> k) -> k . Son conseil, cependant, mène à l'élimination de la double négation, ce qui ne peut pas être écrit en Haskell.

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

Answer 3

C'est un vieux thread, mais je trouve la question intéressante, j'ai donc fait quelques calculs moi-même. Espérons que Bartosz est toujours là et peut lire ceci..

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

Laissez - T la liste monade < T,eta,mu > (eta = return et mu = concat) et d'envisager un T-algèbre h:T a -> a.

(À noter qu' T a = [a] gratuite est un monoïde <[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, certains facile diagramme de chasser prouve qu' h fait induit une structure de monoïde sur un (défini par l' x*y = h[x,y] ), et qu' h devient un monoïde homomorphism pour cette structure.

A l'inverse, toute structure de monoïde < a,a0,* > défini dans Haskell est naturellement défini comme un T-algèbre.

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

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

(Veuillez vérifier que le morphisms T-algèbres sont en fait monoïde homomorphisms.)

Elle caractérise également les listes universel objets dans HaskMon, tout comme des produits gratuits en Grp, polynôme anneaux en CRng, etc.

Le adjuction correspondant à la construction précédente est - < F,G,eta,epsilon >

où

• F:Hask -> HaskMon, ce qui prend un type un pour le " libre-monoïde généré par a',c'est - [a],
• G:HaskMon -> Hask, les oublieux foncteur (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 (le "surjection canonique" à partir d'un monoïde libre à son monoïde quotient)

Ensuite, il y a une autre catégorie de Kleisli' et de la contiguïté. Vous pouvez vérifier que c'est juste la catégorie de Haskell types avec morphisms a -> T b, où ses compositions sont données par la soi-disant "Kleisli composition' (>=>). Un typique Haskell programmeur trouverez cette catégorie de plus en plus familiers.

Enfin,comme il est illustré dans CWM, la catégorie des T-algèbres (resp. Catégorie de Kleisli) devient le terminal (resp. initiale) de l'objet dans la catégorie de adjuctions qui définissent la liste monade T dans un sens.

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

Answer 4

J'ai trouvé un standard constructions de complément foncteurs pour toute monade par Eilenberg-Moore, mais je ne suis pas sûr si elle ajoute aucune idée du problème. La deuxième catégorie dans la construction est une catégorie de T-algèbres. Un T algèbre ajoute un "produit" à la catégorie initiale.

Alors, comment serait-il travailler pour une liste monade? Le foncteur dans la liste monade se compose d'un constructeur de type, par exemple, Int->[Int] et une cartographie des fonctions (par exemple, la norme d'application de la carte à des listes). Une algèbre ajoute une cartographie à partir des listes d'é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, de type Int, et les cartes dans l'algèbre définie sur les listes de type Int, où le produit est défini par monadique de joindre (ou vice-versa, la jointure est défini comme le produit). L'oublieux foncteur G prend une algèbre et oublie le produit. La paire F, G, adjoint de foncteurs est ensuite utilisée pour construire la monade de la manière habituelle.

Je dois dire que je suis pas plus avancé.

Answer 5

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

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

Même l'utilisation de IO monades est non essentiel, pour le courant Haskell type de système est puissant suffisant pour réaliser l'encapsulation de données (existentielle).

C'est ma réponse à votre question de départ, mais je suis curieux de ce que Haskell experts 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 (T)algèbres. Adjoints, dans MacLane, sont " une façon pour exprimer les équivalences de catégories.' Dans un décor typique de adjunctions <F,G>:X->A où F est une sorte de "libre-algèbre génératrice' et G 'oublieux foncteur", le correspondant de la monade sera (grâce à l'utilisation de T-algèbres) décrire comment (et quand) la structure algébrique de l' A est construit sur les objets de l' X.

Dans le cas de Hask et la liste monade T, la structure qui T introduit, c'est que de monoïde,et cela peut nous aider à établir les propriétés (y compris l'exactitude du code algébriques méthodes de la théorie de la monoids fournit. Par exemple, la fonction foldr (*) e::[a]->a peut facilement être vu comme un cadre associatif fonctionnement tant qu' <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 'récursivité des schémas de programmation fonctionnelle en utilisant catégorique méthodes dans l'espoir de (partiellement) élimination du "goto de la programmation fonctionnelle', Y (l'arbitraire de la récursivité combinator).

Apparemment, ce genre d'application est l'une des principales motivations des créateurs de la Théorie de la Catégorie (MacLane, Eilenberg, etc.), à savoir, pour établir naturel équivalence de catégories, et le transfert d'une méthode bien connue dans une catégorie à l'autre (par exemple homologique méthodes d'espaces topologiques,des méthodes algébriques pour la programmation, etc.). Ici, les adjoints et les monades sont des outils indispensables pour exploiter cette connexion de catégories. (D'ailleurs, la notion de monades (et son double, comonads) est si générale que l'on peut même aller jusqu'à définir "cohomologies' de Haskell types.Mais je n'ai pas une pensée encore).

Comme pour les non-determistic fonctions que vous avez mentionné, j'ai beaucoup moins de choses à dire... Mais notez que, si une contiguïté <F,G>:Hask->A pour certaines catégorie A définit la liste monade T, il doit y avoir un unique foncteur de comparaison' K:A->MonHask (catégorie de monoids définissable en Haskell), voir CWM. Cela signifie, en effet, que votre catégorie d'intérêt doit être une catégorie de monoids dans certaines forme restreinte (par exemple, il peut manquer certains quotients, mais pas gratuitement algèbres) afin de définir la liste monade.

Enfin,quelques remarques:

L'arbre binaire foncteur je l'ai mentionné dans mon dernier message généralise facilement à l'arbitraire de type de données T a1 .. an = T1 T11 .. T1m | .... À savoir,tout type de données en Haskell définit naturellement une monade (avec les correspondants de la catégorie des algèbres et la catégorie de Kleisli), qui n'est que le résultat de toutes les données constructeur en Haskell être total. C'est une autre raison pourquoi je considère que Haskell Monade classe n'est pas beaucoup plus qu'une syntaxe de sucre (ce qui est assez important dans la pratique,bien sûr).