La théorie des catégories est-elle utile pour apprendre la programmation fonctionnelle?

118

J'apprends Haskell et je suis fasciné par la langue. Cependant, je n'ai aucun fond sérieux en mathématiques ou en CS. Mais je suis un programmeur expérimenté.

Je veux apprendre la théorie des catégories afin de devenir meilleur à Haskell.

Quels sujets de la théorie des catégories devrais-je apprendre à fournir une bonne base pour comprendre Haskell?

Raphaël
la source
1
J'apprécie que vous distinguiez la programmation et cs.
Jmite
4
"L'apprentissage de la théorie des catégories pour s'améliorer à Haskell", c'est un peu comme "L'apprentissage de la physique pour s'améliorer au tennis"
user26756

Réponses:

115

Dans une réponse précédente du site d'informatique théorique , j'ai dit que la théorie des catégories est le "fondement" de la théorie des types. Ici, je voudrais dire quelque chose de plus fort. La théorie des catégories est la théorie des types . À l'inverse, la théorie des types est la théorie des catégories . Laissez-moi développer sur ces points.

La théorie des catégories est la théorie des types

En tout langage formel typé, et même en mathématiques normales en utilisant la notation informelle, on finit par déclarer les fonctions avec les types . En écriture, c'est l'idée et sont appelées "types" et que est une "fonction" d'un type à l'autre. La théorie des catégories est la théorie algébrique de tels "types" et "fonctions". (Officiellement, la théorie des catégories les appelle "objets" et "morphismes" afin d'éviter de taper sur la théorie des ensembles des traditionalistes, mais de plus en plus, je vois de plus en plus des théoriciens des catégories lâcher une telle prudence et utiliser les termes plus intuitifs: "type "et" fonction ". Mais,A B ff:ABABf

Nous avons tous appris la théorie des ensembles à partir du lycée. Nous sommes donc habitués à considérer les types tels que et comme des ensembles et les fonctions telles que comme des mappages théoriques des ensembles. Si vous n'y avez jamais pensé de cette façon, vous êtes en forme. Vous avez échappé au lavage de cerveau selon la théorie des ensembles. La théorie des catégories dit qu'il existe de nombreux types et types de fonctions. Ainsi, l’idée des types en tant qu’ensembles est limitante. Au lieu de cela, la théorie des catégories axiomatise les types et les fonctions de manière algébrique. Fondamentalement, c'est ce que la théorie des catégories est. Une théorie des types et des fonctions. Il devient assez sophistiqué, impliquant des niveaux élevés d'abstraction. Mais si vous pouvez l'apprendre, vous acquerrez une compréhension profonde des types et des fonctions.b fABf

La théorie des types est la théorie des catégories

Par "théorie des types", j'entends tout type de langage formel dactylographié, basé sur des règles rigides de formation des termes qui garantissent que tout est vérifié. Il s'avère que chaque fois que nous travaillons dans un tel langage, nous travaillons dans une structure de catégorie théorique. Même si nous utilisons des notations de la théorie des ensembles et pensons de manière théorique, nous finissons toujours par écrire des choses qui ont un sens catégorique. C'est un fait étonnant .

Historiquement, Dana Scott a peut-être été le premier à le réaliser. Il a travaillé à la production de modèles sémantiques de langages de programmation basés sur le calcul lambda typé (et non typé). Les modèles traditionnels de la théorie des ensembles étaient inadéquats à cette fin, car les langages de programmation impliquent une récursion sans restriction, ce qui rend la théorie des ensembles absente. Scott a inventé une série de modèles sémantiques qui capturent les phénomènes de programmation et a compris que le lambda calcul typé représentait exactement une classe de catégories appelées catégories fermées cartésiennes . Il y a beaucoup de catégories fermées cartésiennes qui ne sont pas de la "théorie des ensembles". Mais le lambda calcul typé s’applique également à tous. Scott a écrit un bel essai intitulé " Relier les théories du calcul lambda"expliquant ce qui se passe, dont certaines parties semblent être disponibles sur le Web. L'article original a été publié dans un volume intitulé" To HB Curry: Essais sur la logique combinatoire, le calcul lambda et le formalisme ", Academic Press, 1980. Berry and Curien en est venu à la même réalisation, probablement indépendamment: ils ont défini une machine abstraite catégorique (CAM) pour utiliser ces idées dans la mise en œuvre de langages fonctionnels, et le langage qu'ils ont implémenté s'appelait "CAML", qui est la structure sous-jacente du F # de Microsoft .

Les constructeurs de type standard tels que , , etc. sont des foncteurs . Cela signifie qu’ils mappent non seulement les types sur les types, mais également entre les types et les fonctions entre les types. Les fonctions polymorphes préservent toutes les fonctions résultant des actions du foncteur. La théorie des catégories a été inventée dans les années 1950 par Eilenberg et MacLaneL i s t×Listprécisément pour formaliser le concept de fonctions polymorphes. Ils les ont appelées "transformations naturelles", "naturelles" car ce sont les seules que vous pouvez écrire de manière correcte en utilisant des variables de type. On pourrait donc dire que la théorie des catégories a été inventée précisément pour formaliser les langages de programmation polymorphes, avant même que les langages de programmation ne soient apparus!

Un traditionaliste de la théorie des ensembles n'a aucune connaissance des foncteurs et des transformations naturelles qui se déroulent sous la surface lorsqu'il utilise des notations de la théorie des ensembles. Mais, tant qu’il utilise le système de typage fidèlement, il fait réellement des constructions catégoriques sans s’en rendre compte.


Tout compte fait, la théorie des catégories est la théorie mathématique par excellence des types et des fonctions. Ainsi, tous les programmeurs peuvent tirer des enseignements de la théorie des catégories, en particulier les programmeurs fonctionnels. Malheureusement, il ne semble pas y avoir de manuels sur la théorie des catégories destinés aux programmeurs en particulier. Les livres "Théorie des catégories pour l'informatique" s'adressent généralement aux étudiants / chercheurs en informatique théorique. Le livre de Benjamin Pierce, La théorie des catégories de base pour les informaticiens est peut-être le plus lisible.

Cependant, il existe de nombreuses ressources sur le Web destinées aux programmeurs. La page Haskellwiki peut être un bon point de départ. À la Midlands Graduate School , nous organisons des conférences sur la théorie des catégories (entre autres). Le cours de Graham Hutton était considéré comme un cours "débutant" et le mien comme un cours "avancé". Mais les deux couvrent essentiellement le même contenu, allant à des profondeurs différentes. L'Université de Chalmers a une belle page de ressources sur les livres et les notes de cours du monde entier. Le site de blog enthousiaste de "sigfpe" fournit également beaucoup de bonnes intuitions du point de vue du programmeur.

Les sujets de base que vous voudriez apprendre sont:

  • définition des catégories et quelques exemples de catégories
  • foncteurs, et des exemples d'entre eux
  • transformations naturelles et exemples
  • définitions de produits, coproduits et exposants (espaces fonctions), objets initiaux et terminaux.
  • adjonctions
  • monades, algèbres et catégories de Kleisli

Mes propres notes de cours à la Midlands Graduate School couvrent tous ces sujets, à l’exception du dernier (monades). De nombreuses autres ressources sont disponibles pour les monades de nos jours. Donc, ce n'est pas une grosse perte.

Plus vous connaissez les mathématiques, plus il serait facile d'apprendre la théorie des catégories. La théorie des catégories étant une théorie générale des structures mathématiques, il est utile de connaître quelques exemples pour comprendre le sens des définitions. (Quand j'ai appris la théorie des catégories, j'ai dû créer mes propres exemples en utilisant mes connaissances en sémantique des langages de programmation, car les manuels classiques ne contenaient que des exemples mathématiques, ce que je ne connaissais pas du tout.) Puis vint le brillant livre de Lambek et Scott a appelé " Introduction à la logique catégorique"qui reliaient la théorie des catégories aux systèmes de typage (ce qu'ils appellent" logique "). Il est maintenant possible de comprendre la théorie des catégories simplement en la reliant à des systèmes de typage, même sans connaître beaucoup d'exemples. Beaucoup des ressources que j'ai mentionnées ci-dessus approche pour expliquer la théorie des catégories.

