Monade en programmation Haskell vs Monade en théorie des catégories

Question

J'ai une question sur le concept de monade utilisé dans la programmation Haskell et la théorie des catégories en mathématiques.

Rappel dans Haskell une monade se compose des éléments suivants:

• Un constructeur de type qui définit pour chaque type sous-jacent comment le type de monade correspondant doit être obtenu. Le nom de ce constructeur de type est souvent utilisé comme synonyme de la monade entière. Si$M$ est le nom de la monade et $t$ est un type de données fixe arbitraire, alors $M t$ est le type monadique correspondant

• Une fonction d'unité qui mappe une valeur du type sous-jacent à la valeur du type de monade correspondant. Le résultat est la valeur "la plus simple" du type correspondant qui peut être obtenue à partir de la valeur d'origine. Dans Haskell, cette fonction est appelée retour. La fonction unitaire est de type polymorphe$t → M t$

• Au moins une autre opération, qui décrit la combinaison d'opérations monadiques.

Par contre, dans la théorie des catégories, une monade est un triple $(T, \eta, \mu)$ d'une catégorie $C$ où

• $T: C \to C$ est un foncteur

• $\eta: 1_K \to T$ une transformation naturelle au sens de la théorie des catégories

• $\mu: T^2 \to T$ une transformation naturelle

et ces objets doivent satisfaire les diagrammes suivants: https://en.wikipedia.org/wiki/Monad_(category_theory)

Question: Comment ces monades de Haskell et la théorie abstraite des catégories sont-elles liées? La structure de la monade dans Haskell a-t-elle une «structure de monade» naturelle au sens de la théorie des catégories, c'est-à-dire que nous pouvons associer canoniquement à$M$ un triple canonique comme décrit ci-dessus?

Answer 1

Une monade en Haskell est destinée à être une monade sur la catégorie des types, lorsque la théorie des catégories est faite en interne à la théorie des types. Les capacités de Haskell et des langages similaires sont quelque peu limitées, donc il y a beaucoup de constructions de base dans la théorie des catégories qui ne peuvent pas être faites, mais il y a beaucoup de structures qui peuvent être encodées raisonnablement.

• M :: * → * est le mappage d'objets du foncteur, que vous avez plutôt nommé $T$ plus tard.
• La partie cartographie des flèches du foncteur est donnée par fmap
• $η$est la fonction unitaire, que Haskell appelle return(ou pure, qui est un peu plus générale)
• $μ$est donné par join.

Les exigences attendues des Monadinstances sont équivalentes à celles d'être une monade dans la théorie des catégories.

En gros, ce n'est pas très différent de parler spécifiquement des monades de la catégorie $\mathsf{Set}$, mis à part la mention précédente de Haskell / etc. il manque certaines constructions de la théorie des ensembles (il y a des choses qui agissent assez comme des (co) produits, mais pas comme des pullbacks / pushouts). Vous pourriez faire beaucoup de choses uniquement en pensant aux monades$\mathsf{Set}$, parce que de nombreuses structures en algèbre abstraite / universelle en donnent naissance à une, et sont présentables de cette façon.

On pourrait se plaindre que les types dans divers langages de programmation ne forment pas techniquement une catégorie avec de bonnes propriétés / structure, mais vous pourriez plutôt imaginer que vous les utilisez comme un moyen de parler de quelque chose de mieux se comporter, comme System $F_ω$, et cela ne changerait pas vraiment la réponse d'une manière intéressante.