¿Dónde se superpone el álgebra abstracta con la informática?

Me vinieron a la mente dos áreas algo relacionadas: teoría de categorías y teoría de tipos .

Teoría de la categoría , que formaliza las relaciones de las estructuras matemáticas, donde una categoría es básicamente una simple colección de objetos , morfismos (que une dos objetos) y una noción de composición de estos morfismos. La teoría de categorías se ha utilizado para formalizar abstracciones de alto nivel ( conjuntos, anillos, grupos, etc.) y también se puede utilizar como una base axiomática para las matemáticas.

Tiene muchas aplicaciones en la teoría del lenguaje de programación , especialmente en la programación funcional. Por ejemplo, en Haskell [1], las mónadas ( un tipo especial de functor, un mapeo entre categorías) son extremadamente importantes y ampliamente utilizadas, los monoides, functores y otras estructuras algebraicas se usan ampliamente en los fundamentos de los lenguajes funcionales.

La teoría de tipos también es otra área muy importante en la teoría del lenguaje de programación, y también se puede utilizar como una base axiomática para las matemáticas. La teoría de tipos formaliza las relaciones de términos , al dar a cada término un tipo, y las operaciones están restringidas a tipos específicos. Existen relaciones entre algunas áreas específicas de la teoría de tipos y otras áreas de matemática pura, como la relación entre tipos dependientes y funciones homotópicas en la topología algebraica.

Nuevamente, la programación funcional tiene muchos usos para la teoría de tipos. Considere el cálculo de Typed Lambda , que es una teoría de tipos específica, que es muy importante para describir las relaciones en lenguajes de programación fuertemente tipados. Trayendo nuevamente a Haskell, las implementaciones en el Glasgow Haskell Compiler (GHC) usan tipos dependientes, y también tipos de datos algebraicos. También hay un libro completo que explica las relaciones de la teoría de tipos y la programación funcional (Teoría de tipos y programación funcional).

Notas al pie

[1] Haskell / Teoría de la categoría