Uday Reddy
la source
3
@UdayReddy Je ne suis absolument pas d'accord avec votre identification de la théorie des catégories avec la théorie des types. La théorie des types moderne concerne essentiellement les types pour les processus de simultanéité, par exemple la théorie des types de session. À ma connaissance, il n’existe pas de compréhension catégorique de tels systèmes de dactylographie.
Martin Berger
6
@MartinBerger Je pense que votre interprétation de la "théorie des types" est un peu étroite. Cependant, je conviens qu’une bonne compréhension des types de session fondée sur la théorie des types et la théorie des catégories est actuellement un bon défi pour la recherche et que je compte y consacrer beaucoup de temps.
Uday Reddy
2
@MartinBerger. Pour voir comment la théorie des catégories s’applique à des notions de calcul plus riches, je vous invite à regarder comment elle a été appliquée à la théorie de la programmation impérative et à la sémantique des jeux (qui peut encore très bien coder des calculs impératifs). Donc, je ne pense pas que la programmation fonctionnelle ait le monopole de la théorie des catégories.
Uday Reddy
1
@nicolas, les fibrations permettent de créer des catégories indexées, qui modélisent des types dépendants. Les fibrations peuvent également être considérées comme une forme très générale de logique de programme, où signifie que mappe les valeurs satisfaisant satisfaisant les valeurs satisfaisant. f P Qf:PQfPQ
Uday Reddy
2
"Malheureusement, il ne semble pas exister de manuels sur la théorie des catégories destinés aux programmeurs en particulier." Un tel "manuel" existe maintenant plus ou moins dans la théorie des catégories pour programmeurs de Bartosz Milewski . Bartosz a également créé une série de conférences d'accompagnement .
Alx9r
30

