Discussion :

[Alp]

Bonsoir,

Je me documente de plus en plus sur la liaison entre théorie des catégories, en mathématiques, et programmation fonctionnelle, en informatique donc.

J'ai notamment vu que les monades en programmation fonctionnelle sont issues de monades en théorie des catégories, où elles sont représentées par un triplet (T, u, v) où T est un endofoncteur et u,v deux transformations naturelles, le tout respectant les lois des monades.

J'ai également vu le lien entre modules/foncteurs OCaml par exemple, et catégorie/foncteurs.

Y aurait-il d'autres telles correspondances ? Je veux dire par là à quel point ces deux mondes sont-ils liés ? Quels sont les points que j'ignore encore à ce sujet-là ?

à tous ceux qui prendront le temps de lire et de répondre

[gasche]

Dommage que j'y aie pas pensé plus tôt, j'aurais pu te filer mon rapport de TIPE, qui doit être un des rares documents accessibles en français sur le sujet Maintenant, le contenu serait certainement trop basique.

Je ne pense pas qu'il y aie de véritable correspondance entre les foncteurs OCaml et les foncteurs catégoriques. On pourrait le croire en première approche mais en fait ce n'est pas une bonne analogie. Par contre, la notion de foncteurs en Haskell (ou en OCaml des types à un seul paramètre (covariant)) correspond très bien à des foncteurs.

En partant de l'idée "types paramétrés ~ foncteurs", il y a aussi la correspondance entre les transformations naturelles et les fonctions polymorphes.

On peut aussi utiliser les monades au niveau sémantique, comme l'a fait Moggi au départ : au lieu de représenter "dans ton langage" des objets correspondant à ta monade, tu le regardes "du dehors" comme une catégorie de Kleisli. C'est un domaine que je connais très mal, mais il y a des gens qui savent ça dans le coin.


Par contre, il faut aussi savoir que les catégories c'est pas forcément non plus la panacée. Ça colle très bien par endroit (même si fondamentalement autant OCaml et Haskell sont trop impurs pour que ça colle parfaitement), mais les monades n'ont pas non plus fournit la réponse à l'univers. En particulier, au niveau du "comment représenter les effets de bords ?" qui sont quand même un des trucs pour lequel on parle le plus des monades, elles ne sont en fait qu'une solution très partielle, qui a des défauts, et dont on sait maintenant qu'elle ne colle pas exactement au problème : il y a plus dans les effets de bords que juste des monades, tout comme il y a plus dans les monades que les effets de bords. On peut s'attendre à ce qu'émerge une autre solution (à priori pas spécialement basée sur les catégories) nettement plus satisfaisante à ce problème précis (penser par exemple aux types linéaires de Clean).

[Alp]

Dommage que j'y aie pas pensé plus tôt, j'aurais pu te filer mon rapport de TIPE, qui doit être un des rares documents accessibles en français sur le sujet Maintenant, le contenu serait certainement trop basique.

Tu ne l'as plus ?

Je ne pense pas qu'il y aie de véritable correspondance entre les foncteurs OCaml et les foncteurs catégoriques. On pourrait le croire en première approche mais en fait ce n'est pas une bonne analogie. Par contre, la notion de foncteurs en Haskell (ou en OCaml des types à un seul paramètre (covariant)) correspond très bien à des foncteurs.

Ok, je vois ce que tu veux dire. Pourrais-tu illustrer en t'appuyant sur un exemple ?

On peut aussi utiliser les monades au niveau sémantique, comme l'a fait Moggi au départ : au lieu de représenter "dans ton langage" des objets correspondant à ta monade, tu le regardes "du dehors" comme une catégorie de Kleisli. C'est un domaine que je connais très mal, mais il y a des gens qui savent ça dans le coin.

Il faut que j'approfondisse encore un peu les catégories de Kleisli notamment, je réfléchirai à ce passage de ton post à ce moment-là, probablement d'ici 2 ou 3 mois

