¿Es útil la teoría de categorías para aprender programación funcional?

Estoy aprendiendo Haskell y estoy fascinado por el idioma. Sin embargo, no tengo antecedentes serios en matemáticas o CS. Pero soy un programador de software experimentado.

Quiero aprender teoría de categorías para poder mejorar en Haskell.

¿Qué temas de la teoría de categorías debería aprender a proporcionar una buena base para comprender a Haskell?

En una respuesta anterior en el sitio de Teoría de la informática , dije que la teoría de categorías es la "base" para la teoría de tipos. Aquí, me gustaría decir algo más fuerte. La teoría de categorías es la teoría de tipos . Por el contrario, la teoría de tipos es teoría de categorías . Permítanme ampliar estos puntos.

La teoría de categorías es teoría de tipos

En cualquier lenguaje formal escrito, e incluso en matemáticas normales usando la notación informal, terminamos declarar funciones con tipos . Implícita en la escritura, esta es la idea de que y son algunas cosas llamadas "tipos" es una "función" de un tipo a otro. La teoría de categorías es la teoría algebraica de tales "tipos" y "funciones". (Oficialmente, la teoría de categorías los llama "objetos" y "morfismos" para evitar pisar los dedos de los teóricos de los tradicionalistas, pero cada vez más veo teóricos de categorías arrojando tanta precaución al viento y usando los términos más intuitivos: "tipo "y" función ". Pero,$f : A \to B$B $A$$B$$f$

Todos hemos sido educados en la teoría de conjuntos desde la escuela secundaria en adelante. Entonces, estamos acostumbrados a pensar en tipos como y como conjuntos, y funciones como como asignaciones teóricas de conjuntos. Si nunca pensó en ellos de esa manera, está en buena forma. Has escapado del lavado de cerebro teórico de conjuntos. La teoría de categorías dice que hay muchos tipos de tipos y muchos tipos de funciones. Entonces, la idea de los tipos como conjuntos es limitante. En cambio, la teoría de categorías axiomatiza los tipos y funciones de forma algebraica. Básicamente, eso es lo que es la teoría de categorías. Una teoría de tipos y funciones. Se vuelve bastante sofisticado e involucra altos niveles de abstracción. Pero, si puede aprenderlo, adquirirá una comprensión profunda de los tipos y funciones.B $A$$B$$f$

La teoría de tipos es teoría de categorías

Por "teoría de tipos", me refiero a cualquier tipo de lenguaje formal escrito, basado en reglas rígidas de formación de términos que aseguran que todo tipo verifique. Resulta que, cada vez que trabajamos en un lenguaje así, estamos trabajando en una estructura teórica de categorías. Incluso si usamos notaciones de teoría de conjuntos y pensamos teóricamente, terminamos escribiendo cosas que tienen sentido categóricamente. Ese es un hecho asombroso .

Históricamente, Dana Scott pudo haber sido la primera en darse cuenta de esto. Trabajó en la producción de modelos semánticos de lenguajes de programación basados ​​en cálculo lambda con tipo (y sin tipo). Los modelos tradicionales de teoría de conjuntos eran inadecuados para este propósito, porque los lenguajes de programación implican una recursión sin restricciones que carece de teoría de conjuntos. Scott inventó una serie de modelos semánticos que capturaban fenómenos de programación, y se dio cuenta de que el cálculo lambda mecanografiado representaba exactamente una clase de categorías llamadas categorías cerradas cartesianas . Hay muchas categorías cerradas cartesianas que no son "teóricas de conjuntos". Pero el cálculo lambda mecanografiado se aplica a todos por igual. Scott escribió un bonito ensayo llamado " Teorías relacionadas del cálculo lambda"explicando lo que está sucediendo, partes de las cuales parecen estar disponibles en la web. El artículo original fue publicado en un volumen llamado" A HB Curry: Ensayos sobre lógica combinatoria, cálculo y formalismo de Lambda ", Academic Press, 1980. Berry y Curien llegó a la misma conclusión, probablemente de forma independiente: definieron una máquina abstracta categórica (CAM) para usar estas ideas en la implementación de lenguajes funcionales, y el lenguaje que implementaron se llamó "CAML", que es el marco subyacente de F # de Microsoft .

Los constructores de tipo estándar como , , , etc. son functors . Eso significa que no solo asignan tipos a tipos, sino que también funcionan entre tipos a funciones entre tipos. Las funciones polimórficas preservan todas esas funciones resultantes de las acciones del functor. La teoría de categorías fue inventada en 1950 por Eilenberg y MacLane→ L i s $\times$$\to$$List$precisamente para formalizar el concepto de funciones polimórficas. Los llamaron "transformaciones naturales", "naturales" porque son los únicos que puede escribir de forma correcta usando variables de tipo. Entonces, uno podría decir que la teoría de categorías fue inventada precisamente para formalizar lenguajes de programación polimórficos, ¡incluso antes de que los lenguajes de programación surgieran!

Un tradicionalista teórico de conjuntos no tiene conocimiento de los functores y las transformaciones naturales que están ocurriendo bajo la superficie cuando usa anotaciones teóricas de conjuntos. Pero, mientras esté usando el sistema de tipos fielmente, realmente está haciendo construcciones categóricas sin darse cuenta de ellas.

Dicho y hecho, la teoría de categorías es la teoría matemática por excelencia de tipos y funciones. Por lo tanto, todos los programadores pueden beneficiarse al aprender un poco de teoría de categorías, especialmente los programadores funcionales. Desafortunadamente, no parece haber ningún libro de texto sobre teoría de categorías dirigido específicamente a los programadores. Los libros de "teoría de categorías para ciencias de la computación" generalmente están dirigidos a estudiantes / investigadores teóricos de ciencias de la computación. El libro de Benjamin Pierce, Teoría de la categoría básica para informáticos es quizás el más legible de ellos.

Sin embargo, hay muchos recursos en la web, que están dirigidos a los programadores. La página de Haskellwiki puede ser un buen punto de partida. En la Escuela de Graduados de Midlands , tenemos conferencias sobre teoría de categorías (entre otras). El curso de Graham Hutton se definió como un curso "para principiantes" y el mío como un curso "avanzado". Pero ambos cubren esencialmente el mismo contenido, llegando a profundidades diferentes. La Universidad de Chalmers tiene una buena página de recursos sobre libros y notas de conferencias de todo el mundo. El entusiasta sitio del blog "sigfpe" también ofrece muchas buenas intuiciones desde el punto de vista del programador.

Los temas básicos que le gustaría aprender son:

• definición de categorías y algunos ejemplos de categorías
• functors, y ejemplos de ellos
• transformaciones naturales y ejemplos de ellas
• definiciones de productos, coproductos y exponentes (espacios de funciones), objetos iniciales y terminales.
• adjuntos
• categorías mónadas, álgebras y Kleisli

Mis propias notas de clase en Midlands Graduate School cubren todos estos temas excepto el último (mónadas). Hay muchos otros recursos disponibles para las mónadas en estos días. Entonces eso no es una gran pérdida.

Cuantas más matemáticas conozca, más fácil será aprender teoría de categorías. Debido a que la teoría de categorías es una teoría general de las estructuras matemáticas, es útil conocer algunos ejemplos para apreciar lo que significan las definiciones. (Cuando aprendí la teoría de categorías, tuve que inventar mis propios ejemplos usando mi conocimiento de la semántica del lenguaje de programación, porque los libros de texto estándar solo tenían ejemplos matemáticos, de los que no sabía nada). Luego vino el brillante libro de Lambek y Scott llamó " Introducción a la lógica categórica"qué teoría de categorías se relaciona con los sistemas de tipos (lo que llaman" lógica "). Ahora es posible comprender la teoría de categorías simplemente relacionándola con los sistemas de tipos, incluso sin conocer muchos ejemplos. Muchos de los recursos que mencioné anteriormente usan esto enfoque para explicar la teoría de categorías.

Voy a intentar que sea breve y dulce. Existe una correspondencia informal entre los programas de Haskell y ciertas clases de categorías, que pueden hacerse más formales con algún trabajo. Esta correspondencia se conoce como la correspondencia Curry-Howard-Lambek y se relaciona:

1. Tipos de Haskell con objetos de la categoría
2. Términos de tipo con morfismos (tenga en cuenta las notaciones similares)f : A → $A\rightarrow B$ $f\colon A\rightarrow B$
3. Tipos de datos algebraicos con objetos iniciales
4. Constructores tipográficos con functores.
5. etc.

La lista sigue y sigue, pero un punto crucial es que puede definir cosas como mónadas y álgebras en la teoría de categorías y llegar a nociones que sean útiles para los matemáticos pero que también sean omnipresentes en la práctica de la programación de Haskell.

No estoy seguro de qué libro recomendar, ya que no he encontrado un libro introductorio completamente satisfactorio sobre categorías para informáticos. Puede probar Categorías, Tipos y Estructuras de Asperti y Longo. La idea es aprender definiciones básicas hasta adjuntos, y luego intentar leer algunos de los excelentes blogs para tratar de entender estos conceptos.

Haciéndose eco del consejo de @AJed, recomiendo cambiar su declaración

I want to learn category theory so I can become better at Haskell.

sobre su cabeza: aprende Haskell, construyendo sobre tu intuición de programación. Una vez que eres un gurú de FP, puede ser más fácil elegir la teoría de la categoría (si aún te importa).

La teoría de categorías es simple para alguien con una amplia educación matemática (grupos, anillos, módulos, espacios vectoriales, topología, etc.). Al carecer de estos antecedentes, la teoría de la categoría es casi impenetrable. La belleza de la teoría de categorías es que unifica muchas cosas aparentemente no relacionadas (p. Ej., Los elementos secundarios de los funductores olvidadizos incluyen grupos libres, álgebras envolventes universales, compactaciones de Stone-Cech, abelianizaciones de grupos, ...) y, por lo tanto, reduce la complejidad. Pero si no está familiarizado con los múltiples ejemplos que la teoría de categorías unifica, la teoría de categorías es solo una capa adicional de complejidad que le dificulta la vida.

En mi experiencia, aprender es más fácil al construir sobre cosas que uno ya sabe. Como desarrollador de software, usted sabe mucho sobre programación, y la programación de Haskell no es tan diferente de otra programación, por lo que mi recomendación es abordar a Haskell desde un punto de vista de programación pragmática, ignorando la teoría de categorías. La parte de la teoría de categorías que se encuentra en Haskell, por ejemplo, un poco de apoyo para las mónadas, es mucho más fácil de entender para un programador sin desviarse a través de la teoría de categorías. Después de todo, las mónadas son meramente una composición generalizada (y ya habrá usado mónadas en su práctica de programación, aunque sin saber que lo hizo), y Haskell realmente no apoya a las mónadas de verdad, ya que no hace cumplir las leyes monádicas.

Una respuesta corta: no [pero esto es solo una opinión]

No vaya a la teoría de categorías ni a ningún otro dominio teórico para volverse bueno en Haskell. Aprenda técnicas de programación funcional, como la recursividad de cola, el mapa, la reducción y otras. Lea tanto código como pueda. Implementa tantas ideas como puedas. Si tienes problemas, lee y lee.

Si desea una buena referencia teórica para aprender Haskell y otros paradigmas de programación funcional, eche un vistazo a: Introducción a la programación funcional a través del cálculo de Lambda, Greg Michaelson (disponible en línea). ... Hay otros libros similares.

Aquí hay una publicación de blog (larga), que brinda motivación sobre cómo las ideas de teoría de categorías son relevantes para la programación práctica: http://cdsmith.wordpress.com/2012/04/18/why-do-monads-matter/

La teoría de categorías es una rama muy sofisticada de las matemáticas y su dominio unificará la mayoría de sus aprendizajes anteriores al convertirlos en instancias de los mismos objetos abstractos. Por lo tanto, es muy útil y muy intuitivo. Pero es vasto y amplio, y se encontrará con muchos conceptos nuevos que ni siquiera sabrán cuál es el adecuado para sus necesidades y cuál debe omitir. Por lo tanto, su enfoque intencional necesita elección entre los conceptos, de lo contrario, dominarlo inevitablemente requiere mucho tiempo y realmente no es un dominio de autoaprendizaje.

Por cierto, sugiero un muy buen punto de partida para su propósito de estar aquí .