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

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?

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 $f : A \to B$$A$$B$$f$

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 $A$$B$$f$

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 MacLane→ L i s $\times$$\to$$List$pré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.

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 → $A\rightarrow B$ $f\colon A\rightarrow B$
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.

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.

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.

Voici un (long) article de blog, qui explique pourquoi les idées de la théorie des catégories sont pertinentes pour la programmation pratique: http://cdsmith.wordpress.com/2012/04/18/why-do-monads-matter/

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 .