Par contre, il faut aussi savoir que les catégories c'est pas forcément non plus la panacée. Ça colle très bien par endroit (même si fondamentalement autant OCaml et Haskell sont trop impurs pour que ça colle parfaitement), mais les monades n'ont pas non plus fournit la réponse à l'univers. En particulier, au niveau du "comment représenter les effets de bords ?" qui sont quand même un des trucs pour lequel on parle le plus des monades, elles ne sont en fait qu'une solution très partielle, qui a des défauts, et dont on sait maintenant qu'elle ne colle pas exactement au problème : il y a plus dans les effets de bords que juste des monades, tout comme il y a plus dans les monades que les effets de bords. On peut s'attendre à ce qu'émerge une autre solution (à priori pas spécialement basée sur les catégories) nettement plus satisfaisante à ce problème précis (penser par exemple aux types linéaires de Clean).

Pour être tout à fait sincère, c'est vraiment l'aspect mathématique qui m'intéresse, pas les applications des catégories à la programmation. Seulement, autant à programmer, hé bien je préfère prendre la programmation fonctionnelle et si je peux y trouver des maths ce n'est pas plus mal

Donc je ne cherche pas une théorie mathématique qui permettrait d'abstraire toute la programmation fonctionnelle, mais c'est toujours intéressant d'en apprendre sur ce genre de choses

[DrTopos]

Bonjour à tous (et bonne année 2009).

Ceux d'entre vous qui me connaissent savent que ce sujet me passionne. Je signale pour ceux que cela intéresse que je fais un cours de Master 2 sur ce sujet à Paris Diderot, et que ce cours commence mercredi prochain (14 janvier) à Chevaleret (175, rue du Chevaleret, Paris 13ème).

Ce cours est librement accessible à tous. Il n'est pas nécessaire d'être inscrit. Bien que le niveau soit Master 2, il n'y a pratiquement pas de prérequis.

J'y parlerai de logique (puisque le cours s'intitule ``Introduction à la Logique Catégorique'') mais aussi beaucoup de catégories bien sûr. Il est prévu un chapitre sur les monades. Les références à l'informatique (et à la compilation en particulier) seront très nombreuses.

Vous trouverez un résumé du cours ici. Des documents seront mis en ligne après chaque cours. Les infos sur le Master LMFI sont ici.

Amitiés.

A.P.

[Alp]

J'ai passé la nuit à lire des tas de choses dessus. Je ne compte plus les papiers que j'ai lus et ceux que j'ai mis de côté pour lire plus tard, qui tournent autour des catégories.

Je ne veux pas déranger, mais serait-il possible de déplacer les cours à Marseille ?

Je suivrai de près les cours mis en ligne dans ce cas, merci beaucoup en tout cas

[DrTopos]

Je ne veux pas déranger, mais serait-il possible de déplacer les cours à Marseille ?

Ce n'est pas complètement impossible, et cela a déjà failli se faire. Mon ami Yves Lafont qui est professeur à Luminy m'a proposé de venir faire ce cours à Marseille, mais pour des raisons pratiques diverses, cela n'a pas eu lieu. Il est toujours possible qu'il reprenne cette idée.

[Alp]

Ce n'est pas complètement impossible, et cela a déjà failli se faire. Mon ami Yves Lafont qui est professeur à Luminy m'a proposé de venir faire ce cours à Marseille, mais pour des raisons pratiques diverses, cela n'a pas eu lieu. Il est toujours possible qu'il reprenne cette idée.

Hélas, je risque de ne pas aller à Luminy pour la continuation de mes études, ce qui fait que je risque en fait d'être tout à fait de l'autre côté de Marseille, à Château-Gombert... A moins que ce soit vraiment mieux à Luminy niveau qualité de cours / activité de recherche / thèmes de recherche / ...

Je vais surveiller, sait-on jamais.

[Garulfo]

Hélas, je risque de ne pas aller à Luminy pour la continuation de mes études, ce qui fait que je risque en fait d'être tout à fait de l'autre côté de Marseille, à Château-Gombert... A moins que ce soit vraiment mieux à Luminy niveau qualité de cours / activité de recherche / thèmes de recherche / ...[...]

Tu abuses pas un peu là Tu veux pas que le cours se passe chez toi non plus ?

[Alp]

Tu abuses pas un peu là Tu veux pas que le cours se passe chez toi non plus ?

Le fait que je ne vais p-ê pas aller à Luminy ne veut pas dire que je veux que le cours me suive

