Relacionar la teoría de las categorías con la teoría de los lenguajes de programación

Question

Me pregunto cuál es la relación de la teoría de las categorías con la teoría del lenguaje de programación.

He estado leyendo algunos libros sobre la teoría de las categorías y la teoría de los topos, pero si por casualidad alguien sabe cuáles son las conexiones y pudiera decírmelo sería muy útil, ya que eso me daría motivos para continuar con este empeño con fuerza, y saber dónde buscar.

Motivación: Actualmente estoy investigando sobre la educación matemática de pregrado/graduado, específicamente la enseñanza de la programación a los graduados/graduados en matemáticas. Estoy jugando con la idea de que si toco los puntos fuertes de los matemáticos puedo instruirlos mejor en la programación y serán mejores programadores, y lo que aprendan les será útil. Estoy en el proceso (muy temprano) de escribir un libro de texto sobre el tema.

Answer 1

Las conexiones que he visto son en el área de la semántica denotacional y la teoría de tipos. Por ejemplo, los objetos pueden ser los tipos Entero, Lista(Entero), Entero+Lista(Lista(Entero)), etc. Las funciones (en el lenguaje) son flechas entre los objetos. (Así, la función sucesora es una flecha de Entero a Entero.) Entonces las construcciones categóricas se traducen en construcciones del lenguaje de programación ("Lista" es un endofuntor, por ejemplo). La existencia de funciones recursivas está garantizada por ciertas propiedades categóricas de la categoría, etc.

Answer 2

Si quieres ensuciarte las manos, busca en el lenguaje de programación Haskell, que tiene funtores y transformaciones naturales.

Los funtores implementan la estructura. Por ejemplo, considere la categoría de tipos T y un functor L que envía un tipo t al tipo L(t), listas de t. Esto es algo similar al functor sobre Set que envía un conjunto X al conjunto de todas las listas finitas sobre el conjunto X (es decir, el conjunto subyacente del monoide libre sobre X). También se podría considerar un functor B que envía un tipo t al tipo B(t) de un árbol binario sobre t.

Ahora se puede definir una transformación natural de B(t) a L(t) como flatten, que toma un árbol binario y lo aplana a una lista. Así como los funtores implementan la estructura, las transformaciones naturales alteran la estructura.

La cosa se pone interesante cuando se introducen las mónadas. Usando el functor de lista anterior, piensa en L(L(t)), listas de listas. Puedes concatenar una lista de listas en una sola lista, lo que corresponde al mapa de mónadas L(L(t)) a L(t).

Mira esto lien para más.

Answer 3

Puede disfrutar de El álgebra de la alegría que "da varios análogos de conceptos de la teoría de categorías".

Answer 4

Si quieres una descripción muy básica, de nivel de entrada, de la teoría de categorías desde el punto de vista de la programación Haskell (no es exactamente lo que el OP pidió),

• http://en.wikibooks.org/wiki/Haskell/Category_theory

es agradable.