En el área de la lógica matemática y la informática conocida como teoría de tipos , un tipo es el tipo de un constructor de tipos o, con menos frecuencia, el tipo de un operador de tipos de orden superior . Un sistema de tipos es esencialmente un cálculo lambda tipado de forma simple "un nivel superior", dotado de un tipo primitivo, denotado y llamado "tipo", que es el tipo de cualquier tipo de datos que no necesita ningún parámetro de tipo .
A veces se describe de manera confusa un tipo como el "tipo de un tipo (de datos) ", pero en realidad es más bien un especificador de aridad . Sintácticamente, es natural considerar que los tipos polimórficos son constructores de tipos, y por lo tanto, los tipos no polimórficos son constructores de tipos nulos . Pero todos los constructores nulos, y por lo tanto todos los tipos monomórficos, tienen el mismo tipo, el más simple; es decir , .
Dado que los operadores de tipos de orden superior son poco comunes en los lenguajes de programación , en la mayoría de las prácticas de programación, los tipos se utilizan para distinguir entre los tipos de datos y los tipos de constructores que se utilizan para implementar el polimorfismo paramétrico . Los tipos aparecen, ya sea de forma explícita o implícita, en lenguajes cuyos sistemas de tipos tienen en cuenta el polimorfismo paramétrico de una manera accesible mediante programación, como C++ , [1] Haskell y Scala . [2]
( Nota : la documentación de Haskell utiliza la misma flecha para ambos tipos y clases de funciones).
El sistema de tipos de Haskell 98 [4] incluye exactamente dos tipos:
Un tipo habitado (como se denomina a los tipos propios en Haskell) es un tipo que tiene valores. Por ejemplo, ignorando las clases de tipos que complican el panorama, 4es un valor de tipo Int, mientras que [1, 2, 3]es un valor de tipo [Int](lista de enteros). Por lo tanto, Inty [Int]tienen tipo , pero también lo tienen cualquier tipo de función, por ejemplo o incluso .Int -> BoolInt -> Int -> Bool
Un constructor de tipo toma uno o más argumentos de tipo y produce un tipo de datos cuando se suministran suficientes argumentos, es decir, admite la aplicación parcial gracias a la currificación. [5] [6] Así es como Haskell logra tipos paramétricos. Por ejemplo, el tipo [](lista) es un constructor de tipo: toma un solo argumento para especificar el tipo de los elementos de la lista. Por lo tanto, [Int](lista de Ints), [Float](lista de Floats) e incluso [[Int]](lista de listas de Ints) son aplicaciones válidas del []constructor de tipo. Por lo tanto, []es un tipo de kind . Debido a que tiene kind , aplicarlo da como resultado , de kind . El constructor de 2- tuplas tiene kind , el constructor de 3-tuplas tiene kind y así sucesivamente.Int[][Int](,)(,,)
El estándar Haskell no permite tipos polimórficos, a diferencia del polimorfismo paramétrico en tipos, que sí es compatible con Haskell. Por ejemplo, en el siguiente ejemplo:
datos Árbol z = Hoja | Horquilla ( Árbol z ) ( Árbol z ) El tipo de zpodría ser cualquier cosa, incluyendo , pero también etc. Haskell por defecto siempre inferirá que los tipos son , a menos que el tipo indique explícitamente lo contrario (ver abajo). Por lo tanto, el verificador de tipos rechazará el siguiente uso de :Tree
tipo FunnyTree = Tree [] -- inválido porque el tipo de [], no coincide con el tipo esperado para , que siempre es .z
Sin embargo, se permiten operadores de orden superior. Por ejemplo:
datos Aplicación unt z = Z ( unt z ) tiene tipo , es decir, se espera que sea un constructor de datos unario, que se aplica a su argumento, que debe ser un tipo, y devuelve otro tipo.unt
GHC tiene la extensión PolyKinds, que, junto con KindSignatures, permite clases polimórficas. Por ejemplo:
datos Árbol ( z :: k ) = Hoja | Bifurcación ( Árbol z ) ( Árbol z ) tipo FunnyTree = Árbol [] -- OK Desde GHC 8.0.1, los tipos y clases se fusionan. [7]