T'es logicien ou psychanalyste toi ?

[SpiceGuid]

Bonjour Alain, et bonnée à vous

Pour être tout à fait sincère, c'est vraiment l'aspect mathématique qui m'intéresse, pas les applications des catégories à la programmation. Seulement, autant à programmer, hé bien je préfère prendre la programmation fonctionnelle et si je peux y trouver des maths ce n'est pas plus mal

La programmation fonctionnelle c'est le prérequis indispensable pour voir où est le caractère computationnel dans la notion de morphisme.
Passé ce stade, les langages fonctionnels et les langages de preuves qui leur sont attachés traînent quand même une très forte coloration algorithmique qui ne les rend pas forcément aptes et/ou agréables au mathématicien.
Par exemple la principale motivation pour les modules c'est de créer des abstractions (espaces de nommage, types abstraits) destinées au programmeur et on ne peut guère y voir plus que de la réutilisation à la manière design patterns.
Si tu considères les 'extensions' de OCaml (modules,POO,variants polymorphes,labels) tu es bien obligé d'admettre qu'elles sont motivées par des considérations pragmatiques (modularité,extensibilité,interface avec le monde 'extérieur').

Tu as déjà évoqué FoCal, et des dérivés/apparentés à Coq il y en a d'autres, à mon avis il faut s'attendre à voir se développer des familles d'assistants de preuve comme il y a des familles de langages de programmation.
La frontière informatique/mathématiques va persister, et même à l'intérieur des deux camps il y aura des usages si diversifiés qu'un seul outil ne pourra pas tous pleinement les satisfaire, quelque soit la bonne volonté de son architecte. D'ailleurs le risque à viser l'universalité c'est au final de n'être optimal pour aucune niche particulière. La bonne stratégie pour tout langage c'est d'établir une petite communauté (à l'aide d'un avantage compétitif sur une certaine niche) pour ensuite faire valoir ses atouts en dehors du cercle initial.

Je ne compte plus les papiers que j'ai lus et ceux que j'ai mis de côté pour lire plus tard, qui tournent autour des catégories.

J'en ai moi aussi survolé quelques-uns, évidemment ceux de la page d'Alain Prouté, au début il est difficile de faire plus que de retenir les mots tout en oubliant les définitions. Je crois bien que j'ai presque fini par comprendre les foncteurs. Mes bases en maths sont assez fragiles et aller plus loin demande un investissement considérable que je ne suis pas prêt à consentir pour l'instant.

[gasche]

Nostalgie, j'ai été tenté par la question d'Alp et j'ai mis les documents relatifs à ce que j'avais écrit pour mon TIPE en ligne. Dans l'ordre chronologique d'écriture :
- un petit pavé en cours d'exploration : http://bluestorm.info/textes/article...des/draft2.pdf
- les slides d'une présentation : http://bluestorm.info/textes/article...des/slides.pdf
- le rapport final : http://bluestorm.info/textes/articles-monades/rendu.pdf

Le petit pavé est le plus verbeux, et il explique de manière je pense assez accessible les concepts de catégorie, foncteur et transformation naturelle ainsi qu'une de leur transposition dans un langage fonctionnel. La présentation des monades qui suit est assez détaillée mais les exemples d'applications informatiques ne sont pas très convaincants. C'est mieux dans les autres documents, qui par contre souffrent de contraintes de taille.
Ce sont des documents sans prétentions, à prendre avec des pincettes (je ne suis évidemment pas un connaisseur du sujet), mais si ça peut intéresser quelqu'un, j'accueille avec intérêt les remarques/critiques.

Peut-être que si j'ai le temps un jour, j'essaierai de reprendre tout ça pour en faire un seul document plus cohérent.

[Alp]

La programmation fonctionnelle c'est le prérequis indispensable pour voir où est le caractère computationnel dans la notion de morphisme.

C'est bien l'impression que je commence à avoir.

Passé ce stade, les langages fonctionnels et les langages de preuves qui leur sont attachés traînent quand même une très forte coloration algorithmique qui ne les rend pas forcément aptes et/ou agréables au mathématicien.

C'est toujours mieux que d'essayer de trouver des analogies à la CT en Java...

