Statu quo de la théorie des catégories et des monades dans la recherche théorique en informatique?

Contexte . Je suis un étudiant de baccalauréat qui s'intéresse à la recherche liée à la théorie des catégories, aux monades et à Haskell, et je veux trouver un sujet pour ma thèse de baccalauréat dans ce domaine.

J'ai regardé le papier

Eugenio Moggi , « Notions de calculs et monades », 1991,

et je ne comprends pas encore grand-chose. J'aurai probablement besoin d'un certain temps pour bien le comprendre. Mais avant de passer plus de temps à l'étudier, je veux mieux comprendre le domaine et son potentiel de recherche. J'en ai récemment parlé à un de mes professeurs et il m'a dit que les monades étaient à la mode dans le milieu de la recherche dans les années 90, mais aujourd'hui elles ne sont plus à la mode.

Par conséquent , je recherche maintenant des travaux récents sur les monades et je me demande:

Dans quels domaines de l'informatique théorique fait-on aujourd'hui des recherches liées à la théorie des catégories et aux monades?
Quel type de recherche a été construit ou proposé sur les travaux d'E. Moggi sur les monades dans la théorie de la programmation? Y a-t-il eu un suivi ou des recherches en cours concernant son article?

reference-request pl.programming-languages big-picture ct.category-theory monad k.stm
la source

Avant de répondre à cette question: ce n'est pas au niveau de la recherche n'est-ce pas? Il peut être mieux adapté à cs.stackexchange.com.

Andrej Bauer

@AndrejBauer Ma thèse de baccalauréat ne sera pas au niveau de la recherche, mais ma question porte sur les recherches en cours ou au moins les recherches effectuées au cours de la dernière décennie.

k.stm

@AndrejBauer Je ne suis pas d'accord. Le site sœur est principalement destiné aux questions de devoirs, alors qu'ici un avis d'expert est nécessaire.

Yuval Filmus

@Kaveh C'était la modification drastique que vous venez de faire. Vous avez amélioré certains points, mais maintenant ce n'est plus vraiment la question que je posais. Quand j'aurai le temps demain, je vais annuler certaines de vos modifications. Par exemple, il est important pour moi d'avoir des antécédents là-dedans. Veuillez me dire quels changements vous paraissent nécessaires et pourquoi je sais quoi ne pas annuler.

k.stm

@Yuval, je pense que beaucoup de gens en informatique seraient fortement en désaccord avec votre commentaire selon lequel c'est principalement pour les devoirs et que les experts ne sont pas présents en informatique . Dans ce cas, Andrej a répondu à plus de 100 questions sur l' informatique .

Kaveh

Réponses:

Il y a eu un certain nombre de développements concernant l'utilisation des monades dans la théorie du calcul depuis les travaux d'Eugenio Moggi. Je ne suis pas en mesure de donner un compte rendu complet, mais voici quelques points que je connais, d'autres peuvent y répondre avec leurs réponses.

Exemples spécifiques de monades

Vous n'avez pas à étudier tout le temps la théorie super-générale. Il existe des exemples de monades très intéressantes et suffisamment compliquées pour remplir une thèse de premier cycle.

J'aime beaucoup le blog de Dan Piponi où il donne des exemples étonnants de la façon dont les monades peuvent être utilisées pour mélanger la programmation fonctionnelle et les mathématiques. Recherchez son travail sur les nœuds et les tresses à travers des monades, par exemple.

Un autre exemple spécifique de mondes à étudier a été donné par Martin Escardo et Paulo Oliva dans le contexte des fonctions de sélection, voir leurs fonctions de sélection, la récursion de la barre et l'induction en arrière , ou peut-être pour vous intéresser, lisez d'abord What Sequential Games, le Tychonoff Theorem et le Double-Negation Shift ont en commun (les fichiers Haskell et Agda associés ici ).

Contexte mathématique

