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
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
.
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.
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.