Solicitud de referencia: teoría de categorías aplicada a sistemas de tipos

13

Sigo escuchando acerca de cómo uno debe aprender la teoría de categorías para comprender realmente la teoría del lenguaje de programación. Hasta ahora, he aprendido una gran cantidad de PL sin siquiera entrar en el ámbito de las categorías. Sin embargo, pensé que era hora de dar el salto para ver lo que me había estado perdiendo.

Desafortunadamente, ninguna de las fuentes que puedo encontrar parece hacer conexiones para escribir sistemas o programar. Ellos dicen que es una introducción a la teoría de categorías para los informáticos, pero luego desviarse en sentido general abstracto (lo digo con amor) sin dar ejemplos prácticos o aplicaciones.

Supongo que mi pregunta es realmente doble:

  1. ¿Es esencial la teoría de categorías para comprender los "conceptos profundos" en PL?
  2. ¿Cuál es una fuente que explica la teoría de categorías desde el punto de vista de aplicaciones prácticas para escribir sistemas y programación?

Hasta ahora, lo más lejos que he llegado es a una vaga concepción de los functores (que, hasta donde puedo decir, no parecen estar relacionados con los functores). Temo la abstracción que necesitaré tener en mi cabeza para comprender las mónadas desde una perspectiva teórica de categoría.

cabeza de jardín
fuente
2
@Raphael Es una mala idea hacer una pregunta que consta de dos preguntas diferentes solo vagamente relacionadas entre sí. Pero la pregunta 1. no es subjetiva. Es más bien una solicitud de aclaración y explicación. Supongo que la pregunta 2 se entiende en el sentido de que está contento con una referencia a un lugar donde se explica en lugar de una explicación real también.
Thomas Klimpel
2
En el futuro, es mejor hacer solo una pregunta por publicación. Puede hacer la pregunta 1, luego, dependiendo de las respuestas que obtenga, decida si hacer la pregunta 2 por separado. Eso a menudo hace que las cosas salgan mejor.
DW
1
@Raphael ¿Cómo es subjetiva la pregunta uno? Puede ser difícil de juzgar, ¿es eso lo que quieres decir? Y podría tener como respuesta "Depende de qué tipo de persona seas". - ¿Es eso lo que quieres decir? Todavía podría resultar que es definitivamente esencial o definitivamente no es esencial, ¿verdad? (Y la gente parece estar de acuerdo en que no es esencial.)
k.stm
1
@ k.stm La forma general de la pregunta me preocupa. Si alguien preguntara: "¿El álgebra es esencial para comprender los conceptos profundos de los lenguajes formales?", Sé con certeza que diferentes personas darán diferentes respuestas, en función de sus preferencias y gustos. No espero que sea diferente aquí.
Raphael
1
@Raphael Bien, lo entiendo. Pero creo que son personas que dan respuestas subjetivas a una pregunta objetiva. (Se siente como la gente diciendo “Oh, estoy beber cinco tazas al día y me siento muy bien!” Cuando se le preguntó si el café es saludable o no.)
k.stm

Respuestas:

15

La teoría de categorías no es necesaria para comprender los lenguajes de programación, ni siquiera es necesario hacer una investigación avanzada sobre lenguajes de programación. La mayoría de las personas del lenguaje de programación no conocen (mucho) la teoría de categorías.

Los métodos teóricos de categorías han sido útiles principalmente en una pequeña parte de la investigación del lenguaje de programación, especialmente en el análisis de la programación funcional, particularmente, desde el gran descubrimiento de Moggi de que algunos efectos computacionales tienen una estructura monádica. En la década de 1990, tras el avance de Moggi, se realizó una gran investigación para extender los métodos categóricos a otras formas de lenguajes de programación. Sin embargo, a mi leal saber y entender, los métodos categóricos no se han encontrado tan útiles para OO, cómputo concurrente, paralelo y distribuido, cómputo temporizado o compiladores. Por esta razón, la gente ha abandonado principalmente la extensión de los métodos categóricos.

Los enfoques categóricos para la programación escrita funcionan bien en funciones puras. De hecho, algunos sistemas de mecanografía simples son categorías. Esto se describe, por ejemplo, en

Ahora hay mucho trabajo sobre tipos para procesos concurrentes (por ejemplo, tipos de sesión) y nada de eso es de naturaleza categórica a partir de septiembre de 2016.

