¿Status quo de teoría de categorías y mónadas en la investigación teórica en informática?

Antecedentes . Soy un estudiante de licenciatura que está interesado en investigaciones relacionadas con la teoría de categorías, mónadas y Haskell, y quiero encontrar un tema para mi tesis de licenciatura en esa área.

He mirado el papel

Eugenio Moggi , " Nociones de computaciones y mónadas ", 1991,

y todavía no entiendo mucho. Probablemente necesitaré bastante tiempo para entenderlo completamente. Pero antes de dedicar más tiempo a estudiarlo, quiero comprender mejor el campo y su potencial de investigación. Hace poco hablé con un profesor mío al respecto y me dijo que las mónadas estaban de moda en la comunidad de investigación en los años 90, pero hoy en día no están de moda.

Por lo tanto , ahora estoy buscando trabajo reciente relacionado con las mónadas, y me pregunto:

¿En qué áreas de la informática teórica se realizan actualmente investigaciones relacionadas con la teoría de categorías y las mónadas?
¿Qué tipo de investigación se ha desarrollado o propuesto sobre el trabajo de E. Moggi sobre mónadas en la teoría de la programación? ¿Ha habido algún seguimiento o investigación en curso relacionada con su artículo?

reference-request pl.programming-languages big-picture ct.category-theory monad k.stm
fuente

Antes de responder a esta pregunta: no es a nivel de investigación, ¿verdad? Puede ser más adecuado para cs.stackexchange.com.

Andrej Bauer

@AndrejBauer Mi tesis de licenciatura no será a nivel de investigación, pero mi pregunta aborda la investigación actual o al menos la investigación realizada en la última década.

k.stm

@AndrejBauer No estoy de acuerdo. El sitio hermano es principalmente para preguntas de tarea, mientras que aquí se necesita una opinión experta.

Yuval Filmus

@Kaveh Esa fue la edición bastante drástica que acabas de hacer. Mejoraste algunos puntos, pero ahora ya no es la pregunta que estaba haciendo. Cuando tenga tiempo mañana, revertiré algunos de sus cambios. Por ejemplo, es importante para mí tener los antecedentes allí. Por favor, dime qué cambios crees que fueron necesarios y por qué, así que sé qué no revertir.

k.stm

@Yuval, creo que mucha gente en Ciencias de la Computación estaría muy en desacuerdo con su comentario de que es principalmente para tareas y que los expertos no están presentes en Ciencias de la Computación . En este caso, Andrej ha respondido más de 100 preguntas sobre informática .

Kaveh

Respuestas:

Ha habido una serie de desarrollos con respecto al uso de mónadas en la teoría de la computación desde el trabajo de Eugenio Moggi. No puedo dar una cuenta completa, pero aquí hay algunos puntos con los que estoy familiarizado, otros pueden intervenir con sus respuestas.

Ejemplos específicos de mónadas

No tienes que estudiar teoría súper general todo el tiempo. Hay ejemplos de mónadas que son muy interesantes y suficientemente complicadas para completar una tesis de pregrado completa.

Me gusta mucho el blog de Dan Piponi donde da ejemplos asombrosos de cómo las mónadas se pueden usar para mezclar programación funcional y matemáticas. Busque su trabajo en nudos y trenzas a través de mónadas, por ejemplo.

Martin Escardo y Paulo Oliva dieron otro ejemplo específico de mondas que vale la pena estudiar en el contexto de las funciones de selección, ver sus Funciones de selección, Recursión de barras e Inducción hacia atrás , o quizás para interesarse primero por leer What Sequential Games, The Tychonoff Theorem y the El cambio de doble negación tiene en común (archivos Haskell y Agda asociados aquí ).

Antecedentes matemáticos

Las mónadas provienen de la teoría de categorías y son mucho más antiguas que Eugenio Moggi. Podrías estudiar la teoría de fondo si eres matemáticamente inclinado. Por ejemplo, podrías atacar el teorema de monadicidad de Beck . Un informático teórico nunca puede saber demasiado de matemáticas.

Variaciones sobre un tema

Podrías mirar algo que no es estrictamente mónadas.

Por ejemplo, los modismos de Connor McBride y Ross Paterson : la programación aplicativa con efectos muestra cómo uno puede generalizar mónadas a algo que sea prácticamente relevante y perspicaz.

O podría observar cómo se utilizan las comonads para modelar efectos computacionales. Alguien debería sugerir algunas referencias para este tema, pero un buen comienzo podrían ser las diapositivas de David Overtone .

Teoría de tipo modal

En la teoría de tipos de homotopía, así como en la teoría de tipos en general, las mónadas aparecen en forma de teoría de tipos modal . Recientemente, la teoría de tipo modal se ha considerado en la teoría de tipo de homotopía porque los operadores de truncamiento son ejemplos de operadores modales. Y luego está la teoría del tipo de homotopía cohesiva en la que los operadores modales (que son mónadas) juegan un papel esencial.

Efectos algebraicos y manejadores

[Descargo de responsabilidad: tocar parcialmente mi propio cuerno aquí.]

Hace un tiempo, Gordon Plotkin y John Power observaron que muchos efectos computacionales no son solo mónadas, sino mónadas especiales que surgen de las teorías algebraicas. Esto condujo a un tratamiento completamente nuevo de los efectos computacionales conocidos como efectos algebraicos . Más tarde, Gordon Plotkin y Matija Pretnar presentaron manejadores y, junto con los efectos algebraicos, forman una teoría muy agradable de los efectos computacionales. Una ventaja de este enfoque es que las teorías algebraicas se pueden combinar fácilmente mientras que las mónadas no.

Podrías estudiar cómo se relacionan exactamente los efectos algebraicos con las mónadas. Podrías ver cómo las personas implementaron los efectos y manejadores algebraicos, por ejemplo, en el lenguaje Eff o en Haskell como biblioteca . Esta es una investigación más o menos actual.

Andrej Bauer
fuente

Hola, gracias por esa respuesta! Hice clic en su sitio web sobre Eff, y parece que el enlace a Introducción a los efectos y manejadores algebraicos está desactualizado, es decir, eff-lang.org/handlers-tutorial.pdffalta el archivo .

k.stm

Le pedí a Matija que arreglara el enlace, mientras tanto podías mirar arxiv.org/abs/1203.1539 .

Andrej Bauer el

Yo ya estoy. ¿Puede, por cierto, dar una breve descripción de la teoría de antecedentes que necesito estudiar para comprender su trabajo? Sé algo de teoría de categorías, cálculo lambda sin tipo y algo de teoría elemental de computación y teoría elemental de programación (sé lo que son las semánticas denotacionales), pero no mucho más hasta ahora. Por ejemplo, ya puedo decir en la sección 3 de su artículo que necesito analizar las reglas de escritura (así que tal vez en el cálculo lambda escrito). Lo siento si estoy siendo agresivo aquí.

k.stm

Deberías saber un poco sobre álgebra universal y / o la teoría de Lavwere sobre teorías algebraicas. Si no está familiarizado con las reglas de escritura, podría estudiar un libro de texto general sobre lenguajes de programación, como TAPL de Benjamin Pierce o Fundamentos prácticos de lenguajes de programación de Bob Harper .

Andrej Bauer

Este documento ofrece algunos trabajos recientes importantes usando mónadas.

NietzscheanAI
fuente

Hola, gracias por su respuesta. Le agradecería un poco de contexto, es decir, si puede perder el tiempo para dar algunos detalles. (En realidad, el documento tiene una buena introducción sobre su contenido, pero todavía me gustaría ver algo de contexto para su entorno, como si hubiera un trabajo relacionado y tal.)

k.stm 13/15