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

13

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.

gardenhead
la source
2
@Raphael C'est une mauvaise idée de poser une question qui se compose de deux questions différentes qui ne sont que vaguement liées l'une à l'autre. Mais la question 1. n'est pas subjective. Il s'agit plutôt d'une demande de clarification et d'explication. Je suppose que la question 2. voulait dire qu'il est satisfait d'une référence à un endroit où cela est expliqué au lieu d'une explication réelle aussi.
Thomas Klimpel
2
À l'avenir, il est préférable de poser une seule question par message. Vous pouvez poser la question 1, puis en fonction des réponses que vous obtenez, décidez de poser la question 2 séparément. Cela rend souvent les choses plus fluides.
DW
1
@Raphael Comment la première question est-elle subjective? Il pourrait être difficile de juger - c'est ce que vous voulez dire? Et cela pourrait avoir comme réponse "Cela dépend du type de personne que vous êtes." - c'est ce que tu veux dire? Il pourrait encore se révéler que c'est absolument essentiel ou certainement pas essentiel, non? (Et les gens semblent convenir que ce n'est pas essentiel.)
k.stm
1
@ k.stm La forme générale de la question m'inquiète. Si quelqu'un demandait: "L'algèbre est-elle essentielle pour comprendre les concepts profonds des langages formels?", Je sais pertinemment que différentes personnes donneront des réponses différentes - en fonction de leurs préférences et de leurs goûts. Je ne m'attends pas à ce que ce soit différent ici.
Raphael
1
@Raphael D'accord, je comprends. Mais je pense que ce sont des gens qui donnent des réponses subjectives à une question objective. (On dirait que les gens disent «Oh, je bois cinq tasses par jour et je me sens bien!» Lorsqu'on leur demande si le café est sain ou non.)
k.stm

Réponses:

15

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

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.

Martin Berger
la source
"Cependant, au meilleur de ma connaissance, les méthodes catégoriques n'ont pas été jugées très utiles pour ..." C'est exactement mon problème. La sémantique opérationnelle peut décrire avec précision tous ces concepts, donc je n'avais pas l'impression de manquer. J'adore les mathématiques, mais ma formation en algèbre abstraite fait cruellement défaut. Je ne comprends que les bases nues des structures algébriques courantes. Cela a rendu la compréhension de la théorie des catégories particulièrement lourde.
gardenhead
2
@gardenhead Alors peut-être que CT n'est pas si utile pour vous. Si vous voulez lire beaucoup d'articles dans l'espace "Programmation fonctionnelle", y compris le travail sur les types, alors beaucoup d'entre eux utiliseront le langage de CT.
Martin Berger
Est- ce un duplicata?
Raphael
2
Je suggérerais également le livre cs.unibo.it/~asperti/PAPERS/book.pdf "Catégories, types et structures", qui est apparemment épuisé, mais c'est un lien vers un pdf à partir de l'un des pages d'accueil des auteurs, donc je suppose que c'est légitime.
John Forkosh
6

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.

Thomas Klimpel
la source
Merci pour vos pensées. Vos raisons pour apprendre la théorie des catégories semblent être différentes des miennes; vos intérêts découlent d'une perspective purement mathématique, alors que j'aimerais élargir ma compréhension des types. Pourtant, il est bon de savoir que d'autres personnes assoiffées moi-même trouvent la catégorie difficile à approcher et à appliquer
gardenhead