que - ¿Cuál es exactamente el tipo "*" en Haskell?

hola mundo en haskell (3)

En Haskell, las expresiones (de nivel de valor) se clasifican en tipos , que se pueden anotar con :: like so: 3 :: Int , "Hello" :: String , (+ 1) :: Num a => a -> a . Del mismo modo, los tipos se clasifican en tipos . En GHCi, puede inspeccionar el tipo de expresión de un tipo usando el comando :kind o :k :

> :k Int Int :: * > :k Maybe Maybe :: * -> * > :k Either Either :: * -> * -> * > :k Num Num :: * -> Constraint > :k Monad Monad :: (* -> *) -> Constraint

Hay definiciones que flotan alrededor de que * es el tipo de "tipos concretos" o "valores" o "valores de tiempo de ejecución". Ver, por ejemplo, Learn You A Haskell . ¿Qué tan cierto es eso? Hemos tenido algunas questions sobre los tipos que abordan el tema de paso, pero sería bueno tener una explicación canónica y precisa de * .

¿Qué significa exactamente * ? ¿Y cómo se relaciona con otros tipos más complejos?

Además, ¿las DataKinds o PolyKinds cambian la respuesta?

En la forma más básica del lenguaje amable, donde solo hay el tipo * y el constructor amable -> , entonces * es el tipo de cosas que pueden estar en una relación de tipo a los valores; nada con un tipo diferente puede ser un tipo de valores.

Existen tipos para clasificar valores. Todos los valores con el mismo tipo son intercambiables para la verificación de tipo, por lo que al verificador de tipos solo le deben importar los tipos, no los valores específicos. Entonces tenemos el "nivel de valor" donde viven todos los valores reales, y el "nivel de tipo" donde viven sus tipos. La relación "tipo de" forma enlaces entre los dos niveles, siendo un tipo único el tipo de (generalmente) muchos valores. Haskell hace que estos dos niveles sean bastante explícitos; es por eso que puedes tener declaraciones como data Foo = Foo Int Chat Bool donde has declarado una cosa de nivel de tipo Foo (un tipo con tipo * ) y una cosa de nivel de valor Foo (un constructor con tipo Int -> Char -> Bool -> Foo ). Los dos Foo implicados simplemente se refieren a diferentes entidades en diferentes niveles, y Haskell los separa tan completamente que siempre puede decir a qué nivel se está refiriendo y así puede permitir (a veces de manera confusa) que las cosas en los diferentes niveles tengan el mismo nombre .

Pero tan pronto como introduzcamos tipos que tienen estructura propia (como Maybe Int , que es un constructor de tipo Maybe aplicado a un tipo Int ), entonces tenemos cosas que existen en el nivel de tipo que en realidad no están en una relación de tipo de relación a cualquier valor. No hay valores cuyo tipo sea solo Maybe , solo valores con el tipo Maybe Int (y Maybe Bool , Maybe () , incluso Maybe Void , etc.). Entonces, debemos clasificar nuestras cosas de nivel de tipo por la misma razón por la que necesitamos clasificar nuestros valores; solo ciertas expresiones de tipo representan realmente algo que puede ser el tipo de valores, pero muchas de ellas funcionan indistintamente con el propósito de "verificar la clase" (si es un tipo correcto para el nivel de valor, se ha declarado que es el tipo de es un problema para un nivel diferente). ¹

Entonces * (que a menudo se dice que se pronuncia "tipo") es el tipo básico; es el tipo de cosas a nivel de tipo que se puede decir que son el tipo de valores. Int tiene valores; por lo tanto, su tipo es * . Maybe no tenga valores, pero toma un argumento y produce un tipo que tiene valores; esto nos hace un tipo como ___ -> * . Podemos completar el espacio en blanco al observar que el argumento de Maybe se usa como el tipo del valor que aparece en Just a , por lo que su argumento también debe ser un tipo de valores (con kind * ), y así Maybe debe tener kind * -> * . Y así.

Cuando se trata de tipos que solo involucran estrellas y flechas, entonces solo las expresiones de tipo tipo * son tipos de valores. Cualquier otro tipo (por ejemplo, * -> (* -> * -> *) -> (* -> *) ) solo contiene otras "entidades de nivel de tipo" que no son tipos reales que contienen valores.

