Explicando os transformadores de mônada em termos categóricos

8

Muitos recursos relacionados a noções categóricas na programação descrevem mônadas, mas nunca vi uma descrição categórica de transformadores de mônada.

Como os transformadores de mônada podem ser descritos nos termos da teoria das categorias?

Em particular, eu estaria interessado em:

  • a relação entre os transformadores de mônada e suas correspondentes mônadas de base;
  • o relacionamento entre eles e as mônadas que estão transformando em novas mônadas;
  • pilhas de transformadores de mônada.
Petr Pudlák
fonte

Respostas:

8

Segundo Oleksandr Manzuk, eles são "tradução de uma mônada ao longo de uma adjunção", consulte "Cálculo de transformadores de mônada com teoria de categorias" . A propósito, esse é o terceiro hit no Google de "transformador de mônada categoricamente". A primeira é uma pergunta sobre o Stackoverflow e a segunda é a sua pergunta.

Andrej Bauer
fonte
7

Aumentando a resposta de Andrej:

Ainda não há um amplo acordo sobre a interface apropriada que os transformadores de mônada devem suportar no contexto de programação funcional. O MTL de Haskell é a interface de fato, mas o Monatron de Jaskelioff é uma alternativa.

Um dos relatórios técnicos anteriores de Moggi, uma visão abstrata das linguagens de programação , discute qual deve ser a noção correta de transformador até certo ponto (seção 4.1). Em particular, ele discute a noção de uma operação para uma mônada, que ele (20 anos depois) revisita com Jaskelioff em transformadores de mônada como transformadores de monóide .

(Essa noção de operação é diferente da noção de Plotkin e Power de uma operação algébrica para uma mônada , que equivale a uma flecha de Kleisli.)

Ohad Kammar
fonte