Quelle est la définition théorique d'une fonction en Haskell ?

Question

J'aimerais voir, du point de vue des fondations, ce qu'on appelle des fonctions en Haskell.

Vous voyez, d'un point de vue catégorique, il existe des "choses" qui se composent de manière associative, avec une fonction d'identité, et cela suffirait, en théorie.

Mais tout le monde essaie de me convaincre que ce n'est pas ainsi que les fonctions sont définies. Une fonction est définie (disent-ils) comme un ensemble de paires d'éléments de deux ensembles (domaine et codomaine), satisfaisant certaines conditions. Ce qui signifie qu'une fonction est juste un ensemble. Que vous ne pouvez pas définir une fonction sur quelque chose qui n'est pas un ensemble.

Si nous appliquons cette approche à Haskell, je constate que Hask est juste une sous-catégorie de Sets ce qui, pour moi, est bizarre.

Je préférerais étendre la notion de fonction pour l'appliquer à ce que nous avons en Haskell.

Ici dans les commentaires, cette question est abordée de manière tangentielle, mais pas très profonde. J'aimerais entendre une déclaration claire, comme "mais en fait ce sont tous des ensembles", ou "non, nous n'avons rien à voir avec la théorie des ensembles".

Des idées ? Des considérations ?

Answer 1

Il s'agit d'un sujet très complexe. Afin de le rendre simple et gérable, nous faisons souvent des économies et nous "mentons".

Haskell, comme tous les langages de programmation, possède sa propre syntaxe et ses propres règles d'évaluation ( sémantique opérationnelle ). Cependant, le fait de ne penser à un langage de programmation qu'en termes opérationnels peut s'avérer assez limitatif et encombrant. Lorsque nous appelons un factorial nous ne nous soucions pas de la manière dont elle est mise en œuvre, ni du nombre exact d'étapes d'évaluation qu'elle prend pour fournir son résultat.

Pour surmonter ce problème sémantique dénotationnelle a été proposé, où la syntaxe est interprétée, morceau par morceau, dans un modèle "mathématique". Il est possible que de nombreux programmes différents (expressions syntaxiques) correspondent à la même interprétation (la "sémantique").

Pour autant que je sache, une sémantique dénotationnelle pour l'ensemble du langage Haskell n'a jamais été définie. Il existe cependant des modèles pour les fragments Haskell. Ces modèles sont généralement des catégories.

Voici quelques exemples.

Si nous limitons (grandement !) Haskell à un noyau terminant, simplement typé, alors tout ce dont nous avons besoin est une catégorie fermée (bi-)cartésienne, et la catégorie des ensembles suffit, avec ses produits, coproduits et exponentielles.

Cependant, Haskell n'est pas terminatif et possède une récursion générale, nous avons donc besoin de points fixes. Habituellement, ce problème est résolu en passant à la catégorie des ordres partiels complets (généralement un entre omega-CPO ou DCPO).

Ensuite, nous avons besoin de points fixes au niveau du type, donc nous devons considérer une catégorie avec des F-algèbres initiales (au moins pour les foncteurs F bien conformés). Cela rend les choses beaucoup plus complexes.

Nous n'avons pas encore ajouté le polymorphisme ! Ceci est particulièrement délicat puisque Reynolds a prouvé que le polymorphisme ne peut pas être naïvement modélisé par des ensembles ("polymorphism is not set-theoretic" est le principal article de référence). Nous avons donc maintenant les modèles PER et les modèles cohérents (tous deux étant des catégories) comme tentatives de fournir une sémantique au polymorphisme.

Ensuite, nous avons besoin de classes de type, de GADTs, de grades supérieurs, de types supérieurs, ...

En pratique, nous n'avons pas besoin de ce niveau de complexité. Lorsque nous programmons, nous avons généralement affaire à un nombre limité de fonctionnalités, aussi nous nous "mentons" à nous-mêmes et prétendons souvent que tout fonctionne comme un ensemble, ou de manière assez proche. Ensuite, nous ajoutons de la complexité si cela est vraiment nécessaire.