PolyKinds , como yo lo entiendo, realmente no cambia esta imagen en absoluto. Simplemente le permite hacer declaraciones polimórficas en el nivel de clase, lo que significa que agrega variables a nuestro lenguaje amable (además de las estrellas y flechas). Entonces ahora puedo contemplar cosas de tipo tipo k -> * ; esto podría ser instanciado para que funcione como kind * -> * o (* -> *) -> * o (* -> (* -> *)) -> * . Hemos obtenido exactamente el mismo tipo de poder que tener (a -> b) -> [a] -> [b] en el nivel de tipo que nos ha ganado; podemos escribir una función de map con un tipo que contenga variables, en lugar de tener que escribir cada función de mapa posible por separado. Pero todavía hay un solo tipo que contiene cosas de tipo de tipo que son los tipos de valores: * .

DataKinds también introduce cosas nuevas al lenguaje amable. Efectivamente, lo que hace es permitirnos declarar nuevos tipos arbitrarios, que contienen nuevas entidades de nivel de tipo (al igual que las declaraciones de data ordinarios nos permiten declarar nuevos tipos arbitrarios, que contienen nuevas entidades de nivel de valor). Pero no nos permite declarar cosas con una correspondencia de entidades en los 3 niveles; si tengo data Nat :: Z | S Nat data Nat :: Z | S Nat y usa DataKinds para DataKinds al nivel bueno, entonces tenemos dos cosas diferentes llamadas Nat que existen en el nivel de tipo (como el tipo de nivel de valor Z , SZ , S (SZ) , etc.), y en el nivel amable (como el tipo de nivel de tipo Z , SZ , S (SZ) ). Sin embargo, el nivel de tipo Z no es el tipo de ningún valor; el valor Z habita en el nivel de tipo Nat (que a su vez es de tipo * ), no en el tipo de nivel Z Así que DataKinds agrega nuevas cosas definidas por el usuario al lenguaje amable, que puede ser el tipo de nuevas cosas definidas por el usuario en el nivel de tipo, pero sigue siendo el caso que las únicas cosas de nivel de tipo que pueden ser los tipos de valores son de tipo * .

La única adición al lenguaje amable del que soy consciente y que realmente cambia esto son los tipos mencionados en la respuesta de @ ChristianConkle, como # (¿creo que hay un par más ahora? No estoy realmente bien informado " bajo nivel "tipos como ByteArray# ). Estos son los tipos de tipos que tienen valores que GHC necesita saber para tratarlos de manera diferente (como no suponer que se pueden clasificar y evaluar de forma perezosa), incluso cuando se trata de funciones polimórficas, por lo que no podemos adjuntar el conocimiento que necesitan. ser tratado de manera diferente a los tipos de estos valores, o se perdería al invocar funciones polimórficas sobre ellos.

¹ La palabra "tipo" puede ser un poco confusa. A veces se usa para referirse a cosas que realmente se encuentran en una relación de tipo a las cosas en el nivel de valor (esta es la interpretación que se usa cuando la gente dice " Maybe no es un tipo, es un constructor de tipos"). Y a veces se usa para referirse a cualquier cosa que exista en el nivel de tipo (bajo esta interpretación Maybe sea de hecho un tipo). En esta publicación intento referirme muy explícitamente a "cosas de tipo de letra" en lugar de usar "tipo" como una abreviatura.

Para los principiantes que están tratando de aprender sobre los tipos (puede pensar que son del tipo de un tipo), recomiendo este capítulo del libro Aprenda un libro de Haskell .

Personalmente pienso en tipos de esta manera:

Tiene tipos concretos, por ejemplo, Int , Bool , String , [Int] , Maybe Int o Either Int String .

Todos estos tienen el tipo * . ¿Por qué? Porque no pueden tomar más tipos como parámetro; un Int , es un Int ; a Maybe Int es un Maybe Int . ¿Qué pasa con Maybe o [] o con Either ?

Cuando dices Maybe , no tienes un tipo concreto porque no especificaste su parámetro. Maybe Int o Maybe String son diferentes, pero ambos tienen un * tipo, pero Maybe está esperando que un tipo de tipo * devuelva un tipo * . Para aclarar, veamos qué comando GHCI :kind puede decirnos:

Prelude> :kind Maybe Int Maybe Int :: * Prelude> :kind Maybe Maybe :: * -> *

Con listas, es lo mismo:

Prelude> :k [String] [String] :: * Prelude> :k [] [] :: * -> *

¿Qué pasa con Either ?

Prelude> :k Either Int String Either Int String :: * Prelude> :k Either Int Either Int :: * -> *

Podría pensar intuitivamente en Either como una función que toma parámetros, pero los parámetros son tipos :

