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 kind es esencialmente un cálculo lambda simplemente tipado "un nivel arriba", dotado de un tipo primitivo, denotadoy 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, por lo que los tipos no polimórficos son constructores de tipos nulos . Pero todos los constructores nulares, por lo tanto todos los tipos monomórficos, tienen el mismo tipo, el más simple; a saber.
Dado que los operadores de tipo de orden superior son poco comunes en los lenguajes de programación , en la mayoría de la práctica de programación, los tipos se utilizan para distinguir entre los 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]
Ejemplos de
- , pronunciado "tipo", es el tipo de todos los tipos de datos vistos como constructores de tipo nular , y también llamados tipos propios en este contexto. Esto normalmente incluye tipos de funciones en lenguajes de programación funcionales .
- es el tipo de constructor de tipo unario , por ejemplo, de un constructor de tipo lista .
- es el tipo de un constructor de tipo binario (mediante currying ), por ejemplo, de un constructor de tipo par , y también el de un constructor de tipo de función (no confundir con el resultado de su aplicación, que en sí mismo es un tipo de función, por lo tanto de tipo)
- es el tipo de operador de tipo de orden superior desde los constructores de tipo unario hasta los tipos adecuados. [3]
Tipos en Haskell
( Nota : la documentación de Haskell usa la misma flecha para los tipos y tipos de funciones).
El sistema de tipos de Haskell 98 [4] incluye exactamente dos tipos:
- , pronunciado "tipo" es el tipo de todos los tipos de datos .
- es el tipo de constructor de tipo unario , que toma un tipo de tipo y produce un tipo de especie .
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 la imagen 4
es un valor de tipo Int
, mientras que [1, 2, 3]
es un valor de tipo [Int]
(lista de Ints). Por tanto, Int
y [Int]
ten amabilidad, pero también lo hace cualquier tipo de función, por ejemplo Int -> Bool
o incluso Int -> 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 aplicaciones parciales gracias al currying. [5] [6] Así es como Haskell logra tipos paramétricos. Por ejemplo, el tipo []
(lista) es un constructor de tipos: se necesita un solo argumento para especificar el tipo de los elementos de la lista. Por lo tanto, [Int]
(lista de Ints), [Float]
(lista de flotantes) e incluso [[Int]]
(lista de listas de Ints) son aplicaciones válidas del []
constructor de tipos. Por lo tanto, []
es un tipo de especie. Porque Int
tiene amabilidad, aplicándolo []
da como resultado [Int]
, de tipo. El constructor de 2 tuplas(,)
tiene tipo, el constructor de 3 tuplas (,,)
tiene tipo y así.
Amable inferencia
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 | Tenedor ( árbol z ) ( árbol z )
el tipo de z
podría ser cualquier cosa, incluyendo, pero también etc. Haskell de forma predeterminada siempre inferirá los tipos que se , 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
:
type FunnyTree = Árbol [] - no válido
porque la clase de []
,no coincide con el tipo esperado z
, que siempre es.
Sin embargo, se permiten operadores de tipo de orden superior. Por ejemplo:
Aplicación de datos unt z = Z ( unt z )
tiene amabilidad , unt
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.
GHC tiene la extensión PolyKinds
que, junto con KindSignatures
, permite tipos polimórficos. Por ejemplo:
árbol de datos ( z :: k ) = Hoja | Tenedor ( árbol z ) ( árbol z ) tipo Árbol divertido = Árbol [] - OK
Desde GHC 8.0.1, se fusionan tipos y clases. [7]
Ver también
Referencias
- Pierce, Benjamin (2002). Tipos y lenguajes de programación . Prensa del MIT. ISBN 0-262-16209-1., capítulo 29, "Operadores de tipo y tipo"
- ^ "CS 115: polimorfismo paramétrico: funciones de plantilla" . www2.cs.uregina.ca . Consultado el 6 de agosto de 2020 .
- ^ Genéricos de un tipo superior
- ↑ Pierce (2002), capítulo 32
- ^ Tipos - El informe Haskell 98
- ^ "Capítulo 4 Declaraciones y Vinculantes" . Informe de idiomas de Haskell 2010 . Consultado el 23 de julio de 2012 .
- ^ Miran, Lipovača. "¡Aprende Haskell para siempre!" . Elaboración de nuestros propios tipos y clases de tipos . Consultado el 23 de julio de 2012 .
- ^ "9.1. Opciones de idioma - Guía del usuario del compilador de Glasgow Haskell" .