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

24

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.

Guy Coder
la source
1
Vous pouvez essayer d'envoyer un courriel à Dave McQueen pour une réponse définitive, je suppose.
Gilles 'SO- arrête d'être méchant'

Réponses:

14

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
Andrej Bauer
la source
15

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 bR n gF:MonGrpF:AbRng

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.

Uday Reddy
la source
"La théorie des catégories ne sait pas encore comment gérer les fonctions d'ordre supérieur." Cela ressemble à une autre question parce que je pensais que la théorie des catégories pouvait tout faire comme base.
Guy Coder
2
Le problème des fonctions d'ordre supérieur est assez simple à énoncer. Un constructeur de type comme n'est pas un foncteur. Ça aurait dû l'être. Une fonction polymorphe comme n'est pas une transformation naturelle. Ça aurait dû l'être. Si vous lisez Eilenberg et MacLane , les intuitions qu'ils présentent couvrent ces cas. Mais leur théorie ne le fait pas. Leur document a été un excellent article pour 1945. Mais, aujourd'hui, nous en avons besoin de plus. t w i c e X = T ( X ) T ( X )T(X)=[XX]twiceX=T(X)T(X)
Uday Reddy
J'en ai fait une vraie question .
Guy Coder
"Une structure ML standard s'apparente à une algèbre ". Les foncteurs ne sont-ils pas un peu plus généraux que ça? Rien n'empêche une structure de contenir des objets non liés (types, valeurs et fonctions), c'est-à-dire. ne formant pas une algèbre.
didierc
2
@didierc Une signature pour les algèbres consiste en une ou plusieurs sortes (comme nos types), et une ou plusieurs opérations (comme nos fonctions) et éventuellement quelques axiomes (comme nos spécifications). Une algèbre pour la signature choisit des ensembles particuliers pour ces sortes et des fonctions particulières pour ces opérations, de sorte que les axiomes sont satisfaits. Les signatures et les structures SML sont précisément de telles choses, sauf que SML permet des opérations d'ordre supérieur, contrairement à l'Algèbre.
Uday Reddy le
3

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.

Gilles 'SO- arrête d'être méchant'
la source
2
Les foncteurs ne sont pas seulement des fonctions sur des objets, ils cartographient également les morphismes. Les foncteurs sont des "morphismes entre catégories".
Andrej Bauer
@AndrejBauer Oui, les foncteurs sont des fonctions sur les objets. Toutes les fonctions sur les objets ne sont pas un foncteur, mais c'est une considération secondaire ici.
Gilles 'SO- arrête d'être méchant'