Prelude> :k Either Int Either Int :: * -> *

significa que Either Int está esperando un parámetro de tipo.

Primero, * no es un comodín! También es típicamente pronunciado como "estrella".

Nota de sangrado : a partir de febrero de 2015, una propuesta para simplificar el sistema de subgéneros de GHC (en 7.12 o posterior) . Esa página contiene una buena discusión de la historia de GHC 7.8 / 7.10. De cara al futuro, GHC puede eliminar la distinción entre tipos y tipos, con * :: * . Ver Weirich, Hsu y Eisenberg, System FC con igualdad explícita .

El estándar: una descripción de las expresiones de tipo.

El informe Haskell 98 define * en este contexto como :

El símbolo * representa el tipo de todos los constructores de tipo nullary.

En este contexto, "nullary" simplemente significa que el constructor no toma parámetros. Either es binario; se puede aplicar a dos parámetros: Either ab . Maybe es único; se puede aplicar a un parámetro: Maybe a . Int es nulo; se puede aplicar a ningún parámetro.

Esta definición es un poco incompleta por sí misma. Una expresión que contiene un constructor de tipo unario, binario, etc. totalmente aplicado también tiene kind * , por ejemplo, Maybe Int :: * .

En GHC: algo que contiene valores?

Si examinamos la documentación de GHC, obtenemos algo más cerca de la definición de "puede contener un valor de tiempo de ejecución". La página de Comentarios de GHC "Tipos" indica que "'' * '' es el tipo de valores encuadrados. Cosas como Int y Maybe Float tienen kind * ." La guía de usuario de GHC para la versión 7.4.1 , por otro lado, indicó que * es el tipo de "tipos levantados". (Ese pasaje no se retuvo cuando se revisó la sección para PolyKinds .)

Los valores en caja y los tipos levantados son un poco diferentes. De acuerdo con la página de Comentarios de GHC "TypeType" ,

Un tipo se desempaqueta si su representación es distinta de un puntero. Los tipos no compartidos tampoco se han eliminado.
Un tipo se levanta si tiene fondo como elemento. Los cierres siempre tienen tipos levantados: es decir, cualquier identificador ligado a let en Core debe tener un tipo levantado. Operacionalmente, un objeto levantado es uno que se puede ingresar. Solo los tipos elevados pueden unificarse con una variable de tipo.

Así que ByteArray# , el tipo de bloques de memoria sin formato , está encuadrado porque se representa como un puntero, pero no se ha alzado porque el fondo no es un elemento.

> undefined :: ByteArray# Error: Kind incompatibility when matching types: a0 :: * ByteArray# :: #

Por lo tanto, parece que la antigua definición de la Guía del usuario es más precisa que la del Comentario de GHC: * es el tipo de tipos levantados . (Y, a la inversa, # es el tipo de tipos no actualizados ).

Tenga en cuenta que si los tipos de tipo * siempre se eliminan, para cualquier tipo t :: * puede construir un "valor" de clases con undefined :: t o algún otro mecanismo para crear bottom. Por lo tanto, incluso los tipos "lógicamente deshabitados" como Void pueden tener un valor, es decir, inferior.

Por lo tanto, parece que sí, * representa el tipo de tipos que pueden contener valores de tiempo de ejecución, si undefined está undefined es su idea de un valor de tiempo de ejecución. (Lo cual no es una idea totalmente loca, no creo)

Extensiones de GHC?

Hay varias extensiones que animan un poco el sistema tipo. Algunos de estos son mundanos: KindSignatures nos permite escribir anotaciones amables , como escribir anotaciones.

ConstraintKinds agrega el tipo Constraint , que es, aproximadamente, el tipo del lado izquierdo de => .

DataKinds nos permite introducir nuevos tipos además de * y # , del mismo modo que podemos introducir nuevos tipos con data , type y type .

Con DataKinds cada declaración de data (pueden aplicarse términos y condiciones) genera una declaración tipo promocionada. Asi que

data Bool = True | False

introduce el constructor de valor habitual y el nombre de tipo; Además, produce un nuevo tipo , Bool , y dos tipos: True :: Bool y False :: Bool .

PolyKinds introduce variables amables . Esta es solo una manera de decir "para cualquier tipo k " tal como decimos "para cualquier tipo t " en el nivel de tipo. En cuanto a nuestro amigo * y si todavía significa "tipos con valores", supongo que podría decirse un tipo t :: k donde k es una variable tipo podría contener valores, si k ~ * o k ~ # .