Demande de référence: théorie des catégories telle qu'elle s'applique aux systèmes de types

Je n'arrête pas d'entendre comment on doit apprendre la théorie des catégories pour vraiment comprendre la théorie du langage de programmation. Jusqu'à présent, j'ai appris beaucoup de PL sans jamais entrer dans le domaine des catégories. Cependant, j'ai pensé qu'il était temps de faire le saut pour voir ce qui m'avait manqué.

Malheureusement, aucune des sources que je peux trouver ne semble établir de connexion avec les systèmes de type ou la programmation. Ils disent que c'est une introduction à la théorie des catégories pour les informaticiens, mais se tournent ensuite vers un non-sens abstrait général (je le dis avec amour) sans donner d'exemples ou d'applications pratiques.

Je suppose que ma question est en fait double:

1. La théorie des catégories est-elle essentielle pour comprendre les "concepts profonds" en PL?
2. Qu'est-ce qu'une source qui explique la théorie des catégories du point de vue des applications pratiques pour taper les systèmes et la programmation?

Jusqu'à présent, le plus loin que j'ai obtenu est une conception vague des foncteurs (qui ne semblent pas être liés aux foncteurs en ML, pour autant que je sache). Je redoute l'abstraction que je devrai garder dans ma tête pour comprendre les monades d'un point de vue théorique de catégorie.

La théorie des catégories est pas nécessaire pour comprendre les langages de programmation, il n'est même pas nécessaire de faire des recherches avancées sur les langages de programmation. La plupart des gens du langage de programmation ne connaissent pas (beaucoup) la théorie des catégories.

Les méthodes théoriques de catégorie ont été utiles principalement dans une petite partie de la recherche sur les langages de programmation, à savoir dans l'analyse de la programmation fonctionnelle, en particulier, depuis la grande découverte de Moggi que certains effets de calcul ont une structure monadique. Dans les années 1990, suite à la percée de Moggi, de nombreuses recherches ont été effectuées pour étendre les méthodes catégorielles à d'autres formes de langages de programmation. Cependant, au meilleur de ma connaissance, les méthodes catégorielles n'ont pas été jugées très utiles pour l'OO, le calcul simultané, parallèle et distribué, le calcul temporisé ou les compilateurs. Pour cette raison, les gens ont pour la plupart abandonné l'extension des méthodes catégoriques.

Les approches catégorielles de la programmation typée fonctionnent bien dans les fonctions pures. En effet, certains systèmes de frappe simples sont des catégories. Ceci est décrit par exemple dans

• Catégories pour Types par Roy Crole
• Introduction à la logique catégorielle d'ordre supérieur par Joachim Lambek et Phil Scott.

Il y a maintenant beaucoup de travail sur les types de processus simultanés (par exemple, les types de session) et rien de tout cela n'est de nature catégorique en septembre 2016.

Cela dit, on ne peut jamais trop connaître les mathématiques, et connaître la théorie des catégories est utile. C'est donc une question de coût / bénéfice. Si vous aimez les mathématiques, si vous avez peut-être un peu d'expérience en algèbre (par exemple, quel est le groupe libre sur un ensemble, anneau libre, etc.), l'apprentissage de la théorie des catégories sera facile, et si vous prévoyez de faire un travail qui est (inspiré par) programmation fonctionnelle, connaître les catégories sera utile.

Enfin, la théorie des catégories est de belles mathématiques, et mérite d'être étudiée simplement parce qu'elle est si soignée.

Voir la contribution d'Uday Reddy dans cette discussion pour un point de vue différent.

L'apprentissage de la théorie des catégories est un énorme investissement en temps, et la question de savoir si cela en vaut la peine est très valable. J'ai encore du mal avec ça , et je sais déjà pourquoi je devrais l'apprendre. J'ai écrit:

J'ai aimé le langage d'assemblage lorsque j'ai commencé à programmer, et la théorie des ensembles ressemble au langage d'assemblage. La théorie des catégories est une alternative pour contourner tous les préjugés ancrés sur la logique et la théorie des modèles intégrés dans la théorie des ensembles ZFC.

L'idée ici est d'utiliser des catégories au lieu d'ensembles ou de "bits non spécifiés" comme sémantique possible pour une théorie des types ou un langage de programmation donné. Pourquoi devrait-on vouloir faire cela? Considérez la dualité entre une action et une observation. Différentes observations (ou du moins leur ordre dans le temps) n'interfèrent pas les unes avec les autres (en dehors de la mécanique quantique), mais ce n'est pas nécessairement vrai pour différentes actions. Les préjugés ancrés sur la logique intégrés dans la théorie des ensembles rendent difficile la modélisation des actions, par rapport aux observations de modélisation.

Je ne suis pas convaincu qu'il y ait vraiment une correspondance parfaite entre la théorie des catégories et la théorie des types comme revendiqué ici :

Par une dualité syntaxe-sémantique, on peut considérer la théorie des types comme un langage syntaxique formel ou un calcul pour la théorie des catégories, et inversement, on peut penser que la théorie des catégories fournit une sémantique pour la théorie des types.

Il est vrai que la théorie des catégories peut fournir une sémantique pour la théorie des types (ce qui peut être vraiment utile), mais je doute que la théorie des types fournisse vraiment un langage syntaxique formel suffisamment puissant pour exprimer tous les calculs effectués dans la théorie des catégories.

Dans la pratique, l'utilité de la théorie des catégories peut surgir en suggérant des questions et des analogies utiles. Mais la théorie des catégories peut également suggérer des activités et des questions qui, en fin de compte, ne sont qu'une distraction (perte de temps) des questions vraiment importantes. Et vous pouvez certainement apprendre la logique et la théorie des types sans vous soucier de la théorie des catégories.