Un cálculo lambda tipado es un formalismo tipado que utiliza el símbolo lambda ( ) para denotar la abstracción de una función anónima. En este contexto, los tipos son normalmente objetos de naturaleza sintáctica que se asignan a términos lambda; la naturaleza exacta de un tipo depende del cálculo considerado (ver tipos a continuación). Desde cierto punto de vista, los cálculos lambda tipados pueden verse como refinamientos del cálculo lambda no tipado , pero desde otro punto de vista, también pueden considerarse la teoría más fundamental y el cálculo lambda no tipado un caso especial con un solo tipo. [1]
Los cálculos lambda tipados son lenguajes de programación fundamentales y son la base de los lenguajes de programación funcional tipados como ML y Haskell y, de forma más indirecta, de los lenguajes de programación imperativos tipados . Los cálculos lambda tipados desempeñan un papel importante en el diseño de sistemas de tipos para lenguajes de programación; aquí, la tipabilidad suele capturar propiedades deseables del programa (por ejemplo, el programa no provocará una violación de acceso a la memoria).
Los cálculos lambda tipados están estrechamente relacionados con la lógica matemática y la teoría de la demostración a través del isomorfismo de Curry-Howard y pueden considerarse como el lenguaje interno de ciertas clases de categorías . Por ejemplo, el cálculo lambda tipado de manera simple es el lenguaje de las categorías cartesianas cerradas (CCC) [2]
Se han estudiado varios cálculos lambda tipados. El cálculo lambda de tipo simple tiene un solo constructor de tipos , la flecha , y sus únicos tipos son los tipos básicos y los tipos de función . El Sistema T extiende el cálculo lambda de tipo simple con un tipo de números naturales y recursión primitiva de orden superior ; en este sistema todas las funciones demostrablemente recursivas en la aritmética de Peano son definibles. El Sistema F permite el polimorfismo al usar cuantificación universal sobre todos los tipos; desde una perspectiva lógica puede describir todas las funciones que son demostrablemente totales en lógica de segundo orden . Los cálculos lambda con tipos dependientes son la base de la teoría de tipos intuicionista , el cálculo de construcciones y el marco lógico (LF), un cálculo lambda puro con tipos dependientes. Basado en el trabajo de Berardi sobre sistemas de tipos puros , Henk Barendregt propuso el cubo Lambda para sistematizar las relaciones de los cálculos lambda de tipo puro (incluyendo el cálculo lambda de tipo simple, el Sistema F, LF y el cálculo de construcciones). [3]
Algunos cálculos lambda tipados introducen una noción de subtipificación , es decir, si es un subtipo de , entonces todos los términos del tipo también tienen tipo . Los cálculos lambda tipados con subtipificación son los cálculos lambda tipados simplemente con tipos conjuntivos y Sistema F <: .
Todos los sistemas mencionados hasta ahora, con excepción del cálculo lambda no tipado, son fuertemente normalizadores : todos los cálculos terminan. Por lo tanto, no pueden describir todas las funciones computables por Turing . [4] Como otra consecuencia, son consistentes como una lógica, es decir, hay tipos no habitados. Sin embargo, existen cálculos lambda tipados que no son fuertemente normalizadores. Por ejemplo, el cálculo lambda de tipo dependiente con un tipo de todos los tipos (Tipo:Tipo) no es normalizador debido a la paradoja de Girard . Este sistema es también el sistema de tipo puro más simple, un formalismo que generaliza el cubo Lambda. Los sistemas con combinadores de recursión explícitos, como el " lenguaje de programación para funciones computables " (PCF) de Plotkin , no son normalizadores, pero no están destinados a ser interpretados como una lógica. De hecho, PCF es un lenguaje de programación funcional tipado prototípico, donde los tipos se utilizan para garantizar que los programas se comporten bien, pero no necesariamente que terminen.
En programación informática , las rutinas (funciones, procedimientos, métodos) de los lenguajes de programación fuertemente tipados corresponden estrechamente a las expresiones lambda tipadas. [5]