Je vais essayer de rester bref et gentil. Il existe une correspondance informelle entre les programmes Haskell et certaines classes de catégories, ce qui peut être rendu plus formel avec un peu de travail. Cette correspondance est connue sous le nom de correspondance Curry-Howard-Lambek et concerne:

  1. Types Haskell avec des objets de la catégorie
  2. Termes de type avec morphismes (notez les notations similaires)f : A BAB f:AB
  3. Types de données algébriques avec les objets initiaux
  4. Constructeurs de types avec des foncteurs
  5. etc

La liste est encore longue, mais un point crucial est que vous pouvez définir des choses comme les monades et les algèbres dans la théorie des catégories et proposer des notions utiles aux mathématiciens mais aussi omniprésentes dans la pratique de la programmation Haskell.

Je ne sais pas quel livre recommander, car je n'ai pas trouvé de livre d'introduction entièrement satisfaisant sur les catégories d'informaticiens. Vous pouvez essayer les catégories, types et structures d’Asperti et Longo. L'idée est d'apprendre les définitions de base jusqu'aux adjonctions, puis d'essayer de lire quelques-uns des excellents blogs disponibles pour essayer de comprendre ces concepts.

Cody
la source
1
"proposez des notions qui sont à la fois utiles aux mathématiciens mais aussi omniprésentes dans la pratique de la programmation Haskell" - pouvez-vous donner un exemple, ou faudrait-il trop de connaissances préalables?
Raphaël
7
@Raphael: Monades. Flèches. Algèbres. Coalgebras.
Dave Clarke
6
Functors, dualité, la catégorie Kleisli, le lemme Yoneda ...
cody
4
Cartesion catégories fermées. Currying.
Dave Clarke
2
"Une introduction à la théorie des catégories pour les ingénieurs en logiciel", cs.toronto.edu/~sme/presentations/cat101.pdf
Vladimir Alexiev
29

En écho au conseil de @AJed, je vous recommande de transformer votre déclaration

I want to learn category theory so I can become better at Haskell.

sur sa tête: apprenez Haskell, bâtissez sur votre intuition de programmation. Une fois que vous êtes un gourou de la PF, il sera peut-être plus facile de saisir la théorie des catégories (si vous vous en souciez encore).

La théorie des catégories est simple pour une personne ayant une formation mathématique étendue (groupes, anneaux, modules, espaces vectoriels, topologie, etc.). En l'absence de ce contexte, la théorie des catégories est presque impénétrable. La beauté de la théorie des catégories réside dans le fait qu’elle unifie beaucoup de choses apparemment non liées (par exemple, les adjonctions gauche des foncteurs oublieux incluent les groupes libres, les algèbres enveloppantes universelles, les compactifications Stone-Cech, les abélianisations de groupes, ...), et réduit ainsi la complexité. Mais si vous ne connaissez pas les multiples exemples que la théorie des catégories unifie, la théorie des catégories n’est qu’une couche supplémentaire de complexité qui vous rend la vie plus difficile.

D'après mon expérience, l'apprentissage est plus facile en s'appuyant sur des connaissances déjà acquises. En tant que développeur de logiciels, vous en savez beaucoup sur la programmation, et la programmation Haskell n’est pas très différente de la programmation. Je vous recommande donc d’aborder Haskell d’un point de vue de la programmation pragmatique, en ignorant la théorie des catégories. Le peu de théorie des catégories qui se trouve dans Haskell, par exemple un certain support pour les monades, est beaucoup plus facile à comprendre pour un programmeur sans faire de détour via la théorie des catégories. Après tout, les monades ne sont que de la composition généralisée (et vous en aurez déjà utilisé dans votre pratique de la programmation - même si vous ne le saviez pas), et Haskell ne supporte pas vraiment les monades, car il ne fait pas respecter les lois monadiques.

