constructor de tipos
En el área de la lógica matemática y la informática conocida como teoría de tipos , un constructor de tipos es una característica de un lenguaje formal tipificado que construye nuevos tipos a partir de los antiguos. Se considera que los tipos básicos se construyen utilizando constructores de tipos nulos . Algunos constructores de tipos toman otro tipo como argumento, por ejemplo, los constructores de tipos de productos, tipos de funciones, tipos de potencia y tipos de listas . Los nuevos tipos se pueden definir mediante la composición recursiva de constructores de tipos.
Por ejemplo, el cálculo lambda simplemente tipeado puede verse como un lenguaje con un solo constructor de tipo: el constructor de tipo de función. Los tipos de productos generalmente se pueden considerar "incorporados" en los cálculos lambda tipificados a través de curry .
En resumen, un constructor de tipo es un operador de tipo n -ario que toma como argumento cero o más tipos y devuelve otro tipo. Haciendo uso de curry, los operadores de tipo n -ario se pueden (re)escribir como una secuencia de aplicaciones de operadores de tipo unario. Por lo tanto, podemos ver los operadores de tipo como un cálculo lambda simplemente tipificado, que tiene solo un tipo básico, generalmente denotado y pronunciado "tipo", que es el tipo de todos los tipos en el lenguaje subyacente, que ahora se denominan tipos propios en para distinguirlos de los tipos de los operadores de tipo en su propio cálculo, que se denominan tipos .
Los operadores de tipo pueden vincular variables de tipo. Por ejemplo, dar la estructura del cálculo λ de tipo simple en el nivel de tipo requiere operadores de tipo vinculantes o de orden superior. Estos operadores de tipo vinculante corresponden al segundo eje del cubo λ y teorías de tipo como el cálculo λ de tipo simple con operadores de tipo, λ ω . La combinación de operadores de tipos con el cálculo λ polimórfico ( Sistema F ) produce el Sistema F ω .