[Débat] Que pensez-vous du Langage Anubis ?

[DrTopos]

Bonjour.

Merci Flodelarab pour ton post, qui me montre qu'il y a quand même des gens qui s'intéressent à Anubis. Ton message est à la fois enthousiate et critique, ce qui le rend particulièrement crédible. J'espère qu'il incitera d'autres personnes à faire un tour du coté d'Anubis. Je vais maintenant répondre à tes questions.

Le forum dont il est question doit être celui du langage Anubis. Tu ne peux pas ne pas avoir remarqué l'onglet 'Les forums' en haut de chaque page de mon site. Il n'est pas aussi perfectionné que PHPBB mais il fonctionne. Certains membres s'en sont d'ailleurs servi.

Tes remarques sur la manipulation des fichiers sont très justes. Cela fait partie des défauts patents d'Anubis. Sans vouloir chercher d'excuses, c'est clairement la conséquence du fait que mes recherches abstraites portaient sur les aspects abstraits du langage (tout ce que j'appelle 'déterministe'), mais quand j'ai abordé la réalisation, je n'avais encore que des idées très floues sur ce qui n'est pas déterministe (fichiers, connections réseau, objets en général...). Bien entendu, pour la prochaine version (Anubis 1 a été réalisé en 2000), je tiendrai compte de toutes les expériences acquises. Je retiens l'idée de la base de connaissance. D'ailleurs le forum actuel sur mon site peut servir pour cela.

Quant-à ta remarque sur la rapidité à laquelle je peux moi-même développer en Anubis, je te fais quand même remarquer que la librairie contient déjà bon nombre de programmes, et que je n'ai pas chômé. J'ai consacré à Anubis enormément de temps. J'ai aussi un métier et des occupations privées. De toute façon, si tu as pratiqué un peu Anubis, tu as du te rendre compte par toi même que le compilateur détecte des fautes potentielles que des compilateurs C ou Java ne pourraient pas détecter. Il faut se rendre compte qu'Anubis est le travail d'une seule personne (mes collaborateurs ne font que de l'utilisation d'Anubis et du portage Linux -> Windows), et qu'il comporte déjà 800 pages de C et plus de 1200 pages d'Anubis. Mon expérience m'a montré qu'on développe beaucoup plus vite en Anubis qu'en C, surtout parce qu'on ne débogue presque pas, le compilateur Anubis étant beaucoup plus exigeant qu'un compilateur C. Comme tu n'as expérimenté Anubis que depuis quelques jours (6 novembre, d'après les infos administrateur de mon site), tu n'as peut être pas encore eu le temps de bien t'en rendre compte.

