Théorie des catégories (pas) pour la programmation?

21

Après avoir appris Haskell et d'autres langages de FP pas si purs, j'ai décidé de lire sur la théorie des catégories. Après avoir acquis une bonne compréhension de la théorie des catégories, j'ai commencé à réfléchir à la façon dont les concepts de la théorie des catégories peuvent être utilisés pour penser à la conception de programmes, mais peu importe mes efforts, il semble que ce ne soit pas la voie à suivre.

Après avoir passé de nombreuses tentatives infructueuses pour relier la théorie des catégories à la conception de programmes, je suis arrivé à la conclusion que:

  • La théorie des catégories est utile lors de la conception d'un langage de programmation .
  • La théorie des catégories n'est pas quelque chose que vous utilisez lors de la conception de programmes (même lorsque vous utilisez un langage qui a été conçu sur la base des principes de catégorie). Par exemple: lors de la programmation dans Haskell, vous utiliserez des types, des constructeurs de types, des fonctions, des fonctions d'ordre supérieur, etc. pour concevoir votre programme, pas des concepts de théorie des catégories.

En résumé, nous avons un système de couches inférieures (l'ordre est faible à élevé):

Théorie des catégories -> Langage de programmation -> Programme

À une couche particulière, vous utilisez les concepts de la couche sous-jacente immédiate .

Cette compréhension est-elle correcte? Si ce n'est pas le cas et que vous pensez qu'en concevant des programmes, nous pouvons utiliser directement les concepts de la théorie des catégories, veuillez vous référer à certains articles ou articles de blog où cela est démontré.

REMARQUE: En concevant des programmes, j'entends la conception de programmes basés sur différents concepts, comme la concurrence, le parallélisme, la réactivité, le passage de messages, etc.

Ankur
la source
1
Considérez-vous les monades comme faisant partie du ou des programmes de programmation? Flèches?
Dave Clarke
2
Cela me semble être une question philosophique, du moins en partie. Je ne suis pas sûr qu'il y ait une seule bonne réponse. Un adepte de la théorie des catégories appliquera l'intuition acquise lors de la programmation, un autre privilégiera différentes façons de penser.
Raphael
2
La plupart des programmes en cours d'écriture utilisent des langages de programmation non inspirés de la théorie des catégories. Pour autant que je sache, le programmeur moyen n'est pas au courant de la théorie des catégories, et donc la plupart des programmes (y compris votre système d'exploitation et votre navigateur) ne sont pas inspirés par les mathématiques supérieures.
Yuval Filmus
1
@YuvalFilmus: Ma question s'adresse aux langages de programmation fonctionnels
Ankur
1
voir aussi cette question pour quelques applications CS de
monoids

Réponses:

13

Eh bien, cela dépend bien sûr du type de programme que vous essayez de concevoir.

Si vous concevez un programme de comptabilité pour la chocolaterie de votre tante, je doute fort que la théorie des catégories soit très utile.

Mais il y a bien sûr des situations dans lesquelles la théorie des catégories est extrêmement utile dans la conception de programmes (j'entends également par là les structures de données, les bibliothèques, etc.). De telles situations se produisent principalement lorsque les programmes impliqués sont de nature mathématique.

Si vous voulez écrire des programmes qui calculent avec des nombres réels exacts et d'autres structures se produisant dans l'analyse mathématique, la première question à laquelle vous devez répondre est ce que signifie implémenter correctement un objet mathématique compliqué (comme une fonction différenciable, une variété, etc.). ). Ici, cela aide beaucoup à connaître la théorie et la logique des catégories, car elles vous donnent un moyen systématique de traduire les définitions des structures mathématiques en spécifications et en implémentations des structures de données correspondantes. Le mot à la mode que vous devriez rechercher est la théorie de la réalisabilité . Mais ce n'est qu'un exemple.

La meilleure façon de voir comment la théorie des catégories est utile est de regarder des programmes écrits par des gens qui connaissent beaucoup la théorie des catégories (et les mathématiques en général). Martín Escardó et ses fonctionnels impossibles en sont un exemple évident: par exemple:

M. Escardó et P. Oliva: What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common , Mathematically Structured Functional Programming 2010, ACM Press. (avec les fichiers compagnons Haskell et Agda )

Vous pouvez vous plaindre qu'il ne s'agit pas seulement de la théorie des catégories mais aussi de la logique et de la topologie. De telles plaintes seraient gravement malavisées. La meilleure théorie des catégories est toujours mélangée à d'autres choses.

Enfin, je déconseille de tirer de grandes conclusions sur la nature des choses basées sur un peu de lecture auto-assignée.

Andrej Bauer
la source
C'est précisément mon point. Si je conçois un logiciel de comptabilité, le système de saisie sera ma langue de conception. Si je conçois même un logiciel mathématique, j'utiliserai le système de types pour représenter les concepts de la théorie des catégories. Ce qui indique essentiellement que la théorie des types OU les systèmes de types sont des abstractions plus générales que la théorie des catégories.
Ankur
1
C'est une déclaration ridicule. Je pense que vous devriez peut-être en savoir plus avant de faire de telles déclarations. Vous pouvez peut-être commencer par existentialtype.wordpress.com/2011/03/27/the-holy-trinity
Andrej Bauer
Je ne suis pas un chercheur, un doctorant, un scientifique, un mathématicien ou un théoricien des catégories, alors ne vous inquiétez pas de mes déclarations, elles ne seront pas publiées dans des revues scientifiques ou des articles de recherche. Je suis juste un programmeur qui essaie de comprendre l'autre côté de la médaille. Au fait, merci pour le lien.
Ankur
1
Je le sais, c'est précisément pourquoi je suggère que vous fassiez attention à tirer des conclusions comme vous le faites: vous n'avez tout simplement pas les informations nécessaires pour tirer de telles conclusions. Et c'est aussi pourquoi je vous réfère à un article de blog de Bob Harpher plutôt qu'à, disons, un livre technique sur la relation entre la théorie des types et la théorie des catégories. J'essaie d'aider, mais j'attendrais en retour un peu plus de réserve de votre part lorsqu'il s'agit de tirer de grandes conclusions sur la nature de toute une branche des mathématiques.
Andrej Bauer
Par exemple, vous avez déclaré que "la théorie des types est une abstraction plus générale que la théorie des catégories". Ceci est un exemple de déclaration que vous devez savoir ne pas faire sur la base de peu de connaissances. Je travaille professionnellement dans ce domaine et même je serais très prudent de faire une telle conclusion, ou l'opposé.
Andrej Bauer
6

Les gens utilisaient CT pour décrire les types de données.

  1. Le type de données a été défini par une catégorie particulière dont les objets sont des séquences finies de types (langage de spécification), et dont les flèches étaient des projections ou bien des compositions des opérations de type de données. Par exemple, l'objet est le domaine et est le domaine de codage de l'opération push des piles. Cela vous donne la syntaxe, mais vous n'avez toujours pas de notion de sémantique.
  2. Une algèbre, c'est-à-dire une instance du type, est un foncteur de la théorie à Ens, la catégorie des (petits) ensembles. (Nous utilisons "petit" pour éviter le paradoxe de Russell, mais cela n'a pas d'importance.)
  3. Il s'avère que les propriétés de fermeture des catégories correspondent à des familles de théories logiques. Par exemple, si la catégorie de théorie est fermée sous les produits, le type de données peut être axiomatisé par des équations. Si la catégorie de théorie est fermée en prenant des retraits, alors le type de données peut être axiomatisé par des phrases de Horn.

Je ne suis plus sûr que quiconque y prête attention. Je pense que cela , et les liens qui s'y trouvent, l'expliqueraient plus en détail.

Vilcxjo
la source