Pourquoi la catégorie de types de langue a-t-elle des morphismes, pas des foncteurs?

Question

Je ne sais probablement pas bien cette question bien, alors veuillez supporter avec moi alors que j'essaie d'expliquer ce que je veux dire.

Je travaille sur la théorie de la catégorie d'apprentissage, appliquée à la programmation. Jusqu'à présent, je comprends que:

• Les objets dans une catégorie sont "intacts"; Vous n'êtes pas censé regarder à l'intérieur d'eux pour voir leur structure interne.
• Tout ensemble est une catégorie
• Les types de langue de programmation peuvent être considérés comme des ensembles. (Bool est l'ensemble vrai, faux; int est l'ensemble de tous les entiers; etc.)
• Ainsi, tous les types d'une langue forment une catégorie d'ensembles.
• Les morphismes sont des flèches entre les objets.
• Si ces objets sont eux-mêmes catégories, les morphismes sont appelés les foncteurs.

pris ensemble, cela impliquerait qu'une fonction de Int to Bool est un foncteur, car il s'agit d'une carte de la catégorie définie INT vers la catégorie de jeu BOOL.

Cependant, j'ai également lu ailleurs (en particulier https://www.johndcook.com/blog/2014/05/10/haskell-category-Theary/ ), qui en pensant de cette façon est faux et que nous ne devrions pas parler de types de langue étant une catégorie de base avec des morphismes "juste". Mais je ne vois pas comment cela convient à ma logique précédente.

Je dois donc conclure que ma logique précédente est défectueuse, mais je ne suis pas clair comment ou pourquoi. Quelle est la bonne façon de conceptualiser cela? Sont des ensembles juste des exceptions spéciales supplémentaires? Ou est-ce vraiment juste une question de préférence arbitraire pour savoir comment visualiser l'espace problématique? Ou est-ce que je suis juste plat mal quelque part?

Answer 1

Il y a plusieurs idées flottant ici. Vous pouvez regarder une langue de programmation via une lentille catégorique, puis des types sont des objets et ils sont effectivement opaques. Bool n'est donc pas un ensemble de vrai et de faux dans cette image. C'est un objet qui a deux morphismes (injections) qui y est, l'un correspondant à vrai, et à faux. À Haskell, ce sont les deux constructeurs de Bool. Ils ne prennent aucun argument, mais cela est interprété comme étant des morphismes de l'objet terminal (le type d'unité). Tout fonctionne bien.

Il y a ensuite l'image la plus traditionnelle où les types ne sont que des ensembles de valeurs et de morphismes sont des fonctions entre les ensembles. Les ensembles et fonctions forment un ensemble de catégories. Cette image fonctionne bien tant que vous ne parlez pas de fonction partielle (ceux qui bouclent pour toujours).

Ensuite, il y a la troisième idée que chaque ensemble individuel est une catégorie en soi. C'est une catégorie discrète, ce qui signifie qu'il n'y a pas de morphismes (autres que l'identité) entre les éléments. Dans ce cas, les fonctions entre les ensembles correspondraient effectivement aux foncteurs entre catégories discrètes. Mais un foncteur entre catégories discrètes n'est que une fonction d'objets (éléments) qui est triviale sur les morphismes, ce n'est donc pas un point de vue très intéressant.