Par exemple la principale motivation pour les modules c'est de créer des abstractions (espaces de nommage, types abstraits) destinées au programmeur et on ne peut guère y voir plus que de la réutilisation à la manière design patterns.
Si tu considères les 'extensions' de OCaml (modules,POO,variants polymorphes,labels) tu es bien obligé d'admettre qu'elles sont motivées par des considérations pragmatiques (modularité,extensibilité,interface avec le monde 'extérieur').

Je sais bien, ne t'inquiètes pas. J'ai retrouvé pas mal d'analogies avec des choses que j'avais l'habitude de faire en C++, par rapport à la modularité comme la généricité, sauf que je les ai trouvées plus développées en OCaml biensûr.

Tu as déjà évoqué FoCal, et des dérivés/apparentés à Coq il y en a d'autres, à mon avis il faut s'attendre à voir se développer des familles d'assistants de preuve comme il y a des familles de langages de programmation.
La frontière informatique/mathématiques va persister, et même à l'intérieur des deux camps il y aura des usages si diversifiés qu'un seul outil ne pourra pas tous pleinement les satisfaire, quelque soit la bonne volonté de son architecte. D'ailleurs le risque à viser l'universalité c'est au final de n'être optimal pour aucune niche particulière. La bonne stratégie pour tout langage c'est d'établir une petite communauté (à l'aide d'un avantage compétitif sur une certaine niche) pour ensuite faire valoir ses atouts en dehors du cercle initial.

Je trouve ton point de vue assez pertinent. Il faut juste laisser le temps que les techniques se répandent... A mon avis, un élément essentiel est d'inférer la plus grosse portion possible de preuve tout seul, ou de le suggérer à l'utilisateur. C'est là qu'un langage de preuve pourra se différentier des autres, notamment, à mon avis.

J'en ai moi aussi survolé quelques-uns, évidemment ceux de la page d'Alain Prouté, au début il est difficile de faire plus que de retenir les mots tout en oubliant les définitions. Je crois bien que j'ai presque fini par comprendre les foncteurs. Mes bases en maths sont assez fragiles et aller plus loin demande un investissement considérable que je ne suis pas prêt à consentir pour l'instant.

Effectivement, mais je vais m'investir quand cela vaut le détour à mes yeux...

[SpiceGuid]

@bluestorm
c'est assez complet comme synthèse théorique et pratique, en plus avec du code OCaml c'est assez rare.
Quelques petites questions:

1. Comment les zéros monadiques sont-ils introduis en théorie ? Ce sont juste des points fixes du bind ou y a-t-il plus que cela ?
2. Quand tu parles de foncteurs tu parles de foncteurs covariants. Pourquoi les foncteurs contravariants sont-ils si peu courants en programmation fonctionnelle tandis qu'ils ont l'air plus fréquents en théorie des catégories ?

En effet, on peut introduire dans les langages fonctionnels de nombreux concepts comme les comonades [Kieburtz99] ou les arrows

En terme de conteneurs, les comonades vont forcément être liées à des TADs paresseux, non ? Pour les calculs aussi ? Idem pour les arrows ? Arrows = monades + comonades ?

@Alp
Les notions théoriques peuvent être inhibées ou au contraire révélées par les choix initiaux dans la conception d'un langage, par exemple en Anubis il n'y a pas de mécanisme d'exception, du coup les monades Maybe et Result prennent toute leur importance.
Malheureusement en pratique je ne suis pas convaincu que ça fasse une énorme différence de qualité pour le programmeur. Un programmeur SmallTalk peut considèrer ifTrue: comme une construction syntaxique, le fait que ce soit en réalité une méthode de la classe Boolean ne sert guère qu'à introduire le danger qu'elle soit redéfinie.
Par contre le minimalisme que ça suppose est une très bonne idée, car chaque construction supplémentaire ajoutée réduit d'autant la généralité des constructions déjà présentes.

[gasche]

Quand tu parles de foncteurs tu parles de foncteurs covariants. Pourquoi les foncteurs contravariants sont-ils si peu courants en programmation fonctionnelle tandis qu'ils ont l'air plus fréquents en théorie des catégories ?

