En el área de la lógica matemática y la informática conocida como teoría de tipos , una clase es el tipo de un constructor de tipos o, menos comúnmente, el tipo de un operador de tipos de orden superior . Un sistema de tipo es esencialmente un cálculo lambda escrito simplemente "un nivel arriba", 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 .
Un tipo a veces se describe de manera confusa como el "tipo de un tipo (de datos) ", pero en realidad es más un especificador de aridad . Sintácticamente, es natural considerar los tipos polimórficos como constructores de tipos y, por tanto, los tipos no polimórficos como constructores de tipos nulos . Pero todos los constructores nulares, y por 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 parte de la práctica de programación, los tipos se utilizan para distinguir entre tipos de datos y los tipos de constructores que se utilizan para implementar polimorfismo paramétrico . Los tipos aparecen, ya sea explícita o implícitamente, en lenguajes cuyos sistemas de tipos dan cuenta del polimorfismo paramétrico de una manera programáticamente accesible, como C++ , [1] Haskell y Scala . [2]
( Nota : la documentación de Haskell utiliza la misma flecha tanto para los tipos como para los tipos de funciones).
El sistema de tipos de Haskell 98 [4] incluye exactamente dos tipos:
Un tipo habitado (como se llama a los tipos propios en Haskell) es un tipo que tiene valores. Por ejemplo, ignorar 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 Ints). Por lo tanto, Inty [Int]tiene tipo , pero también lo tiene cualquier tipo de función, por ejemplo o incluso .Int -> BoolInt -> Int -> Bool
Un constructor de tipos toma uno o más argumentos de tipo y produce un tipo de datos cuando se proporcionan suficientes argumentos, es decir, admite una aplicación parcial gracias al curry. [5] [6] Así es como Haskell logra tipos paramétricos. Por ejemplo, el tipo [](lista) es un constructor de tipos: se necesita un único 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 tipos. Por tanto, []es un tipo de especie . Porque tiene clase , al aplicarle resulta en , de clase . El constructor de 2 tuplas tiene kind , el constructor de 3 tuplas tiene kind y así sucesivamente.Int[][Int](,)(,,)
Haskell estándar no permite tipos polimórficos. Esto contrasta con el polimorfismo paramétrico en tipos, que es compatible con Haskell. Por ejemplo, en el siguiente ejemplo:
árbol de datos z = Hoja | Horquilla ( Árbol z ) ( Árbol z ) el tipo de zpodría ser cualquier cosa, incluido , pero también etc. Haskell, por defecto, siempre inferirá que los tipos son , a menos que el tipo indique explícitamente lo contrario (ver más abajo). Por lo tanto, el verificador de tipos rechazará el siguiente uso de :Tree
escriba FunnyTree = Árbol [] - no válido porque el tipo de [], no coincide con el tipo esperado , que siempre es .z
Sin embargo, se permiten operadores de tipo de orden superior. Por ejemplo:
aplicación de datos unt z = Z ( unt z ) tiene kind , 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 tipos polimórficos. Por ejemplo:
árbol de datos ( z :: k ) = Hoja | Tipo de bifurcación ( árbol z ) ( árbol z ) FunnyTree = árbol [] - OK Desde GHC 8.0.1, los tipos y clases están fusionados. [7]