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

118

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?

Rafael
fuente
1
Aprecio que distingas programación y cs.
jmite
44
"La teoría de la categoría de aprendizaje para mejorar en Haskell" es un poco como "Aprender física para mejorar en el tenis"
user26756

Respuestas:

115

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:ABB fABf

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 fABf

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 MacLaneL i s t×Listprecisamente 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.

Uday Reddy
fuente
3
@UdayReddy Estoy totalmente en desacuerdo con su identificación de la teoría de categorías con la teoría de tipos. La teoría de tipos moderna trata de manera sostenible los tipos de procesos de concurrencia, por ejemplo, la tradición teórica de los tipos de sesión. Que yo sepa, no existe una comprensión categórica de tales sistemas de escritura.
Martin Berger el
66
@ MartinBerger Creo que su interpretación de la "teoría de tipos" es un poco limitada. Sin embargo, estoy de acuerdo en que una comprensión adecuada de la teoría de tipos y la teoría de categorías de los tipos de sesiones es actualmente un buen desafío de investigación, en el que tengo la intención de pasar el tiempo.
Uday Reddy
2
@MartinBerger. Para ver cómo la teoría de categorías se aplica a las nociones más ricas de computación, lo invito a ver cómo se ha aplicado a la teoría de la programación imperativa y a la semántica de juegos (que nuevamente puede codificar los cálculos imperativos bastante bien). Por lo tanto, no creo que la programación funcional tenga el monopolio de la teoría de categorías.
Uday Reddy
1
@nicolas, las fibraciones son una forma de hacer categorías indexadas, que modelan tipos dependientes. Las fibras también se pueden ver como una forma muy general de lógica de programa, donde significa que asigna valores satisfactorios a -valores satisfactorios. f P Qf:PQfPQ
Uday Reddy
2
"Desafortunadamente, no parece haber ningún libro de texto sobre teoría de categorías dirigido específicamente a los programadores". Tal "libro de texto" ahora existe más o menos en la teoría de categorías para programadores de Bartosz Milewski . Bartosz también ha creado una serie de conferencias acompañantes .
alx9r
30

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 BAB f:AB
  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.

cody
fuente
1
"idear nociones que sean útiles para los matemáticos pero que también sean omnipresentes en la práctica de la programación de Haskell". ¿Puede dar un ejemplo o requeriría demasiado conocimiento previo?
Raphael
77
@Raphael: Mónadas. Flechas Álgebras Coalgebras
Dave Clarke
66
Functores, dualidad, la categoría Kleisli, el lema de Yoneda ...
cody
44
Cartesión de categorías cerradas. Zurra.
Dave Clarke el
2
"Una introducción a la teoría de categorías para ingenieros de software", cs.toronto.edu/~sme/presentations/cat101.pdf
Vladimir Alexiev
29

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.

Martin Berger
fuente
77
No, para ser honesto, Haskell realmente es tan diferente de la mayoría de los otros lenguajes de programación, hasta el punto de que superar las nociones preconcebidas es a menudo el mayor desafío. Los desarrolladores de software experimentados parecen tener más problemas que las personas que nunca antes han programado.
CA McCann
55
@CAMcCann Estoy de acuerdo en que algunos programas experimentados parecen tener dificultades para pasar, por ejemplo, de Java o C # a Haskell, pero no creo que sea porque hay algo fundamentalmente diferente en Haskell. Creo que es en parte porque parece ser diferente. La idea de que necesita aprender teoría de categorías para apreciar a Haskell probablemente ha impedido que muchos desarrolladores de software con experiencia logren el dominio de Haskell. (Cf. por qué F # no tiene mónadas.) Ciertamente me resulta difícil pensar en muchas características de Haskell que no tienen semejanzas en otros idiomas.
Martin Berger el
55
Conocer la teoría de categorías podría ayudar un poco, pero no mucho, y aprender que es sin duda mucho más difícil que aprender Haskell. Existen diferencias bastante fundamentales en comparación con la mayoría de los idiomas (pureza, evaluación no estricta, el sistema de tipos), y eliminar todos los términos de CT no los hace más familiares. Por otro lado, aprender Haskell motiva a algunas personas a aprender algo de CT, porque las ideas prestadas son útiles . El sistema de tipo limitado de F # y la evitación de un término existente perfectamente bueno son fallas, no características.
CA McCann
1
No conozco otro idioma que no sea Scala con un sistema de tipos realmente comparable al de Haskell. Según la observación empírica, la pureza no se capta de inmediato, y la evaluación no estricta (que se omitió) es aún más difícil. Finalmente, soy un programador que trabaja y disputo que alguien en el campo se sienta intimidado por un nombre . La industria del desarrollo de software ya está llena de jerga opaca. Además, el sistema de tipos de F # no puede expresar mónadas directamente: las expresiones de cálculo no son de primera clase, lo que limita su uso significativamente.
CA McCann el
2
CBN también es conceptualmente fácil, por ejemplo, por analogía con thunking, un concepto que la mayoría de los programadores en funcionamiento habrían usado antes. La pureza es algo que todo programador que trabaja comprende. Haskell se utiliza en la educación universitaria en el Reino Unido. Cuando mis alumnos me preguntan cómo ingresar a la programación funcional, a menudo recomiendo aprender Haskell primero, pero los alumnos se sienten intimidados por su reputación, ya que fue el autor de la pregunta. Creo que la razón principal de esto es la asociación de Haskell con la teoría de categorías.
Martin Berger
13

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.

AJed
fuente
1
Levanto una ceja ante esto, porque la "recursión de la cola" generalmente no es importante para programar en Haskell debido a la pereza. Sin embargo, "aprender haciendo" es casi siempre un buen consejo.
Dan Burton
@DanBurton ... observación interesante. Digamos entonces, en lugar de Haskell, aprende erlang o esquema :). [No soy un experto en Haskell, lo acabo de
elegir
0

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í .

shvahabi
fuente
Esto realmente no responde la pregunta: ¿es útil para aprender programación funcional? ¿Qué temas de la teoría de categorías son útiles para Haskell?
David Richerby