Teoría de la categoría (no) para la programación?

21

Después de aprender Haskell y otros lenguajes FP no tan puros, decidí leer sobre teoría de categorías. Después de obtener una buena comprensión de la teoría de la categoría, comencé a pensar en cómo los conceptos de la teoría de la categoría se pueden usar para pensar en el diseño de programas, pero no importa cuánto lo intente, parece que este no es el camino a seguir.

Después de pasar muchos intentos fallidos de relacionar la teoría de categorías con el diseño de programas , llegué a la conclusión de que:

  • La teoría de categorías es útil al diseñar un lenguaje de programación .
  • La teoría de categorías no es algo que se usa al diseñar programas (incluso cuando se usa un lenguaje diseñado en base a principios de categoría). Por ejemplo: al programar en Haskell, utilizará tipos, constructor de tipos, funciones, funciones de orden superior, etc. para diseñar su programa, no conceptos de teoría de categorías.

En resumen, tenemos el siguiente sistema de capas (el orden es de menor a mayor):

Teoría de la categoría -> Lenguaje de programación -> Programa

En una capa particular, utiliza los conceptos de la capa subyacente inmediata .

¿Es correcto este entendimiento? Si no es así, y cree que al diseñar programas podemos usar directamente los conceptos de teoría de categorías, consulte algunos artículos o publicaciones de blog donde se está demostrando.

NOTA: Al diseñar programas me refiero a diseñar programas basados ​​en diferentes conceptos, como concurrencia, paralelismo, reactividad, transmisión de mensajes, etc.

Ankur
fuente
1
¿Considera a las mónadas como parte del lenguaje o programas de programación? Flechas?
Dave Clarke
2
Esto me parece una pregunta filosófica, al menos en parte. No estoy seguro de que haya una sola respuesta correcta. Un experto en teoría de categorías aplicará la intuición obtenida de él durante la programación, otro favorecerá diferentes formas de pensar.
Raphael
2
La mayoría de los programas que se escriben usan lenguajes de programación que no están inspirados en la teoría de categorías. Por lo que puedo decir, el programador promedio no es consciente de la teoría de categorías, por lo que la mayoría de los programas (incluido su sistema operativo y su navegador) no están inspirados en matemáticas superiores.
Yuval Filmus
1
@YuvalFilmus: Mi pregunta está dirigida a lenguajes de programación funcionales
Ankur
1
vea también esta pregunta para algunas aplicaciones CS de monoides
vzn

Respuestas:

13

Bueno, eso, por supuesto, depende del tipo de programa que intente diseñar.

Si está diseñando un programa de contabilidad para la tienda de chocolates de su tía, dudo mucho que la teoría de categorías le sea de mucha utilidad.

Pero, por supuesto, hay situaciones en las que la teoría de categorías es enormemente útil en el diseño de programas (con lo que también me refiero a estructuras de datos, bibliotecas, etc.). Tales situaciones ocurren principalmente cuando los programas involucrados son de naturaleza matemática.

Si desea escribir programas que computen con números reales exactos y otras estructuras que ocurren en el análisis matemático, la primera pregunta que debe responder es qué significa implementar correctamente un objeto matemático complicado (como una función diferenciable, una variedad, etc. ) Aquí ayuda mucho saber algo de teoría y lógica de categorías, porque le brindan una forma sistemática de traducir definiciones de estructuras matemáticas a especificaciones e implementaciones de estructuras de datos correspondientes. La palabra de moda que debe buscar es la teoría de la realizabilidad . Pero este es solo un ejemplo.

La mejor manera de ver cómo la teoría de categorías es útil es mirar programas escritos por personas que conocen mucha teoría de categorías (y matemáticas en general). Un ejemplo obvio de esto es Martín Escardó y sus funciones imposibles, por ejemplo:

M. Escardó y P. Oliva: Qué tienen los juegos secuenciales, el teorema de Tychonoff y el cambio de doble negación en la programación funcional común estructurada matemáticamente 2010, ACM Press. (con archivos complementarios Haskell y Agda )

Puede quejarse de que esto no es solo teoría de categorías, sino también lógica y topología. Tales quejas estarían severamente equivocadas. La mejor teoría de categorías siempre se mezcla con otras cosas.

Por último, recomendaría no sacar grandes conclusiones sobre la naturaleza de las cosas basadas en un poco de lectura autoasignada.

Andrej Bauer
fuente
Ese es precisamente mi punto. Si estoy diseñando software de contabilidad, el sistema de tipos será mi lenguaje para el diseño. Incluso si estoy diseñando un software matemático, usaré el sistema de tipos para representar los conceptos de teoría de categorías. Lo que básicamente indica que la teoría de tipos O los sistemas de tipos son abstracciones más generales que la teoría de categorías.
Ankur
1
Esa es una afirmación ridícula. Creo que tal vez deberías aprender un poco más antes de hacer declaraciones tan amplias como esa. Quizás pueda comenzar con existencialtype.wordpress.com/2011/03/27/the-holy-trinity
Andrej Bauer
No soy investigador, doctor, científico, matemático o teórico de la categoría, así que no se moleste por mis afirmaciones, no se publicarán en alguna revista científica o trabajos de investigación. Solo soy un programador que está tratando de entender el otro lado de la moneda. Por cierto, gracias por el enlace.
Ankur
1
Me doy cuenta de esto, que es precisamente por lo que estoy sugiriendo que debe tener cuidado al sacar conclusiones como lo hace: simplemente no tiene la información necesaria para sacar tales conclusiones. Y esta es también la razón por la que lo remito a una publicación de blog de Bob Harpher en lugar de, por ejemplo, un libro técnico sobre la relación entre la teoría de tipos y la teoría de categorías. Estoy tratando de ayudar, pero esperaría a cambio un poco más de reserva de usted cuando se trata de sacar grandes conclusiones sobre la naturaleza de toda una rama de las matemáticas.
Andrej Bauer
Por ejemplo, usted afirmó que "la teoría de tipos es una abstracción más general que la teoría de categorías". Este es un ejemplo de una declaración que debe saber que no debe hacer en base a poco conocimiento. Trabajo profesionalmente en esta área e incluso sería muy cuidadoso de sacar tal conclusión, o la opuesta.
Andrej Bauer
6

La gente solía usar CT para describir los tipos de datos.

  1. El tipo de datos se definió por una categoría particular cuyos objetos son secuencias finitas de tipos (lenguaje de especificación) y cuyas flechas eran proyecciones o composiciones de las operaciones de tipo de datos. Por ejemplo, el objeto es el dominio y es el codominio de la operación de inserción de pilas. Esto le da sintaxis, pero aún no tiene una noción de semántica.
  2. Un álgebra, es decir, una instancia del tipo, es un functor desde la teoría hasta Ens, la categoría de conjuntos (pequeños). (Usamos "pequeño" para evitar la paradoja de Russell, pero en su mayoría no importa).
  3. Resulta que las propiedades de cierre de las categorías corresponden a familias de teorías lógicas. Por ejemplo, si la categoría de teoría se cierra en productos, el tipo de datos se puede axiomatizar por ecuaciones. Si la categoría de teoría se cierra tomando retrocesos, entonces el tipo de datos puede ser axiomatizado por las oraciones Horn.

No estoy completamente seguro de que alguien le preste más atención a esto. Creo que esto , y los enlaces allí, lo explicarían con más detalle.

Vilcxjo
fuente