Dicho esto, uno nunca puede saber demasiadas matemáticas, y conocer la teoría de categorías es útil. Entonces es una cuestión de costo / beneficio. Si te gustan las matemáticas, si tal vez tienes un poco de experiencia en álgebra (por ejemplo, cuál es el grupo libre en un set, anillo libre, etc.), entonces aprender teoría de categorías será fácil, y si planeas hacer un trabajo que esté (inspirado en) programación funcional, conocer categorías será útil.

Finalmente, la teoría de categorías es una matemática hermosa, y vale la pena estudiarla simplemente porque es muy clara.


Vea la contribución de Uday Reddy en esta discusión para una visión diferente.

Martin Berger
fuente
"Sin embargo, a mi leal saber y entender, los métodos categóricos no se han encontrado tan útiles para ..." Ese es exactamente mi problema. La semántica operativa puede describir con precisión todos estos conceptos, por lo que no sentí que me estuviera perdiendo. Me encantan las matemáticas, pero lamentablemente me falta mi experiencia en álgebra abstracta. Solo entiendo los conceptos básicos básicos de las estructuras algebraicas comunes. Esto ha hecho que la teoría de la categoría de comprensión sea especialmente engorrosa.
cabeza de jardín
2
@gardenhead Entonces, tal vez CT no sea tan útil para ti. Si desea leer muchos documentos en el espacio "Programación funcional", incluido el trabajo sobre tipos, muchos de ellos utilizarán el lenguaje de CT.
Martin Berger
¿Es este un duplicado?
Raphael
2
También sugeriría el libro cs.unibo.it/~asperti/PAPERS/book.pdf "Categorías, tipos y estructuras", que aparentemente está agotado, pero ese es un enlace a un pdf de uno de los páginas de inicio de los autores, así que supongo que es legítimo.
John Forkosh
6

La teoría de la categoría de aprendizaje es una gran inversión de tiempo, y la pregunta de si vale la pena es muy válida. Yo todavía lucha con esto también , y ya sé por qué tengo que aprenderlo. Escribí:

Me gustaba el lenguaje ensamblador cuando comencé a programar, y la teoría de conjuntos se siente similar al lenguaje ensamblador. La teoría de categorías es una alternativa para sortear todos los prejuicios arraigados sobre la lógica y la teoría de modelos integrados en la teoría de conjuntos ZFC convencional.

La idea aquí es usar categorías en lugar de conjuntos o "bits no especificados" como una semántica posible para una teoría de tipos o lenguaje de programación dado. ¿Por qué debería uno querer hacer esto? Considere la dualidad entre una acción y una observación. Las diferentes observaciones (o al menos su orden en el tiempo) no interfieren entre sí (fuera de la mecánica cuántica), pero esto no es necesariamente cierto para diferentes acciones. Los prejuicios arraigados sobre la lógica incrustada en la teoría de conjuntos hacen que sea difícil modelar acciones, en comparación con las observaciones de modelado.


No estoy convencido de que realmente haya una correspondencia perfecta entre la teoría de categorías y la teoría de tipos como se afirma aquí :

Mediante una dualidad sintaxis-semántica, uno puede ver la teoría de tipos como un lenguaje sintáctico formal o cálculo para la teoría de categorías, y por el contrario, uno puede pensar que la teoría de categorías proporciona semántica para la teoría de tipos.

Es cierto que la teoría de categorías puede proporcionar semántica para la teoría de tipos (que puede ser realmente útil), pero dudo que la teoría de tipos realmente proporcione un lenguaje sintáctico formal suficientemente poderoso para expresar todos los cálculos realizados en la teoría de categorías.


En la práctica, la utilidad de la teoría de categorías puede surgir al sugerir preguntas y analogías útiles. Pero la teoría de categorías también puede sugerir actividades y preguntas que al final resultan ser solo una distracción (pérdida de tiempo) de los problemas realmente importantes. Y ciertamente puede aprender lógica y teoría de tipos sin preocuparse por la teoría de categorías.

Thomas Klimpel
fuente
Gracias por tus pensamientos Sus razones para aprender teoría de categorías parecen ser diferentes a las mías; Sus intereses provienen de una perspectiva puramente matemática, mientras que me gustaría ampliar mi comprensión de los tipos. Aún así, es bueno saber que otras personas besdies mismo hallazgo Categoría difícil de abordar y aplicar
gardenhead