Tu as trouvé un bug. C'est fort possible, surtout si tu utilises la version Windows d'Anubis qui est loin d'être aussi bien au point que la version Linux. Ce serait sympa d'entrer en contact avec moi pour que je puisse le corriger, par exemple en donnant des détails sur le forum (pas ici mais sur mon site bien sûr), ou en m'envoyant un mail. Maintenant, ce que j'entends par le slogan 'pas de bug' est que si mon compilateur et ma machine virtuelle sont exempts de bugs (ce qui n'est pas certain; ils consistent en environ 800 pages de C), alors quelle que soit la façon de programmer en Anubis, on ne peut pas faire de bug formel (ce qui ne veut pas dire qu'on ne peut pas faire de bug d'intention). Il y a donc des nuances subtiles.

Je suis bien sûr très satisfait de lire que le formalisme est plaisant. J'ai passé de nombreuses années à paufiner la théoie et la syntaxe. Je suis un peu récompensé. Merci.

Le point 'sécurisation en vue de commercialisation' (qui se conncrétise par les fichiers ankh et djed) n'est qu'une expérience, et je crois que je vais y renoncer. C'est sans grande importance, et j'espère que ça n'a pas géné pour l'installation.

Je ne peux bien sûr que t'encourager à continuer, et surtout à me tenir au courant de tes progrès et de tes problèmes. Mon plus grand problème est le manque de feed-back de la part de mes utilisateurs. Pour la question du bas-niveau dont tu parles, il faudrait me donner plus de détails, pour que je puisse faire quelque chose.

Merci encore de ton intervention et à bientôt j'espère.

[Caine]

Bonjour et Félicitation!

J'ai accroché immédiatement à la syntaxe et à la mentalité simple de ce nouveau venu.

De plus, par certains aspect, il ressemble à du LISP et du Prolog, mes deux langages universitaires préférés.

Je viens d'essayer de "vendre" à mon DG l'apprentissage du langage, pour voir s'il nous approterais des plus.

Notamment ceci:

Dans mes recherches, je suis tombé sur un créateur de langage, rien que ça! Et je pense que son langage (pour l'instant libre et gratuit) pourrait nous être utile. Pourquoi? Il implémente avec une facilité déconcertante certains concepts. Construire un automate finis pour reconnaître un langage est 50 fois plus simple qu'avec d'autres outils. L'intérêt: Preuve de programme, génération d'entête, vérifier le respect de la charte de développement.

Bien sûr, une autorisation me permettra d'en faire plus.
Mais afin de ne pas "mentir" à mon employeur, vous en tant que créateur du langage, peut-il me servir pour les points que j'ai indiqué.

[DrTopos]

Tout en étant bien persuadé qu'Anubis a des qualités qu'on ne trouvera pas ailleurs (résultat non seulement de nombreuses années d'expérimentation et de recherche théorique, mais aussi parce qu'il a été créé par un mathématicien, qui a forcément une vision différente d'un informaticien), je dois avouer qu'il a encore quelques défauts qui, je l'espère, ne sont que des défauts de jeunesse.

Bien entendu, je ne peux que t'encourager à l'utiliser et à le faire utiliser. En essayant d'être aussi objectif que possible, voici comment je vois ses qualités et ses défauts:

Qualités:

• Le compilateur maintient un niveau de cohérence logique bien plus élevé que la plupart des autres compilateurs (C, C++, Java, VB, etc...). La principale conséquence est le très faible temps qu'on passe à déboguer. D'ailleurs, il n'y a pas de débogueur. Depuis 5 ans qu'on utilise ce langage, le besoin ne s'en est pas fait sentir.
  
• Syntaxe réduite et simple, facilité de maintenance et de restructuration des programmes. Risque de régression pratiquement nul. Par exemple, quand je modifie le source du site (250 pages quand même), je ne fais la plupart du temps même pas de test avant de remettre en ligne.
  
• Grande expressivité, grâce notamment à la possibilité de surcharger les symboles (y compris les opérateurs binaire infixes et unaires préfixes), aux paramètres de types (permettant de faire des schémas, analogues des templates du C++), et à la pleine fonctionalité (fonctions de première classe comme par exemple en Caml)

Défauts:

• Lenteur. Toutefois, une nouvelle machine virtuelle est en gestation, et de plus les possibilités supplémentaires d'Anubis 2 amélioreront à la fois les performances et la sûreté.
  
• Pas de compilation fractionnée, ce qui rend le système un peu lourd à manier pour les très gros programmes (quand on commence à compter les lignes de source par 100.000).
  
• Manque d'interfaçage avec l'extérieur sur certains points. Mais bien entendu, on s'en occupe. Ca va changer. Mais tant que je fais tout cela tout seul (ou presque), ça prend du temps.

L'utilisation personnelle et privée est gratuite et libre. Pour une utilisation professionnelle, on peut librement le tester 'pour voir'. Par contre, s'il est mis en exploitation d'une façon où d'une autre, on est prié de prendre un accord avec moi. Il n'y a pas de règle précise (surtout par manque d'expérience de ma part) et tout est négociable. La hot-line est gratuite (on tombe directement sur moi, bien sûr), mais je préfère qu'on utilise le forum de mon site s'il n'y a pas d'urgence vitale. Bien entendu, en cas de projet professionnel (il y en a deux en cours en ce moment), je fais tout mon possible pour satisfaire l'utilisateur.

Pour ce qui est de la création d'automates, il est vrai que l'exemple que j'ai donné dans le tutoriel est alléchant. Toutefois, il ne faut pas s'y tromper. Des générateurs de lexer comme LEX ou FLEX sont indispensables. Il en existe un en Anubis. Je ne l'ai pas mis dans la bibiothèque (je ne sais pas pourquoi d'ailleurs). Il fabrique des automates dans le style de celui que j'ai décrit à partir d'un source de type LEX (expressions régulières). J'avais aussi commencé un clone de YACC/BISON, mais il n'est pas terminé (il fabrique un automate en tous points identique à celui fait par BISON, mais je n'ai pas encore écrit la partie du programme qui transforme cet automate en programme Anubis).

[Caine]

Je me suis inscris et j'ai téléchargé le compilateur Personal Edition.

A chaque page du manuel de ce langage, je suis plus enthousiaste qu'à la page précédente. D'ailleurs, j'en parle à tout le monde dans l'entreprise (je me ballade avec le manuel pour aller en salle de pause).

Je ne peux que recommander de lire le manuel et d'essayer.

[ludovic.fernandez]

Bonjour,
L'un de mes langages préférés est Haskell i.e., typage fort, évaluation paresseuse et parseurs monadiques. DrTopo, comment Anubis aborde t-il ce genre de concepts ?

Ludo

[DrTopos]

Bonjour.

Je réponds d'abord à tes questions. Ensuite je tente une petite comparaison entre Haskell et Anubis (et une petite discussion des fondements théoriques).

Typage fort: Anubis est aussi fortement typé qu'Haskell, peut-être même plus. Quand à Anubis 2, il le sera encore plus, mais de toute façon Anubis 2 appartient à une autre catégorie de langages: les langages avec preuves, et la comparaison avec Haskell n'a alors plus grand sens, puisque ce n'est pas le cas d'Haskell.

Evaluation paresseuse: Anubis 1 fonctionne en évaluation non paresseuse, mais j'ai décidé d'adopter l'évaluation paresseuse (au moins en option) pour Anubis 2. Il y a bien longtemps que je suis convaincu de la supériorité théorique de l'évaluation paresseuse (par exemple via le théorème de Cadiou, que j'ai enseigné à Nantes dans les années 80). Si je ne l'ai pas implémentée dans Anubis 1, c'est surtout parce que c'était déjà assez difficile comme ça de réaliser la machine virtuelle. L'évaluation paresseuse pose de difficiles problèmes d'ordre ou de répétition d'évaluation, dont je n'aime pas top d'ailleurs le traitement qui en est fait en Haskell. Ce problème est aussi fortement lié à celui du déterminisme. Je ne peux pas me lancer dans une discussion là-dessus ici. C'est un sujet qui mériterait un fil à lui tout seul.

Parseur monadique: J'ai beau parcourir le manuel d'Haskell 98, je ne trouve rien sur les 'parseurs monadiques'. Bien sûr, j'ai vu la classe 'Monad', dont je dirai un mot plus loin. Si tu veux discuter des parseurs monadiques, il faut que tu donnes plus d'explications.

Il y a entre Haskell et Anubis des points de ressemblance (en particulier, des définitions de types dans le Prélude d'Haskell et dans l'équivalent en Anubis: le fichier 'predefined.anubis'), et en même temps des différences de fond très importantes.

D'abord les fondements théoriques. Désolé, je vais parler un peu de moi, et ne pas être tendre avec tout le monde. 'Haskell' est le prénom du logicien Haskell Curry (né en 1900), et c'est lui qui a introduit la 'logique combinatoire' qui n'est rien d'autre qu'une forme 'compilée' du lambda-calcul. Ici par 'compilée' j'entends qu'on a remplacé les symboles (variables) par une combinatoire de l'accès aux valeurs (chose que fait à peu près tout compilateur bien sûr). A l'époque de mes débuts en logique (et en informatique), j'ai beaucoup travaillé sur le lambda-calcul en compagnie de mon ami et collègue Jean-Louis Krivine (mon livre de chevet à cette époque était le livre de H. Barendregt: 'The Lambda-Calculus'), et j'ai été amené à lire le livre de Hindley-Lercher-Seldin sur la logique combinatoire de Curry. C'est donc un sujet que je connais bien. Ce n'est qu'un peu plus tard que je me suis tourné vers la logique catégorique et la Théorie des Topos (qui ont été ma source d'inspiration pour Anubis). Il est important de se rendre compte qu'en logique (comme partout ailleurs) il y a des clans (voire des chapelles), et en particulier, on peut distinguer deux grands courants du moins en ce qui concerne la logique appliquée à l'informatique: les lambda-calculistes et les logiciens catégoriciens. La logique catégorique est une discipline recente (premier pas avec W. Lawvere vers 1964-70), et elle s'est considérablement développée depuis. Cette nouvelle logique est de très loin plus fine et plus subtile que le lambda-calcul, qu'elle englobe d'ailleurs. Je suis désolé de devoir dire que les logiciens qui ignorent la logique catégorique, l'ignorent pour de très mauvaises raisons, qui n'ont en tous cas rien d'arguments mathématiques. Les gens de la logique combinatoire de Curry en font manifestement partie. Tout cela pour dire que je considère ces théories (logiques non catégoriques) comme obsolètes, et donc qu'Haskell est fondé sur des mathématiques dépassées.

D'ailleurs, l'emploi du nom 'Monad' pour l'une des classes du prélude d'Haskell me fait quand même doucement sourire. Comme catégoricien, je connais bien les monades. Je t'en inflige la définition: Une monade est un monoïde dans la catégorie monoïdale des endofoncteurs d'une catégorie. Evidemment, cela ne te parle pas beaucoup, mais ce que je voulais seulement dire est que bien qu'on touve la phrase suivante: The term monad comes from a branch of mathematics known as category theory. dans le manuel d'haskell 98 chapitre 7, je ne retrouve rien des monades dans la définition de la classe 'Monad' si ce n'est une vague allusion à la composition des fonctions (dans une monade le produit du monoïde est la composition des endofoncteurs). Conclusion: Haskell n'a strictement aucun rapport avec les catégories, malgré la présence des classes 'Functor' et 'Monad'.

Donc c'est vraiment un autre monde, et c'est cela, je crois, la différence fondamentale. Maintenant que j'ai vidé mon sac, je vais faire quelques comparaisons que j'espère aussi objectives que possible (je suis dans une position délicate bien sûr).

C'est vrai qu'il y a de nombreuses ressemblances. Par exemple:

Envoyé par Haskell

data Maybe a = Nothing | Just a
data [a] = [ ] | a : [a]

Envoyé par Anubis

type Maybe($T): failure, success($T).
type List($T): [ ], [$T, List($T)].

Jusqu'au nom qui est le même pour Maybe (je n'ai pas copié). Il s'agit ici de définition de types absolument équivalentes, encore que le status des sommes de types n'est pas clair en Haskell (de même qu'il n'est pas clair en Caml), à cause du fait que les données dans un type somme sont utilisées par filtrage (pattern matching) ce qui ne tient pas compte du fait qu'une somme est une union disjointe. A vrai dire, Anubis est le seul langage que je connaisse qui en tienne compte. Ceci a d'ailleurs des incidences sur la gestion des erreurs (autre différence très importante entre Haskell/Caml d'une part et Anubis d'autre part).

Le système de types d'Haskell (système de Hindley-Milner) ressemble beaucoup à celui d'Anubis (c'est l'inverse bien sûr, chronologiquement). En particulier, la notion notée avec un quantificateur universel en Haskell correspond aux schémas d'Anubis. Toutefois, le système d'Haskell est plus complexe. La différence essentielles est la possibililité en Haskell de poser des conditions sur les paramètres de type, ce qui n'existe pas en Anubis. J'ai déjà eu l'occasion pandant ma programmation en Anubis de remarquer ce manque. Mais il porte tellement peu à conséquence que je n'ai pas jugé utile d'ajouter ce concept de conditionnement des paramètres de type. Ma position sur ce sujet n'est pas définitive. Toutefois, la Théorie des Topos me donne pour Anubis 2 des mécanismes nettement plus puissants que ces schémas, même avec conditionnement des paramètres de type. Par ailleurs, je crois que le système de typage d'Anubis est nettement plus simple à comprendre que celui d'Haskell. Il serait intéressant justement à ce sujet de connaître l'avis de quelqu'un qui s'est plongé dans les deux langages.

Je reviens sur le filtrage (pattern matching, qu'on trouve comme en Caml en tête des fonctions), car je tiens à souligner la différence avec Anubis. Les conditionnelles d'Anubis, même si elles ressemblent à du filtrage, proviennent d'une idée bien différente. Ce sont les problèmes universels qui en Théorie des Catégories définissent les sommes et les produits de types qui sont à la base de cette conception. Ce n'est certainement pas le cas du filtrage, pour la simple raison que les filtres sont essayés les uns après les autres (Haskell/Caml) alors qu'en Anubis un saut direct est effectué au bon cas de la conditionnelle. Ce comportement est la traduction de la définition catégorique de la somme, ce qui prouve bien (pour les informaticiens en particulier) que le firltrage n'a rien à voir avec les sommes. Les conséquences en matière de sûreté sont importantes. En Haskell, quand aucun des filtres ne peut être franchi il y a déclenchement d'exception. Ceci ne peut pas arriver en Anubis. Le contôle est toujours passé à un et un seul cas. Si les concepteurs de ML/Caml/Haskell connaissaient les catégories (comme ils le prétendent) ils n'auraient pas commis cette erreur grossière (avis personnel bien sûr, mais j'aime bien être incisif de temps en temps).

Autre différence essentielle: les exceptions. En Anubis, pas de notion d'exception, donc aucune exception à capturer. Le comportement est toujours normal, jamais exceptionnel. Bien entendu, il faut un concept de remplacement. Que faire par exemple si une fonction d'ouverture de fichier ne peut pas ouvrir le fichier ? La solution en Anubis est dans la façon d'utiliser le système de types. Ceci revient à dire que la gestion de ce qu'on pourrait appeler quand même les 'exceptions' se fait explicitement et lexicalement au niveau du typage. Il y a un exemple très parlant dans le tutoriel d'Anubis. On pourra reprocher à cette méthode une certaine lourdeur, mais il ne fait aucun doute qu'elle améliore considérablement la sûreté (qui est mon objectif principal).

Essai de conclusion. On l'aura compris, je n'aime pas beaucoup Haskell (j'aime un peu mieux Caml). Je considère que les fondements théoriques sont archaïques. De plus, la syntaxe n'est pas des plus heureuses. Je crois que le novice lira beaucoup plus facilement de l'Anubis que du Haskell. Comprendre le système de typage d'Haskell n'est pas simple. Ce n'est pas le cas d'Anubis. Enfin, malgré quelques ressemblances de surface, je crois que les différences de fond sont très importantes. En pratique, bien sûr, Haskell bénéficie d'une équipe nombreuse, ce qui fait qu'il n'a sûrement pas les défauts de jeunesse d'Anubis (que je développe pratiquement tout seul). Pour terminer je signale qu'Anubis est (comme Haskell et Caml) un langage pleinement fonctionnel (avec fonctions dites de 'première classe'). Anubis peut donc être rangé dans la catégorie 'langages fonctionnels'.

[ludovic.fernandez]

Merci Dr Topos, une réponse réellement intéressante sur laquelle je reviendrai ce week-end e.g., en particulier par l'emploi de "parseurs monadiques" (entre parenthèses pour ne pas m'attirer ta foudre). J'aime les maths et leur histoire et tu nous combles par le contenu de tes propos.

Ludo

[DrTopos]

Bonjour à tous.

Et si on reparlait de monades, puisque ce sujet a été suggéré par Ludo, et qu'il est resté jusqu'à maintenant sans développement.

Je suis tombé par hasard sur un article de Philip Wadler (Université de Glasgow) intitulé Monads for functional programming. Wadler fait semble-t-il partie de l'équipe qui maintient le compilateur Haskell. Dans cet article, il y a des explications beaucoup plus détaillées sur les monades que dans le manuel d'Haskell. Il y aussi une section sur les parseurs monadiques. Malgré cela, la vision des monades qu'ont les informaticiens de Glasgow me laisse assez perplexe. Les monades ne sont pas du tout présentées comme le font les catégoriciens.

Les monades d'Haskell sont motivées (selon Wadler) par une situation de programmation assez courante, et son argument est plutôt convainquant. La motivation des catégoriciens est de nature différente, aboutissant à une définition différente (mais essentiellement équivalente). La définition des matheux est beaucoup plus simple. D'ailleurs, Wadler n'explicite pas précisément le lien entre les deux.

Wadler justifie l'introduction des monades par trois exemples: un portant sur les exception, un portant sur la gestion des états d'une machine (automate), le dernier portant sur la collecte d'information pour l'output. En fait l'idée est d'enrichir un programme existant par des fonctionalités supplémentaires (traiter les exceptions là où elles ne l'étaient pas, se souvenir d'états là où on ne se souvenait de rien, collecter des informations là où on ne collectait rien). Une telle restructuration de programme implique en général une modification de pratiquement tous les types de données, car tous devront tenir compte des nouvelles informations. La monade est essentiellement une sorte de 'template' (au sens du C++), ou type dépendant d'un paramètre de type (Haskell) ou de schéma de type (Anubis). Le rôle de la monade et d'ajouter au type qui va prendre la place du paramètre, les champs ou informations (ou alternatives dans le cas d'Anubis) nouvelles. L'idée est donc assez séduisante, pas seulement pour restructurer un programme mais aussi pour le concevoir même dès le départ d'une manière mieux structurée.

Une monade selon Haskell est donc d'abord un type M(T) où T est un paramètre représentant un type quelconque. Ceci est accompagné de deux fonctions 'unit' et 'product' de types:

Code :

1
2
3
unit: T -> M(T)
product: M(T) -> (T -> M(U)) -> M(U)

L'idée est que quel que soit le type T, M(T) représente l'enrichissement du type T. La fonction 'unit' permet donc de convertir les données de l'ancien type vers le nouveau. La fonction 'product' permet de convertir une opération existante en 'nouvelle opération'. Il faut imaginer qu'on a quelque part une (ancienne) fonction f: T -> U, qui a été remplacée par une fonction F: T -> M(U), c'est à dire tenant compte des nouvelles données à produire. Dès lors, la fonction 'product' permet de composer ces nouvelles fonctions. En effet, si on a une donnée d de type M(T) (donc produite par une nouvelle fonction), et si on a la nouvelle fonction F: T -> M(U), le terme:

Code :

1
2
product(d)(F)

sera de type M(U) et sera le nouveau résultat souhaité. Comme on le voit c'est finalement pas très compliqué. On voit que cette notion facilite la restructuration du programme, car même si elle oblige à rajouter du code, elle minimise la modification de l'ancien code. L'ancien code est essentiellement réutilisé, mais pas (ou très peu) modifié. Elle apporte donc une certaine forme de sureté.

Ceci n'est qu'un aspect des choses. Selon le manuel Haskell98, les monades sont surtout une façon d'encapsuler les effets de bords dans un decor fonctionnel. A cause de l'évaluation paresseuse d'Haskell, l'ordre des évaluations est assez aléatoire. Or les effets de bord doivent être effectués dans un ordre précis. La fonction 'product' de chaque monade permet de séquencer ces effets dans l'ordre voulu.

Ce que j'ai dit ci dessus ne suffit pas à définir précisément les monades. Pour que tout ceci soit vraiment une monade (toujours selon Wadler, mais aussi pour être conforme à la notion mathématique de monade), il faut que les opérations 'unit' et 'product' satisfassent certaines relations. Ces relations ne sont pas très faciles à comprendre sur le modèle des monades d'Haskell. Elles sont par contre parfaitement claires dans la version mathématique.

Bon, ce fil est-il l'endroit pour exposer un peu de théorie des catégories et la structure de monade ? Pas sûr. Je vais donc en rester là pour aujourd'hui, mais je suis prêt bien sûr à répondre à toutes les questions.

[@drien]

L'exe d'Anubis 1.6 pour Win32 a une taille de 0 octets quand j'essaye de le télécharger

[DrTopos]

Envoyé par @drien

L'exe d'Anubis 1.6 pour Win32 a une taille de 0 octets quand j'essaye de le télécharger

C'est arrangé. Désolé. C'était une erreur stupide.

[Jean-Marc.Bourguet]

Envoyé par DrTopos

Bon, ce fil est-il l'endroit pour exposer un peu de théorie des catégories et la structure de monade ? Pas sûr. Je vais donc en rester là pour aujourd'hui, mais je suis prêt bien sûr à répondre à toutes les questions.

Est-ce que tu as des références à conseiller outre les 3 "lecons" sur ta page?
(Pas uniquement sur le web, un bon livre ne me gène pas; question langue: français ou anglais; mon allemand est trop rouillé pour en faire quelque chose d'utile).

Merci.

[Jedai]

Dans le domaine, le site suivant regorge de références et de discussions intéressantes : http://lambda-the-ultimate.org/

--
Jedaï

[DrTopos]

Envoyé par Jean-Marc.Bourguet

Est-ce que tu as des références à conseiller outre les 3 "lecons" sur ta page?

Il existe des livres parlant de monades bien sûr, par exemple:

S. MacLane: Categories for the Working Mathematician. chez Springer-Verlag. C'est le grand classique par l'inventeur même des catégories. Pas vraiment orienté informatique, mais élémentaire (sauf peut-être la fin) et très bien écrit. Il donne un large panorama des applications des catégories en maths, et il y a un chapitre sur les monades.

E. Manes. Algebraic Theories Springer. Ce livre expose la généralisation catégorique de l'algèbre universelle de Birkoff (1935). Il s'agit d'une théorie élaborée dans les années 60, dans laquelle les monades jouent le premier rôle. C'est un peu plus proche certainement des préoccupation des informaticiens.

Il y a certainement des tas d'autres choses plus récentes sur les monades (et la notion duale de 'comonade').

J'ai prévu au moins une dizaine de leçons de logique catégorique, mais je progresse très lentement. Dans ces leçons, les monades ne sont pas pour tout de suite. J'ai voulu écrire ces leçons pour deux raisons: (1) il n'existe pas grand chose en français sur le sujet, (2) le coeur du sujet de ces leçons est l'application à l'informatique, autant que la logique catégorique elle-même.

[DrTopos]

Envoyé par Jedai

Dans le domaine, le site suivant regorge de références et de discussions intéressantes : http://lambda-the-ultimate.org/

Effectivement. C'est d'ailleurs en passant par là que j'ai trouvé les articles Wadler.

[Jean-Marc.Bourguet]

Envoyé par DrTopos

Il existe des livres parlant de monades bien sûr, par exemple:

S. MacLane: Categories for the Working Mathematician
E. Manes. Algebraic Theories Springer.

J'ai commandé le premier, le second a l'air inconnu de mes sources habituelles.

[DrTopos]

J'ai trouvé un Manes d'occasion ici. C'est peut-être un peu cher. Il semble épuisé, même chez Springer.

[Jean-Marc.Bourguet]

Envoyé par DrTopos

J'ai trouvé un Manes d'occasion ici. C'est peut-être un peu cher. Il semble épuisé, même chez Springer.

Ca fait pourtant partie de mes sources habituelles; chercher avec le prénom complet aide (E. Manes, E. G. Manes, Ernest Manes donnent des résultats différents, ça aide à la recherche)

[Caine]

Je suis impressionné par l'IDE qui vient d'être développé pour Anubis.

Je ne sais pas comment ce développeur à fait pour être aussi rapide, mais je lui adresse toute mes félicitations!

[@drien]

Sauf que le site est hors ligne aparement j'arrive pas à aller dessus (sur le site de l'IDE pas de Anubis).

[Anonn]

A quand la partie Anubis sur le forum : Ce language a l'air interressant.