Les monades proviennent de la théorie des catégories et sont beaucoup plus anciennes que Eugenio Moggi. Vous pouvez étudier la théorie de base si vous avez une inclinaison mathématique. Par exemple, vous pourriez attaquer le théorème de monadicité de Beck . Un informaticien théorique ne sait jamais trop de mathématiques.

Variations sur un thème

Vous pourriez regarder quelque chose qui n'est pas strictement monade.

Par exemple, Connor McBride et Ross Paterson's Idioms: la programmation applicative avec effets montre comment on peut généraliser des monades à quelque chose qui est pratiquement pertinent et perspicace.

Ou vous pouvez voir comment les comonades sont utilisées pour modéliser les effets de calcul. Quelqu'un devrait suggérer quelques références pour ce sujet, mais un bon début pourrait être les diapositives de David Overtone .

Théorie des types modaux

Dans la théorie des types d'homotopie, ainsi que dans la théorie des types en général, les monades apparaissent sous la forme d' une théorie de type modale . Récemment, la théorie des types modaux a été considérée dans la théorie des types d'homotopie parce que les opérateurs de troncature sont des exemples d'opérateurs modaux. Et puis il y a la théorie du type homotopique cohésive dans laquelle les opérateurs modaux (qui sont des monades) jouent un rôle essentiel.

Effets algébriques et gestionnaires

[Avertissement: souffler partiellement ma propre corne ici.]

Il y a quelque temps, Gordon Plotkin et John Power ont observé que de nombreux effets de calcul ne sont pas simplement des monades, mais des monades spéciales issues de théories algébriques. Cela a conduit à un tout nouveau traitement des effets de calcul appelés effets algébriques . Plus tard, Gordon Plotkin et Matija Pretnar ont introduit les gestionnaires et, avec les effets algébriques, ils forment une très belle théorie des effets de calcul. Un avantage de cette approche est que les théories algébriques peuvent être facilement combinées, contrairement aux monades.

Vous pourriez étudier comment les effets algébriques se rapportent exactement aux monades. Vous pouvez voir comment les gens ont implémenté des effets algébriques et des gestionnaires, par exemple dans le langage Eff ou dans Haskell en tant que bibliothèque . Il s'agit de recherches plus ou moins actuelles.

Andrej Bauer
la source

Salut, merci pour cette réponse! J'ai cliqué sur votre site Web à propos d'Eff, et il semble que le lien vers An Introduction to Algebraic Effects and Handlers soit obsolète, c'est-à-dire que le fichier eff-lang.org/handlers-tutorial.pdfest manquant.

k.stm

J'ai demandé à Matija de corriger le lien, en attendant, vous pouvez consulter arxiv.org/abs/1203.1539 .

Andrej Bauer

Je le suis déjà. Pouvez-vous, en passant, donner un bref aperçu de la théorie de base que je dois étudier pour comprendre votre article? Je connais une théorie des catégories, un calcul lambda non typé et une théorie élémentaire du calcul et une théorie élémentaire de la programmation (je sais ce que sont la sémantique dénotationnelle), mais pas beaucoup plus jusqu'à présent. Je peux par exemple déjà dire à partir de la section 3 de votre article que je dois examiner les règles de frappe (donc peut-être le calcul lambda tapé). Désolé si je suis arrogant ici.

k.stm

Vous devriez en savoir un peu sur l'algèbre universelle et / ou la théorie de Lavwere sur les théories algébriques. Si vous n'êtes pas familier avec les règles de frappe, vous pouvez étudier un manuel général sur les langages de programmation, comme le TAPL de Benjamin Pierce ou les fondements pratiques des langages de programmation de Bob Harper .

Andrej Bauer

Cet article donne quelques travaux récents importants sur les monades.

NietzscheanAI
la source

Salut, merci pour votre réponse. J'apprécierais un peu le contexte, c'est si vous pouvez gagner du temps pour donner quelques détails. (En fait, le papier a une belle introduction sur son contenu, mais j'aimerais toujours voir un certain contexte pour son environnement, comme s'il y a du travail connexe et autres.)

k.stm