Quelle est l’extension DataKinds de Haskell?

J’essaie de trouver une explication de l’extension DataKinds qui me sera utile en ayant seulement lu Learn You a Haskell . Y a-t-il une source standard qui aura du sens pour moi avec le peu que j’ai appris?

Edit: Par exemple la documentation dit

Avec -XDataKinds, GHC promeut automatiquement chaque type de données approprié pour qu’il soit un type, et ses constructeurs (de valeur) soient des constructeurs de types. Les types suivants

et donne l’exemple

data Nat = Ze | Su Nat 

donner les types et les types de constructeurs suivants:

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

Je ne comprends pas le point. Bien que je ne comprenne pas ce que BOX veut dire, les instructions Ze :: Nat et Su :: Nat -> Nat semblent indiquer ce qui est déjà normalement le cas, Ze et Su sont des constructeurs de données normaux exactement comme on peut s’y attendre avec ghci.

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

Eh bien, commençons par les bases

Genre

Les types sont les types de types *, par exemple

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

Notez que -> est surchargé pour signifier “fonction” au même niveau. So * est le genre d’un type Haskell normal.

Nous pouvons demander à GHCi d’imprimer le type de quelque chose avec :k .

Types de données

Maintenant ce n’est pas très utile, car nous n’avons aucun moyen de faire nos propres genres! Avec DataKinds , quand on écrit

  data Nat = S Nat | Z 

GHC va promouvoir cela pour créer le genre correspondant Nat et

  S :: Nat -> Nat Z :: Nat 

Ainsi, DataKind rend le type de système extensible.

Les usages

Faisons l’exemple des types prototypiques en utilisant les GADT

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

Nous voyons maintenant que notre type Vec est indexé par longueur.

C’est la base, vue d’ensemble de 10k pieds.

** En fait, cela continue, Values : Types : Kinds : Sorts ... Certains langages (Coq, Agda ..) supportent cette stack infinie d’univers, mais Haskell regroupe tout dans un seul type.

Voici ma prise:

Considérons une longueur indexée Vecteur de type:

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

Ici, nous avons un Kind Vec :: * -> * -> * . Puisque vous pouvez représenter un vecteur de longueur zéro de Int par:

 Vect Zero Int 

Vous pouvez également déclarer des types sans signification dire:

 Vect Bool Int 

Cela signifie que nous pouvons avoir une functional programming non typée au niveau du type. On se débarrasse donc de cette ambiguïté en introduisant des types de données et peut avoir un tel type:

 Vec :: Nat -> * -> * 

Alors maintenant, notre Vec obtient un DataKind nommé Nat que nous pouvons déclarer comme:

 datakind Nat = Zero | Succ Nat 

En introduisant un nouveau type de données, personne ne peut déclarer un type sans signification puisque Vec maintenant une signature de type plus contraignant.