HaskellのDataKinds拡張とは？

質問

私はDataKindsエクステンションの説明を探しています。 あなたにハスケルを学ぶ . 私が学んだことを少しでも理解できるような標準的なソースはありますか？

編集：たとえば ドキュメント にはこうあります。

XDataKindsを使うと、GHCは自動的にすべての適切なデータ型をkindに昇格させます。 を種類に、そしてその(値の)コンストラクタを型コンストラクタに自動的に昇格させます。 以下の型は

と例示しています。

data Nat = Ze | Su Nat

は、以下のような種類と型構成子を生じます。

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

要領を得ない。何が言いたいのかわからないが BOX の意味は理解できないが、ステートメント Ze :: Nat と Su :: Nat -> Nat は、Ze と Su が ghci で期待されるような通常のデータコンストラクタであるという、すでに通常であることを述べているように見えます。

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

どのように解決するのですか？

まずは基本的なところから

種類

種類とは、種類*の種類であり、例えば

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

注目すべきは -> は種類レベルでも "function" を意味するようにオーバーロードされていることに注意してください。つまり * は通常のHaskellの型の種類です。

で何かの種類を表示するようにGHCiに依頼することができます。 :k .

データの種類

独自の種類を作る方法がないので、これはあまり役に立ちません! とはいえ DataKinds と書くと

 data Nat = S Nat | Z

GHCはこれを昇格させて、対応する種類の Nat とします。

 Prelude> :k S
 S :: Nat -> Nat
 Prelude> :k Z
 Z :: Nat

そこで DataKind を使うことで、親切なシステムが拡張可能になります。

用途

GADTを使った典型的な種類の例を見てみましょう。

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

ここで、私たちの Vec 型は長さによってインデックス化されていることがわかります。

これが基本的な、10kフィートの概要です。

これは実際に続いています。 Values : Types : Kinds : Sorts ... いくつかの言語（Coq、Agda ...）はこの宇宙の無限スタックをサポートしていますが、Haskellはすべてを1つのソートにひとまとめにしています。