Les subtilités de la correspondance entre la théorie des types et la théorie des catégories sont en dehors de mon ken. Cependant, par ma compréhension naïve de la relation entre les deux disciplines historiquement convergentes, cette dernière subsume entièrement la première. Si tel est le cas, le langage et les descriptions formelles / graphiques utilisés par les théoriciens des catégories peuvent-ils remplacer ceux des théoriciens des types? Et devraient-ils (par exemple, dans la pédagogie et l'édition académique)?
Différents formalismes peuvent inspirer de nouvelles perspectives et établir des connexions conceptuelles nues qui pourraient autrement être obscures. Cependant, une multiplicité de dialectes limite probablement aussi la taille d'un public réceptif et, si une approche polyglotte est adoptée, la longueur et la complexité de l'exposition sont aggravées.
Si la théorie des catégories subsume la théorie des types, les différences dialectiques des deux disciplines devraient-elles être conservées, et si oui, pourquoi? Par souci de valeur historique ou culturelle? Pour conserver des différences différentes mais saillantes d'accent pédagogique ou théorique? Que pourraient-ils être?
la source
Réponses:
Puisque vous dites que "les subtilités de la correspondance entre la théorie des types et la théorie des catégories sont en dehors de votre ken", la meilleure façon de comprendre la correspondance est peut-être de lire des expositions non techniques sur le sujet. Je peux en recommander deux:
Steve Awodey, Des ensembles aux types, aux catégories, aux ensembles , dans: Sommaruga G. (éds) Théories fondamentales des mathématiques classiques et constructives. The Western Ontario Series in Philosophy of Science, vol 76. Springer, Dordrecht ( préimpression gratuite ici )
Le blog de Robert Harper The Holy Trinity , et voir également ces diapositives .
Je suppose que la leçon à retenir est que chaque approche a quelque chose à offrir et qu'elles fonctionnent mieux ensemble, et pas tellement si vous essayez de remplacer ou de subsumer l'une avec l'autre.
la source
Ma vue est plus ou moins similaire à celle du chi. Je vois la théorie des catégories comme étant (à peu près) la théorie des types ce que la théorie des modèles est pour la logique. Certaines des conséquences de cela sont, premièrement, chacune peut exister de manière autonome. En effet, la théorie des types est antérieure à la théorie des catégories, et la création de la théorie des catégories n'était pas motivée par ces préoccupations. Deuxièmement, bon nombre des distinctions théorie / théorie des modèles qui tentent délibérément de brouiller sont d'un intérêt primordial pour la théorie des types / la logique.
Comme exemple très basique, toutes les présentations des axiomes d'un groupe donnent naissance à la même classe de modèles (à savoir les groupes). Du point de vue de l'algèbre universelle, une variété (au sens de l'algèbre universelle, ou une catégorie algébrique finitaire du point de vue de la CT) oublie sa présentation. Pendant ce temps, du point de vue de la logique équationnelle, la présentation est tout ce qu'il y a. Un sujet de calcul principal ici est l' unification électronique qui fonctionne entièrement au niveau de la logique équationnelle, c'est-à-dire la présentation.
C'est typique. Nous disons que le lambda calcul simplement tapé (avec produits) (STLC) est le langage interne des catégories fermées cartésiennes, mais ce n'est vraiment qu'une présentation du langage interne et même pas la plus "directe". La machine abstraite catégorique (CAM) est sans doute une représentation plus "directe". Même avec le STLC, les flèches de la catégorie syntaxique correspondante sontβη classes d'équivalence de termes lambda! (Mais voyez ceci .) Donc, soit nous décrivons directement la catégorie syntaxique comme une structure mathématique dont les hom-sets coïncident avecβη classes d'équivalence de termes STLC et sans contenu informatique , ou nous devons déjà comprendre le STLC externe à la théorie des catégories, ou nous devons parler au lieu de présentations de catégories fermées cartésiennes qui, en adoptant une approche assez naturelle, conduiront à quelque chose de CAM -comme. Dans le dernier cas, l'égalité des flèches devient quelque chose comme un problème d'unification électronique. Comprendre et simplifier ce processus ainsi que placer la façade plus ergonomique du STLC devant lui, nécessite des techniques qui sont le pain et le beurre de la logique et de la théorie des types, mais qui ne sont pas particulièrement naturelles dans la théorie des catégories.
Une image massivement simplifiée qui peut néanmoins donner une meilleure idée de l'interdépendance entre la théorie des catégories et la théorie des types est la suivante. Vous pouvez les imaginer en deux dimensions. Les outils, techniques et notations de la théorie des types sont conçus pour se déplacer verticalement entre différentes présentations du même objet, tandis que les outils, les techniques et les notations de la théorie des catégories sont conçus pour se déplacer horizontalement entre différents objets mathématiques. Vous pourriez même dire qu'une catégorie est une ligne verticale entière et que la théorie des catégories parle de déplacer une ligne verticale vers une autre mais pas comment les points des deux lignes correspondent. Dans cette image, la théorie des catégories n'est même pas capable de parler de la théorie des types de distinctions, mais cela est intentionnel car cela signifie que la cartographie arbitrairement compliquée de points sur une ligne verticale avec des points sur une autre est tout simplement sans rapport avec ce à quoi la théorie des catégories se soucie et peut être ignorée.
Dans mon article de blog, Category Theory, Syntactically , je décris une approche qui fait ressembler la théorie des catégories à la théorie des types (plutôt que l'inverse). Sans surprise, ce dont je parle vraiment, ce sont des présentations de catégories. De plus, vous pouvez voir des aspects de la normalisation entrer en scène, par exemple dans ma discussion sur les "théories des produits", même si ce n'est pas du tout un point de ce poste particulier.
la source