En réalité, les foncteurs contravariants sont aussi fréquents en programmation fonctionnelle, mais on a tendance à ne pas trop les mentionner parce qu'ils sont parfois un peu (pardonne le presque-jeu-de-mot, il se fait tard) contrariants.

Par exemple regarde, si "t" est un type fixé, le type :
type 'a to_t = 'a -> t

Ce type est contravariant. En particulier tu ne peux pas écrire map : ('a -> 'b) -> ('a to_t -> 'b to_t), mais map : ('b -> 'a) -> ('a to_t -> 'b to_t).

La variance a de nombreuses incidences, à la fois pratiques (par exemple, les langages ML souffrent d'une limitation du polymorphisme nommée "value restriction", mais on peut s'en débarrasser pour les types qui ne sont pas utilisés en position contravariante) et théoriques (on s'intéresse à la variance dès qu'on fait du sous-typage, donc en particulier quand on fait de la POO typée comme dans OCaml).

Pour ta première question, je ne sais pas. Je n'ai jamais rien rencontré de frappant sur les MonadPlus, mais ça ne veut pas dire que ça n'existe pas. Je doute un peu que cela se révèle d'une importance cruciale, mais il ne faut pas vendre la peau de l'ours.

Arrows = monades + comonades ?

Je t'invite à jeter un oeil à nouveau sur notre discussion d'il y a quelques temps : http://www.developpez.net/forums/d63...-premonoidale/ (je ne sais plus de quelle discussion provenait le message que tu quotes).
Une monade, tu as du "bling" à droite de la flèche. Une comonade c'est à gauche, et une Arrow (qui ne correspond pas aux simples flèches de la catégorie, attention) des deux côtés.

[Alp]

@Alp
Les notions théoriques peuvent être inhibées ou au contraire révélées par les choix initiaux dans la conception d'un langage, par exemple en Anubis il n'y a pas de mécanisme d'exception, du coup les monades Maybe et Result prennent toute leur importance.
Malheureusement en pratique je ne suis pas convaincu que ça fasse une énorme différence de qualité pour le programmeur. Un programmeur SmallTalk peut considèrer ifTrue: comme une construction syntaxique, le fait que ce soit en réalité une méthode de la classe Boolean ne sert guère qu'à introduire le danger qu'elle soit redéfinie.
Par contre le minimalisme que ça suppose est une très bonne idée, car chaque construction supplémentaire ajoutée réduit d'autant la généralité des constructions déjà présentes.

Effectivement. Mais dans beaucoup (trop) de langages tout est inhibé, et ceux qui préfèrent les aspects théoriques plutôt que ceux purement concrets n'ont rien à se mettre sous la dent...
J'aime bien la documentation d'Anubis, où l'on retrouve beaucoup d'endroits où Alain Prouté met l'équivalent mathématique de telle ou telle chose.

Nostalgie, j'ai été tenté par la question d'Alp et j'ai mis les documents relatifs à ce que j'avais écrit pour mon TIPE en ligne. Dans l'ordre chronologique d'écriture :
- un petit pavé en cours d'exploration : http://bluestorm.info/textes/article...des/draft2.pdf
- les slides d'une présentation : http://bluestorm.info/textes/article...des/slides.pdf
- le rapport final : http://bluestorm.info/textes/articles-monades/rendu.pdf

Le petit pavé est le plus verbeux, et il explique de manière je pense assez accessible les concepts de catégorie, foncteur et transformation naturelle ainsi qu'une de leur transposition dans un langage fonctionnel. La présentation des monades qui suit est assez détaillée mais les exemples d'applications informatiques ne sont pas très convaincants. C'est mieux dans les autres documents, qui par contre souffrent de contraintes de taille.
Ce sont des documents sans prétentions, à prendre avec des pincettes (je ne suis évidemment pas un connaisseur du sujet), mais si ça peut intéresser quelqu'un, j'accueille avec intérêt les remarques/critiques.

Peut-être que si j'ai le temps un jour, j'essaierai de reprendre tout ça pour en faire un seul document plus cohérent.

Merci bluestorm !
J'essayerai de te faire un retour vis à vis de ce que je sais déjà et quand au caractère pédagogique tout. Ca pourrait être intéressant de le mettre en ligne dans un coin de dvp pour le petit cercle restreint que nous sommes

