¿Cuál es la extensión DataKinds de Haskell?

data-kinds

Question

Estoy tratando de encontrar una explicación de la extensión DataKinds que tenga sentido para mí, ya que solo he leído Learn You a Haskell . ¿Hay alguna fuente estándar que tenga sentido para mí con lo poco que he aprendido?

Editar: por ejemplo, la documentation dice

Con -XDataKinds, GHC automáticamente promueve que cada tipo de datos adecuado sea un tipo, y sus (valor) constructores sean constructores de tipo. Los siguientes tipos

y da el ejemplo

data Nat = Ze | Su Nat

dar lugar a los siguientes tipos y tipos de constructores:

Nat :: BOX
Ze :: Nat
Su :: Nat -> Nat

No entiendo el punto. Aunque no entiendo qué significa BOX , las declaraciones Ze :: Nat y Su :: Nat -> Nat parecen indicar lo que normalmente es el caso de que Ze y Su sean constructores de datos normales exactamente como esperarías ver con ghci

Prelude> :t Su
Su :: Nat -> Nat

Answer 1

Aquí está mi opinión:

Considere una longitud indexada Vector de tipo:

data Vec n a where
  Vnil  :: Vec Zero a
  Vcons :: a -> Vec n a -> Vec (Succ n) a

data Zero
data Succ a

Aquí tenemos un Kind Vec :: * -> * -> * . Ya que puedes representar un Vector de Int de longitud cero por:

Vect Zero Int

También puedes declarar tipos sin sentido decir:

Vect Bool Int

Esto significa que podemos tener programación funcional sin tipo en el nivel de tipo. Por lo tanto, nos deshacemos de dicha ambigüedad mediante la introducción de tipos de datos y podemos tener ese tipo:

Vec :: Nat -> * -> *

Así que ahora nuestro Vec obtiene un DataKind llamado Nat que podemos declarar como:

datakind Nat = Zero | Succ Nat

Al introducir un nuevo tipo de datos, nadie puede declarar un tipo sin sentido ya que ahora Vec tiene una firma tipo más restringida.

Answer 2

Bueno, comencemos con los conceptos básicos

Tipos

Tipos son los tipos de tipos *, por ejemplo

Int :: *
Bool :: *
Maybe :: * -> *

Observe que -> está sobrecargado para significar "función" en el nivel amable también. Entonces * es el tipo de tipo Haskell normal.

Podemos pedirle a GHCi que imprima el tipo de algo con :k .

Tipos de datos

¡Ahora esto no es muy útil, ya que no tenemos forma de hacer nuestros propios tipos! Con DataKinds , cuando escribimos

 data Nat = S Nat | Z

GHC promoverá esto para crear el tipo correspondiente Nat y

 S :: Nat -> Nat
 Z :: Nat

Entonces DataKind s hace que el amable sistema sea extensible.

Usos

Hagamos el ejemplo de tipos prototípicos usando GADT

 data Vec :: Nat -> * where
    Nil  :: Vec Z
    Cons :: Int -> Vec n -> Vec (S n)

Ahora vemos que nuestro tipo de Vec está indexado por longitud.

Esa es la descripción básica de 10k pies.

** Esto realmente continúa, Values : Types : Kinds : Sorts ... Algunos idiomas (Coq, Agda ...) admiten esta pila infinita de universos, pero Haskell agrupa todo en un solo género.