Quelle est la relation entre les foncteurs en SML et la théorie des catégories?

Dans le même esprit que cette déclaration d' Andrej Bauer dans cette réponse

La communauté Haskell a développé un certain nombre de techniques inspirées de la théorie des catégories, dont les monades sont les plus connues mais ne doivent pas être confondues avec les monades .

Quelle est la relation entre les foncteurs en SML et les foncteurs en théorie des catégories?

Étant donné que je ne connais pas les détails des foncteurs dans d'autres langues telles que Haskell ou OCaml, s'il y a des informations de valeur, veuillez également ajouter des sections pour d'autres langues.

Les catégories forment une (grande) catégorie dont les objets sont les (petites) catégories et dont les morphismes sont des foncteurs entre de petites catégories. En ce sens, les foncteurs de la théorie des catégories sont des "morphismes de taille supérieure".

Les foncteurs ML ne sont pas des foncteurs au sens catégorique du mot. Mais ce sont des "fonctions de taille supérieure" au sens théorique du type.

Considérez les types de données concrets dans un langage de programmation typique comme «petits». Ainsi int, bool, int -> int, etc sont petits, les classes Java sont petites, ainsi struct en C. Nous pouvons recueillir tous les types de données dans une collection appelée Type. Un constructeur de type, tel que listou arrayest une fonction de Typeà Type. C'est donc une "grande" fonction. Un foncteur ML est juste une grande fonction un peu plus compliquée: il accepte comme argument plusieurs petites choses et renvoie plusieurs petites choses. "Plusieurs petites choses réunies" est connue sous le nom de structure en ML. En termes de théorie des types de Martin-Löf, nous avons un univers Type de petits types. Les grands types sont généralement appelés types . Nous avons donc:

1. Les valeurs sont des éléments de types (exemple: 42 : int)
2. types sont des éléments de Type(exemple: int : Type)
3. Signatures ML sont types (exemple: OrderedType)
4. constructeurs de type sont des éléments de type (exemple: list : Type -> Type)
5. ML Les constructions sont des éléments de type (exemple: String : OrderedType)
6. ML foncteurs sont des fonctions entre types (exemple: Map.Make : Map.OrderedType -> Make.S)

Nous pouvons maintenant faire une analogie entre ML et les catégories, sous lesquelles les foncteurs correspondent aux foncteurs. Mais nous remarquons également que les types de données en ML sont comme des "petites catégories sans morphismes", en d'autres termes, ils sont plus des ensembles que des catégories. On pourrait utiliser une analogie entre ML et théorie des ensembles alors:

1. les types de données sont comme des ensembles
2. les types sont comme des classes théoriques d'ensemble
3. les foncteurs sont comme des fonctions classées

Une structure ML standard s'apparente à une algèbre . Sa signature décrit une classe entière d'algèbres de forme similaire.

Un foncteur ML standard est une carte d'une classe d'algèbres à une autre classe d'algèbres. Une analogie est, par exemple, avec les foncteurs , qui ajoute une opération inverse aux monoïdes, ou qui ajoute un monoïde multiplicatif à des groupes abéliens pour former des anneaux. F : A b → R n $F : {\bf Mon} \to {\bf Grp}$$F : {\bf Ab} \to {\bf Rng}$

La plupart de ces idées ont été élaborées dans une série d'articles par Burstall et Goguen dans la conception d'un langage de spécification appelé CLEAR (Références c5 et c6 sur la page DBLP .) David MacQueen travaillait conjointement avec Burstall et Sannella à cette époque, et était intimement familier avec les problèmes. Le système de modules Standard ML est basé sur ces idées.

Ce que la plupart des gens se demanderaient, qu'en est-il des morphismes? Les foncteurs théoriques de catégorie ont une partie objet et une partie morphisme. Les foncteurs ML standard ont-ils les mêmes? La réponse est oui et non.

• La partie OUI de la réponse s'applique si les structures sont de premier ordre. Ensuite, il y a des homomorphismes entre différentes structures de la même signature et les foncteurs ML standard les mappent automatiquement aux homomorphismes de la signature résultante.
• La partie NON de la réponse s'applique lorsque les structures ont des opérations d'ordre supérieur.

Est-ce à dire que Standard ML s'écarte de la théorie des catégories? Je ne pense pas. Je pense plutôt que Standard ML fait la bonne chose, et la théorie des catégories n'a pas encore rattrapé son retard. La théorie des catégories ne sait pas encore comment gérer les fonctions d'ordre supérieur. Un jour, ce sera le cas.

Il n'y a, à ma connaissance, aucune relation formelle entre les foncteurs en théorie des catégories et les foncteurs en ML (SML ou OCaml, ils sont assez proches pour notre propos ici).

Dans la théorie des catégories, les foncteurs sont des fonctions qui opèrent sur des objets. Ils sont un niveau au-dessus des morphismes, qui sont souvent des fonctions qui opèrent sur des éléments (de nombreuses catégories ont des objets qui sont des ensembles avec une certaine structure algébrique et des flèches qui sont des homomorphismes entre ces structures). Un foncteur ML est une fonction qui opère sur des modules, un niveau au-dessus des fonctions qui opèrent sur des valeurs de langage de base. Je pense que la ressemblance s'arrête là.

Les foncteurs ML ont été baptisés par Dave McQueen dans sa révision de 1985 des modules pour ML standard (citeseerx) qui figurait dans le Polymorphism Newsletter (l'article original utilisait l'expression «module paramétrique» - les publications ultérieures ont tendance à utiliser l'adjectif «paramétriqué»). Malheureusement, je ne trouve pas de copie de ce document. Dans son article de 1986 Utiliser les types dépendants pour exprimer la structure modulaire (citeseerx), il donne le nom tel qu'il est établi.