¿Qué tipos de programación requieren teoría práctica de categorías?

8

La teoría de categorías tiene aplicaciones en informática teórica y, obviamente, es fundamental para las matemáticas abstractas. He oído que también tiene aplicaciones prácticas directas en programación y desarrollo de software.

¿Para qué tipo de programación es necesaria la teoría de categorías prácticas? ¿Para qué utilizan los programadores la teoría de categorías para lograrlo?

Tenga en cuenta mi uso de "necesario" y "requerir" en esta publicación. Me doy cuenta de que, en cierto sentido, la mayoría de los programadores se beneficiarán de tener experiencia en diferentes tipos de teorías, pero estoy buscando aplicaciones directas donde el uso de la teoría de categorías es esencial, es decir, si no conocía la teoría de categorías, probablemente no podría. hazlo.

También, me gustaría aclarar que con "qué tipo de programación" espero menos una respuesta amplia como "programación funcional" y más para aplicaciones específicas como "escribir software de banco" o "hacer sistemas operativos" . "

    
pregunta Alexander Gruber 26.04.2014 - 03:25

2 respuestas

2

La pregunta es sobre un concepto matemático abstracto (teoría de categorías) mientras se espera una respuesta muy práctica (aplicaciones específicas). Con el debido respeto, creo que esta es una expectativa poco realista.

Los conceptos matemáticos abstractos son parte de los fundamentos de los lenguajes de programación, no de las aplicaciones. Por ejemplo, los tipos de datos son fundamentales para la programación. Cada idioma tiene algún tipo de tipo de datos e implementa un tipo de sistema , ya sea estático o dinámico, fuerte o débil, explícito o implícito, etc. Sin embargo, no existe un estándar.

Por lo tanto, muchos científicos informáticos han intentado utilizar la teoría de categorías para definir un sistema de tipo unificado . Consulte, por ejemplo, Lenguaje de Programación Categórica de Hagino (1987) y Charity (1996), luego ML (2003) y CAML, y Haskell por supuesto, que define una" categoría de Haskell "de tipos, y las funciones de Haskell son morfismos en tipos ...

Este es el caso porque teoría de tipos está estrechamente relacionada con la teoría de categorías . Para citar a JL Bell: "Las categorías pueden verse como teorías de tipo de un cierto tipo ... Por lo tanto, la teoría de tipos está mucho más relacionada con la teoría de categorías que con la teoría de conjuntos ... En términos generales, se puede pensar en una categoría Como una teoría de tipos desprovista de su sintaxis ". Se ha demostrado que, por ejemplo, las categorías cerradas cartesianas corresponden a tipificado λ-calculus y C-monoids corresponden a untyped λ-calculus ...

No creo que la teoría de categorías sea necesaria para ningún tipo de programación, pero es una herramienta muy útil en el diseño e implementación de lenguajes de programación, y especialmente . los que son inherentemente matemáticos. Es por eso que la Programación Funcional se cita a menudo como una programación categórica, y todos los lenguajes de programación mencionados anteriormente son lenguajes FP.

Una introducción recomendada al tema es " Un gusto por la teoría de categorías para científicos informáticos "de BC Pierce (1988). Esta y otra información útil se encontró en una discusión similar en mathoverflow .

    
respondido por el michl 04.06.2014 - 19:20
-2

Es como el modo org para los bancos.

Me doy cuenta de que eso es vago, pero dijiste que querías una respuesta práctica ...

Las categorías tienen que ver con la dualidad (o al menos así es como lo veo) debido al axioma de elección, así que personalmente diría que sería una forma tonta de inducir un sistema de tipo unificado aunque sea un tipo en sí mismo (un instancia de un tipo) es básicamente una categoría.

Los cálculos lambda simplemente escritos no tienen un sistema de tipo axiomático, por lo que se dice que son la base de la teoría de tipos. Esto es diferente de los cálculos lambda que utilizan un sistema de tipo adecuado.

El cálculo lambda simplemente escrito se normaliza fuertemente y, aunque los tipos coincidentes son bastante aburridos, la lógica es sólida.

También el cálculo lambda infinito / dependiente (o puramente tipeado) no se normaliza correctamente, ya que tiene un tipo para todos los tipos, que es básicamente un sistema de tipo de codificación de iglesia.

Las categorías están en todas partes, pero por su naturaleza son casi imposibles de ver de inmediato.

    
respondido por el James F. 28.06.2014 - 07:39

Lea otras preguntas en las etiquetas