Dado que sdvccv ya señaló una serie de buenas fuentes para el aprendizaje de la teoría de las categorías aplicada a la CS, voy a tratar de proporcionar algunos puestos de guía.
Mi libro favorito sobre el tema es Practical Foundations of Mathematics, de Paul Taylor, ya que hace un muy buen trabajo al darte una visión general (desafortunadamente no siempre te da suficientes detalles si no tienes ya una formación en lógica). El libro de Bart Jacobs "Categorical Logic and Type Theory" también es muy fácil de leer.
En general, creo que lo más importante que hay que entender para aplicar las categorías a la informática es la correspondencia Curry-Howard-Lambek, que afirma vagamente que los cálculos lambda, las lógicas intuicionistas y las categorías cerradas cartesianas (categorías en las que hay productos y espacios de funciones) son lo mismo. Pruebas y tipos que se transcribió a partir de algunos apuntes de conferencias de Girard es una excelente fuente para la parte de la correspondencia entre Curry y Howard. El libro de Steve Awodey y estos notas de Samson Abramsky son buenos lugares para ver esto traducido a un lenguaje categórico. En cuanto a las conexiones con los topos, el libro Sheaves in Geometry and Logic de Mac Lane es muy bueno.
A continuación, probablemente querrá aprender sobre el álgebra categórica y universal. Una de las aplicaciones más inmediatas y accesibles de estas ideas es la teoría de tipos de datos algebraicos (categóricamente: álgebras iniciales para funtores polinómicos) y mapas y pliegues entre ellos. Mónadas también forman parte de este tema ya que son constructores de tipos (endofunctores) que también tienen una multiplicación y una unidad. La notación do de Haskell corresponde a la formación de la categoría Kliesli para una mónada.
El naciente campo de las álgebras universales ha sido muy útil para formalizar las nociones de estado y observación . También hay algunas conexiones emergentes entre álgebra y lógica modal .
Por último, si no estás agotado puedes aprender sobre la dualidad de la piedra, que es una forma de relacionarse " lógica de las propiedades observables " y topología. Para el informático, la dualidad de Stone es principalmente útil para dar una interpretación lógica a la teoría del dominio pero los matemáticos pueden reconocer la dualidad entre los anillos conmutativos y los espectros de Zariski como un caso especial.
