La relación más evidente con la teoría de las categorías es que tenemos una categoría que consiste en tipos como objetos y funciones como flechas. Tenemos funciones de identidad y podemos componer funciones con los axiomas habituales (con varias salvedades). Eso es sólo el punto de partida.
Un lugar donde se empieza a profundizar es cuando se consideran las funciones polimórficas. Una función polimórfica es esencialmente una familia de funciones, parametrizadas por tipos. O categóricamente, una familia de flechas, parametrizadas por objetos. Esto es similar a lo que es una transformación natural. Introduciendo algunas restricciones razonables, descubrimos que una gran clase de funciones polimórficas son, de hecho, transformaciones naturales, y ahora se aplica mucha teoría de categorías. Los ejemplos estándar que podemos citar aquí son los siguientes teoremas libres .
La teoría de las categorías también encaja perfectamente con la noción de "interfaz" en la programación. La teoría de las categorías nos anima a no mirar de qué está hecho un objeto, sino cómo interactúa con otros objetos y consigo mismo. Al separar una interfaz de una implementación, el programador no necesita saber nada sobre la implementación. Del mismo modo, la teoría de las categorías nos anima a pensar en los objetos hasta el isomorfismo: no proclama con precisión qué conjuntos comprenden nuestros grupos, sólo importa cuáles son las operaciones sobre nuestros grupos. La teoría de las categorías capta precisamente esta noción de interfaz.
También existe una hermosa relación entre el cálculo lambda de tipo puro y las categorías cerradas cartesianas (CCC). Cualquier expresión en el cálculo lambda puede interpretarse como la composición de las funciones estándar que vienen con una CCC: como la proyección sobre los factores de un producto, o la evaluación de una función. Así, las expresiones lambda pueden interpretarse como aplicables a cualquier CCC. En otras palabras, el cálculo lambda es un lenguaje interno para las CCC. Esto se explica en Lambek y Scott. Esto significa, por ejemplo, que la teoría de las CCC está profundamente integrada en Haskell, porque Haskell es esencialmente cálculo lambda tipado puro con un montón de extensiones.
Otro ejemplo es la forma en que la recursión estructural sobre tipos de datos recursivos puede describirse de forma agradable en términos de objetos iniciales en categorías de álgebras F. Puede encontrar algunos detalles aquí .
Y un último ejemplo: dualizar (en el sentido categórico) las definiciones resulta muy útil en el mundo de los lenguajes de programación. Por ejemplo, en el párrafo anterior he mencionado la recursión estructural. La dualización de la misma da lugar a las nociones de F-coalgebras y de recursividad vigilada, y conduce a una buena manera de trabajar con tipos de datos "infinitos", como los flujos. Trabajar con flujos es complicado porque ¿cómo evitar que se intente recorrer inadvertidamente toda la longitud de un flujo causando un bucle infinito? La doble recursividad estructural adecuada conduce a una poderosa forma de tratar con flujos que garantiza un buen comportamiento. Bart Jacobs, por ejemplo, tiene muchos artículos interesantes en esta área.
1 votos
Esto es muy similar a otra pregunta sobre la teoría de categorías y los lenguajes de programación, pero la cambié para reflejar que quería saber algunas conexiones precisas, en lugar de simplemente dónde buscar.
1 votos
Los topos están en una especie de "rama" diferente a la de los lenguajes de programación. Su ancestro menos común sería probablemente las hiperdoctrinas de Lawvere o simplemente las categorías cerradas cartesianas. No se trata de desalentar el aprendizaje de los topoi (¡son fascinantes!), pero no juegan un papel importante en los lenguajes de programación.
4 votos
Además, francamente, creo que los estudiantes de ciencias de la computación estarían mucho mejor si los arrastráramos a través de un semestre de teoría de conjuntos primero. Facilitaría muchas otras cosas; podríamos hablar de "conjuntos recursivos de números naturales" en lugar de problemas decidibles. Pero no creo que se pueda meter suficiente teoría de categorías en la cabeza de un estudiante de grado (incluso de un estudiante de matemáticas) a tiempo para generar un rendimiento significativo de la inversión en términos de comprensión de PL.
4 votos
"Creo que los estudiantes de ciencias de la computación estarían mucho mejor si los arrastráramos a un semestre de teoría de conjuntos primero" ¡Qué pensamiento tan horrible!