Constructor de tipo

En el ámbito de la lógica matemática y la informática conocido como teoría de tipos , un constructor de tipos es una característica de un lenguaje formal tipado que crea nuevos tipos a partir de otros ya existentes. Se considera que los tipos básicos se construyen mediante constructores de tipos nulos . Algunos constructores de tipos aceptan otro tipo como argumento, por ejemplo, los constructores para tipos producto , tipos función , tipos potencia y tipos lista . Se pueden definir nuevos tipos mediante la composición recursiva de constructores de tipos.

Por ejemplo, el cálculo lambda tipado simple puede verse como un lenguaje con un único constructor de tipo no básico : el constructor de tipo función. Los tipos producto generalmente pueden considerarse "integrados" en los cálculos lambda tipados mediante currificación .

Abstractamente, un constructor de tipos es un operador de tipo n -ario que toma como argumento cero o más tipos y devuelve otro tipo. Haciendo uso de currificación, los operadores de tipo n -arios pueden (re)escribirse como una secuencia de aplicaciones de operadores de tipo unarios. Por lo tanto, podemos ver los operadores de tipo como un cálculo lambda simplemente tipado, que tiene solo un tipo básico, generalmente denotado${\displaystyle *}$y se pronuncia "type", que es el tipo de todos los tipos en el lenguaje subyacente, que ahora se denominan tipos propios para distinguirlos de los tipos de los operadores de tipo en su propio cálculo, que se denominan clases .

Los operadores de tipo pueden vincular variables de tipo. Por ejemplo, dar la estructura del cálculo λ simplemente tipado a nivel de tipo requiere operadores de tipo de enlace, o de orden superior. Estos operadores de tipo de enlace corresponden al segundo eje del cubo λ , y las teorías de tipos como el cálculo λ simplemente tipado con operadores de tipo, λ _ω . La combinación de operadores de tipo con el cálculo λ polimórfico ( Sistema F ) produce el Sistema F _ω .

Algunos lenguajes de programación funcional hacen un uso explícito de constructores de tipos. Un ejemplo notable es Haskell , en el que todas datalas declaraciones de tipo se consideran declaraciones de constructores de tipos, y los tipos básicos (o constructores de tipos nulos) se denominan constantes de tipo. ^{[ 1 ] [ 2 ]} Los constructores de tipos también pueden considerarse como tipos de datos polimórficos paramétricos .

• Tipo (teoría de tipos)
• Tipo de datos algebraicos
• Tipo de datos recursivo