[SpiceGuid]

Par exemple regarde, si "t" est un type fixé, le type :
type 'a to_t = 'a -> t

Ce type est contravariant. En particulier tu ne peux pas écrire map : ('a -> 'b) -> ('a to_t -> 'b to_t), mais map : ('b -> 'a) -> ('a to_t -> 'b to_t).

Avoue quand même que cet exemple n'est pas follement passionnant parce que ça n'est rien de plus que de la composition de fonction (même si techniquement c'est bien un foncteur) :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
# type 'a to_unit = Fun of ('a -> unit)

# let compose (Fun g) f =
  Fun (fun x -> g(f x))
val compose : ('a -> 'b) -> 'b to_unit -> 'a to_unit = <fun>

[gorgonite]

Merci bluestorm !
J'essayerai de te faire un retour vis à vis de ce que je sais déjà et quand au caractère pédagogique tout. Ca pourrait être intéressant de le mettre en ligne dans un coin de dvp pour le petit cercle restreint que nous sommes

+1, surtout en version online, pour qu'on puisse le lire depuis n'importe où

[gasche]

Avoue quand même que cet exemple n'est pas follement passionnant parce que ça n'est rien de plus que de la composition de fonction (même si techniquement c'est bien un foncteur)

Je trouve cet exemple attirant précisément parce qu'il est simple. Et il est tout à fait fondamental. Si tu un cadre d'utilisation "technique" de cette contravariance, tu en trouveras par exemple dans le papier "Total functional programming" de Turner.
L'idée est qu'il veut décrire un langage fonctionnel total (dont l'évaluation des termes ne diverge jamais) simple. Il impose donc quelques règles comme le fait que les pattern-matching doivent tous être structurellement exhaustifs (pas de Match Failure), évidemment l'absence de récursion générale, et un critère (règle 2) plus surprenant : pas de types récursifs en position contravariante.

Quand tu as un type récursif comme "type 'a tree = N | T of 'a tree * 'a * 'a tree", les emplacements de récursion sont en position covariante. Si ton langage te permet de définir le type récursif "type boum = Boum of (boum -> unit)" (récursion donc en position contravariante, à gauche de la flèche), tu as un gros problème :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
# type boum = Boum of (boum -> unit);;
type boum = Boum of (boum -> unit)
# let crac (Boum f) = f (Boum f);;
val crac : boum -> unit = <fun>
# let boum = crac (Boum crac);;

Interrupted.

L'évaluation de boum boucle à l'infini. C'est directement lié à la récursion contravariante. En utilisant les mêmes méthodes on peut d'ailleurs coder un combinateur de point fixe en préservant le typage : autrement dit, dans tu prends caml sans "rec", sans effet de bords, sans exceptions, sans filtrages partiels, mais qui autorise la récursion des types en position contravariante, et tu peux définir toutes les fonctions récursives que tu veux.

C'est assez "follement passionnant" ?

[SpiceGuid]

Ce foncteur contravariant est sans doute fondamental puisque la composition est l'opération de base en catégories, d'ailleurs c'est le premier exemple que donne Alain Prouté (Les Topos Elémentaires via les Classifiants), juste après la définition d'un foncteur.

Après c'est certain qu'en pratique mes fonctions sont plus imbriquées que composées, et des foncteurs contravariants j'en vois pas des foules.

[gasche]

Cela vient sans doute du fait qu'en pratique, nous les informaticiens, nous travaillons plus souvent sur le résultat d'une transformation que sur son entrée. Tu vas souvent manipuler des résultats d'une fonction, ainsi que des structures de données (des conténères covariants), que faire des opérations sur l'entrée d'une fonction.

Quand tu sécurises le paramètre d'une fonction, tu as plus tendance à voir ça comme "j'ai transformé une entrée insécurisée en entrée sécurisée" que "j'ai transformé un lecteur d'entrée sécurisée en un lecteur d'entrée insécurisée". Mais dans le fond ce n'est qu'une question de point de vue, et si on s'y habituait on pourrait certainement faire surgir de la contravariance plus souvent.