El más obvio relación a la categoría de la teoría es que tenemos una categoría que consta de los tipos de objetos y funciones como flechas. Hemos identidad de funciones y se puede componer funciones con la habitual axiomas holding (con varias salvedades). Eso es sólo el punto de partida.
Un lugar en el que empieza a ser más profundo es cuando se consideran funciones polimórficas. Un polimórficos función es esencialmente una familia de funciones, parametrizarse por tipos. O categóricamente, una familia de flechas, parametrizarse a través de los objetos. Esto es similar a lo que una transformación natural. Mediante la introducción de algunas restricciones razonables nos encontramos con que una gran clase de funciones polimórficas son, de hecho, natural de transformaciones y mucha de la categoría de la teoría se aplica ahora. El estándar de ejemplos para dar aquí son libres de teoremas.
Categoría de la teoría también mallas muy bien con la noción de un "interfaz" en la programación. Categoría de la teoría nos anima a no mirar lo que un objeto está hecho, pero cómo interactúa con otros objetos, y en sí mismo. Mediante la separación de una interfaz de una aplicación de un programador no necesita saber nada acerca de la implementación. De manera similar categoría anima a pensar acerca de los objetos hasta el isomorfismo - no es precisamente lo que diferencia a nuestros grupos están hechos, sólo importa lo que las operaciones en nuestros grupos. Categoría de la teoría capta con precisión este concepto de interfaz.
También hay una hermosa relación entre la pura escribió cálculo lambda y cartesiana categorías cerradas. Cualquier expresión en el cálculo puede ser interpretado como la composición de las funciones estándar que vienen con un CCC: como la proyección sobre los factores de un producto, o la función de evaluación. Así, las expresiones lambda puede ser interpretado como aplicable a cualquier CCC. En otras palabras, el cálculo lambda es un lenguaje interno para los Ccc. Esto es explicado en Lambek y Scott. Esto significa que la teoría de la Ccc está profundamente incrustado en Haskell, es decir, debido a Haskell es esencialmente pura escribió cálculo lambda con un montón de extensiones.
Otro ejemplo es la manera estructuralmente recursing sobre recursiva tipos de datos pueden ser muy bien descrito en términos de la inicial de los objetos en categorías de F-álgebras. Usted puede encontrar algunos de los detalles aquí.
Y un último ejemplo: dualising (en el sentido categórico) definiciones resulta ser muy útil en los lenguajes de programación mundo. Por ejemplo, en el párrafo anterior mencioné estructurales de la recursividad. Dualising esto le da a las nociones de F-coalgebras y vigilado recursividad y conduce a una bonita manera de trabajar con infinita',' tipos de datos tales como arroyos. Trabajar con secuencias es complicado, porque ¿cómo se puede proteger contra inadvertidamente tratando de recorrer toda la longitud de una secuencia causando un bucle infinito? La adecuada doble de recursividad estructural conduce a una poderosa manera de lidiar con los arroyos que está garantizado para ser portado bien. Bart Jacobs, por ejemplo, tiene muchos buenos trabajos en esta área.