Martin Berger
la source
7
Non, pour être honnête, Haskell est vraiment différent de la plupart des autres langages de programmation, au point que le plus gros défi consiste à dépasser les notions préconçues. Les développeurs de logiciels expérimentés semblent avoir plus de problèmes que ceux qui n’ont jamais programmé auparavant.
CA McCann
5
@CAMcCann Je conviens que certains programmes expérimentés semblent avoir du mal à passer de Java ou C # à Haskell, mais je ne pense pas que ce soit parce qu'il y a quelque chose de fondamentalement différent chez Haskell. Je pense que c'est en partie parce que cela semble être différent. L’idée que vous devez apprendre la théorie des catégories pour pouvoir apprécier Haskell a probablement empêché un certain nombre de développeurs de logiciel expérimentés d’atteindre la maîtrise de Haskell. (Cf. pourquoi F # n'a pas de monades.) J'ai certainement du mal à penser à de nombreuses fonctionnalités de Haskell qui ne ressemblent pas à d'autres langages.
Martin Berger
5
La connaissance de la théorie Catégorie pourrait aider un peu, mais pas tant que ça, et l' apprentissage , il est certainement beaucoup plus difficile que d' apprendre Haskell. Il existe des différences assez fondamentales par rapport à la plupart des langues (pureté, évaluation non stricte, système de typage), et la suppression de tous les termes CT ne les rend pas plus familiers. Par ailleurs, apprendre Haskell motive certaines personnes à apprendre la TD, car les idées empruntées sont utiles . Le système de types limité de F # et l’évitement d’un terme parfaitement correct existant sont des défauts et non des fonctionnalités.
CA McCann
1
Je ne connais aucune autre langue que Scala avec un système de type vraiment comparable à celui de Haskell. D'après l'observation empirique, la pureté n'est pas immédiatement comprise et l'évaluation non stricte (que vous avez sautée) est encore plus difficile. Enfin, je suis un programmeur actif et je conteste que quiconque sur le terrain sera intimidé par un nom . L'industrie du développement logiciel est déjà pleine de jargon opaque. De plus, le système de types de F # ne peut pas exprimer directement des monades - les expressions de calcul ne sont pas de première classe, ce qui limite considérablement leur utilisation.
CA McCann
2
CBN est également conceptuellement facile, par exemple par analogie avec thunking, un concept que la plupart des programmeurs actifs auront utilisé auparavant. La pureté est quelque chose que tout programmeur qui travaille comprend. Haskell est utilisé dans l'enseignement de premier cycle au Royaume-Uni. Lorsque mes étudiants me demandent comment entrer dans la programmation fonctionnelle, je recommande souvent d'apprendre d'abord Haskell, mais les étudiants sont intimidés par sa réputation, comme l'a été l'auteur de la question. Je crois que la raison principale en est l’association de Haskell avec la théorie des catégories.
Martin Berger
13

Une réponse courte: non [mais ceci n'est qu'un avis]

N'allez pas dans la théorie des catégories ni dans aucun autre domaine théorique pour devenir bon en Haskell. Apprenez des techniques de programmation fonctionnelles, telles que la récursion de la queue, la cartographie, la réduction et autres. Lire autant de code que vous pouvez. Mettre en œuvre autant d'idées que vous pouvez. Si vous avez des problèmes, lisez et lisez.

Si vous voulez une bonne référence théorique pour apprendre Haskell et d'autres paradigmes de programmation fonctionnelle, consultez: Introduction à la programmation fonctionnelle par Lambda Calculus, Greg Michaelson (disponible en ligne). ... Il existe d'autres livres similaires.

AJed
la source
1
Je lève un sourcil à cela, car la "récursion de la queue" n'est généralement pas importante pour la programmation en Haskell en raison de la paresse. Néanmoins, "apprendre par la pratique" est presque toujours un bon conseil.
Dan Burton
@ DanBurton .. observation intéressante. Disons alors, au lieu de Haskell, apprenez erlang ou scheme :). [Je ne suis pas un expert en Haskell, je l'ai juste choisi parce que ça a l'air cool.]
AJed
0

La théorie des catégories est une branche très sophistiquée des mathématiques et sa maîtrise unifiera la plupart de vos apprentissages précédents en leur faisant des instances des mêmes objets abstraits. C'est donc très utile et très intuitif. Mais il est vaste et vaste, et vous vous retrouverez dans une foule de nouveaux concepts qui ne sauront même pas lequel convient à vos besoins et lequel vous devez sauter. Ainsi, votre approche ciblée nécessite un choix de concepts, sinon la maîtrise de celui-ci nécessite inévitablement beaucoup de temps et ne constitue pas un domaine d’autodétermination.

En passant, je suggère un très bon point de départ pour votre présence ici .

Shvahabi
la source
Cela ne répond pas vraiment à la question: est-ce utile pour apprendre la programmation fonctionnelle? Quels sujets de la théorie des catégories sont utiles pour Haskell?
David Richerby