From madore@clipper.ens.fr Mon Nov 27 21:42:31 2000 Article: 3711 of ens.forum.sciences.maths Path: eleves!not-for-mail From: madore@clipper.ens.fr (GroTeXdieck) Newsgroups: ens.forum.informatique.lang.caml,ens.forum.sciences.informatique,ens.forum.sciences.maths Subject: Monades (was: Re: Caml c'est de la m***e) Followup-To: ens.forum.sciences.informatique Date: Mon, 27 Nov 2000 20:42:31 +0000 (UTC) Organization: Forum. Lines: 240 Sender: madore@clipper.ens.fr Message-ID: <8vugvn$qtm$1@clipper.ens.fr> References: <7mdvhu$7cv$1@clipper.ens.fr> <8vrgck$ki4$1@clipper.ens.fr> <8vtlst$av0$1@clipper.ens.fr> <8vtmni$j2t$1@clipper.ens.fr> <8vtns8$kmn$1@clipper.ens.fr> NNTP-Posting-Host: clipper.ens.fr X-Trace: clipper.ens.fr 975357751 27574 129.199.129.1 (27 Nov 2000 20:42:31 GMT) X-Complaints-To: forum@clipper.ens.fr NNTP-Posting-Date: Mon, 27 Nov 2000 20:42:31 +0000 (UTC) X-Newsreader: Flrn (0.4.0 - 07/99) X-Start-Date: 27 Nov 2000 17:41:40 GMT X-Mark: BOG Xref: eleves ens.forum.informatique.lang.caml:722 ens.forum.sciences.informatique:327 ens.forum.sciences.maths:3711 Bon, le premier truc c'est que les matheux et les informaticiens ne définissent pas une monade de la même façon. Pour les matheux, une monade dans une catégorie C c'est un triplet (M,µ,h), où M:C->C est un foncteur (covariant), µ:M²->M et h:id->M des transformations naturelles telles que pour tout objet A de C on ait µ_A · h_MA = id_MA µ_A · Mh_A = id_MA µ_A · Mµ_A = µ_A · µ_MA (ici, · désigne la composition pour plus de clarté ; évidemment, Mh_A : MA->M²A c'est l'image du morphisme h_A : A->MA par le foncteur M ; je vous laisse tracer les diagrammes commutatifs correspondats). L'exemple fondamental, c'est que si F-|U sont des foncteurs adjoints, alors M=U·F muni de h l'unité de l'adonction et µ composée de la coünité par le foncteur F, est une monade. En fait, toutes les monades sont de cette forme (voir plus bas). Ainsi, si U est le foncteur d'oubli des groupes vers les ensembles, et F son adjoint à gauche le foncteur groupe libre, alors M est le foncteur « ensemble des éléments du groupe libre basé sur cet ensemble », h est le morphisme évident d'inclusion d'un ensemble dans l('ensemble sous-jacent au) groupe libre dont il est une base et µ est le morphisme de « déparenthésage » qui transforme un élément du groupe libre sur le groupe libre sur une certaine base en l'élément du groupe libre obtenu en remplaçant les générateurs par les éléments correspondants du groupe libre. Très concrètement, les éléments du groupe libre (sur une base a,b,c...) sont des expressions du genre « ab », « cab²c^-1 »..., les éléments du groupe libre sur *ça* sont des expressions du genre « "ab" "cab²c^-1" "1"² "a"^-1 » : je mets des guillemets autour des expressions du groupe libre qui servent comme générateurs du groupe libre sur le groupe libre ; et µ fait quelque chose de très simple : enlever les guillemets (les remplacer par des parenthèses). C'est un exemple très général qu'il faut avoir en tête. Donnons deux autres exemples d'utilité importante en informatique. Premièrement, soit C une catégorie admettant des coproduits finis et un objet terminal {*}. Alors le foncteur M qui envoie un objet A sur le coproduit de A et {*} constitue une monade lorsqu'on le muni des transformations h et µ définies ainsi : h est simplement le plongement canonique de A dans le coproduit, et µ s'obtient en mappant les deux objets terminaux ajoutés à A dans M²A sur un seul dans MA. Il faut comprendre MA comme le type « maybe A » (ou « A option ») : # let eta = fun x -> Some x ;; val eta : 'a -> 'a option = # let mu = function None -> None | Some (None) -> None | Some (Some (x)) -> Some (x) ;; val mu : 'a option option -> 'a option = c'est-à-dire que le foncteur M est le type (paramétrique) « option » et que eta et mu sont les h et µ de la monade. Deuxièmement, soit C une catégorie admettant des produits finis et des exponentielles internes. Soit S un objet fixé (les « états ») de C. On considère le foncteur M qui envoie A sur S=>A×S (ici, => désigne l'exponentielle interne et le parenthésage est à comprendre comme « S => (A×S) ») ; l'action de M sur les morphismes est assez claire : si A->B est un morphisme, M envoie A->B sur le morphisme (S=>A×S)->(S=>B×S) obtenu par composition pour ce qui est de la première composante, et identiquement pour la seconde. On définit h:A->MA transformation naturelle (de décurryfication) par h:A->S=>A×S image de l'identité A×S->A×S par la transformation naturelle de définition de l'exponentielle interne (symboliquement, h envoie a de A sur la fonction S=>A×S qui envoie s sur (a,s)). On définit encore µ:M²A->MA de façon relativement claire mais pénible à décrire : symboliquement, pour w de M²A = S=>((S=>A×S)×S), µ(w) est le point de MA = S=>A×S défini par µ(w)(s) = v(s') où w(s) = (v,s'). (Bon, si on veut vraiment une définition précise, µ est la composition interne par le morphisme d'évaluation - mais ce n'est vraiment pas parlant.) Il faut comprendre MA comme le type « A avec effet de bord sur S » : # module type STATEKIND = sig type state end ;; module type STATEKIND = sig type state end # module State_monad = functor (St : STATEKIND) -> struct type 'a monad = St.state -> 'a * St.state let eta : 'a -> 'a monad = fun a -> fun s -> (a,s) let mu : 'a monad monad -> 'a monad = fun w -> fun s -> let (v,s2)=w(s) in v(s2) end ;; module State_monad : functor (St : STATEKIND) -> sig type 'a monad = St.state -> 'a * St.state val eta : 'a -> 'a monad val mu : 'a monad monad -> 'a monad end À partir de là, on peut faire de la méta-abstraction sur les monades en Caml si on en a envie. Une monade est la donnée d'un foncteur (« foncteur » dans le sens mathématique, pas Caml-ien) « monad », c'est-à-dire à la fois un type paramétrique et une action sur les morphismes, plus les morphismes eta et mu de structure : # module type MONAD = sig type 'a monad val eta : 'a -> 'a monad val mu : 'a monad monad -> 'a monad val monad : ('a -> 'b) -> 'a monad -> 'b monad end ;; module type MONAD = sig type 'a monad val eta : 'a -> 'a monad val mu : 'a monad monad -> 'a monad val monad : ('a -> 'b) -> 'a monad -> 'b monad end # module Maybe_monad : MONAD = struct type 'a monad = 'a option let eta : 'a -> 'a monad = fun x -> Some (x) let mu : 'a monad monad -> 'a monad = function None -> None | Some (None) -> None | Some (Some (x)) -> Some (x) let monad : ('a -> 'b) -> 'a monad -> 'b monad = fun f -> function None -> None | Some (x) -> Some (f x) end ;; module Maybe_monad : MONAD # module type STATEKIND = sig type state end ;; module type STATEKIND = sig type state end # module State_monad : functor (St : STATEKIND) -> MONAD = functor (St : STATEKIND) -> struct type 'a monad = St.state -> 'a * St.state let eta : 'a -> 'a monad = fun a -> fun s -> (a,s) let mu : 'a monad monad -> 'a monad = fun w -> fun s -> let (v,s2)=w(s) in v(s2) let monad : ('a -> 'b) -> 'a monad -> 'b monad = fun f -> fun v -> fun s -> let (a,s2)=v(s) in (f a,s2) end ;; module State_monad : functor (St : STATEKIND) -> MONAD # module Trivial_monad : MONAD = struct type 'a monad = 'a let eta : 'a -> 'a monad = fun x -> x let mu : 'a monad monad -> 'a monad = fun x -> x let monad : ('a -> 'b) -> 'a monad -> 'b monad = fun f -> fun x -> f x end ;; module Trivial_monad : MONAD (Oui, je sais, je ne sais pas écrire en Caml. De toute façon je n'ai jamais rien compris à Caml. Et surtout pas comment on est censé indenter ce langage au parsage tellement délirant.) Bon, revenons à des choses plus sérieuses. Lorsque (M,µ,h) est une monade (dans une catégorie C), une *algèbre* sur M est la donnée d'un objet A de C et d'un morphisme @:MA->A tels que @ · h_A = id_A @ · M@ = @ · µ_A Si @:MA->A et #:MB->B sont deux (M,µ,h)-algèbres, un morphisme f entre elles est la donnée d'un morphisme f:A->B tel que f·@ = #·Mf. De cette façon, les algèbres sur une monade donnée forment une catégorie, appelée *catégorie d'Eilenberg-Moore* de la monade. On a un foncteur U de la catégorie d'Eilenberg-Moore vers la catégorie C, qui à une (M,µ,h)-algèbre @:MA->A fait correspondre l'objet A. Et ce foncteur U admet un adjoint à gauche F, qui envoie un objet A de C sur la (M,µ,h)-algèbre µ_A:M²A->MA, qu'on appelle aussi la (M,µ,h)-algèbre libre sur l'objet A. Par miracle, on a M=U·F, de sorte que, comme je l'avais annoncé, toute monade provient d'une adjonction de foncteurs. (Attention, cependant, celle-ci n'est pas unique ! Si on part d'une adjonction de foncteurs, qu'on construit la catégorie d'Eilenberg-Moore sur la monade correspondante, on ne retrouve pas forcément les foncteurs de départ. La catégorie d'Eilenberg-Moore et les foncteurs correspondants sont même la catégorie *terminale* avec la bonne structure d'adjonction de la monade. On connaît aussi la catégorie *initiale*, c'est la catégorie de Kleisli : voir n'importe quel texte sur la théorie des catégories pour en savoir plus.) Si M est le foncteur, déjà regardé plus haut, qui à un ensemble associe l'ensemble des éléments du groupe libre ayant pour base cet ensemble, M étant muni d'une structure de monade comme décrit, alors une M-algèbre est tout simplement un groupe (enfin, soyons prudent : la catégorie des M-algèbres est équivalente à celle des groupes). Si M est la monade « maybe » qui à un objet A fait correspondre son coproduit avec l'objet terminal, alors une M-algèbre est la donnée d'un « C-objet pointé », c'est-à-dire un objet A de C avec un point global (un morphisme depuis l'objet terminal). Pour le troisième exemple que j'ai donné, je ne sais pas trop ce que ça fait, parce qu'à ce moment-là, ma tête a explosé. (De toute façon, personne ne va lire mon message jusque là, c'est évident.) Maintenant, pour un informaticien, et Alain en est un exemple ;-), une monade est déterminée par la transformation h:A->MA (naturelle en A) et par ð:(A->MB)->MA->MB, pardon, (A=>MB)->(MA=>MB) (naturelle en A et B), de façon à éviter le M². Le ð est déterminé symboliquement comme suit : si f:A->MB alors Mf:MA->M²B, donc µ_B·Mf : MA->MB, d'où l'image par ð. Réciproquement, la donnée de ð permet de retrouver µ : prendre A=MB, et la fonction MB->MB identité, dont l'image par ð est précisément µ_B:M²B->MB. Et la donnée de ð permet aussi de retrouver l'action de M sur les morphismes : si g:A->B, alors h_A·g : A->MB et son image par ð est µ_B·Mh_B·Mg, soit Mg tout court par les axiomes de monadologie. En Caml : # module type MONAD = sig type 'a monad val eta : 'a -> 'a monad val mu : 'a monad monad -> 'a monad val monad : ('a -> 'b) -> 'a monad -> 'b monad end ;; module type MONAD = sig type 'a monad val eta : 'a -> 'a monad val mu : 'a monad monad -> 'a monad val monad : ('a -> 'b) -> 'a monad -> 'b monad end # module type ALTMONAD = sig type 'a monad val eta : 'a -> 'a monad val eth : ('a -> 'b monad) -> 'a monad -> 'b monad end ;; module type ALTMONAD = sig type 'a monad val eta : 'a -> 'a monad val eth : ('a -> 'b monad) -> 'a monad -> 'b monad end # module MonadOfAltMonad : functor (M : ALTMONAD) -> MONAD = functor (M : ALTMONAD) -> struct type 'a monad = 'a M.monad let eta = M.eta let mu : 'a monad monad -> 'a monad = fun x -> M.eth (fun v -> v) x let monad : ('a -> 'b) -> 'a monad -> 'b monad = fun g -> M.eth (fun x -> eta (g x)) end ;; module MonadOfAltMonad : functor (M : ALTMONAD) -> MONAD # module AltMonadOfMonad : functor (M : MONAD) -> ALTMONAD = functor (M : MONAD) -> struct type 'a monad = 'a M.monad let eta = M.eta let eth : ('a -> 'b monad) -> 'a monad -> 'b monad = fun f -> fun a -> M.mu (M.monad f a) end ;; module AltMonadOfMonad : functor (M : MONAD) -> ALTMONAD (C'est dans ce genre de cas que je trouve particulièrement frustrant que le langage Caml - comme les autres du reste - n'inclue pas un vérificateur de preuves. Parce qu'une monade ça a des relations et pas juste des données, et mes deux foncteurs, ils sont quasi-inverses. Je voudrais pouvoir le prouver au langage.) Bon, j'arrête là, parce qu'en fait ça commence à me lourder très sérieusement, les monades, à ce stade. Ceci dit, il faudra que j'examine de quelle façon, en logique linéaire, !A est une monade.