74

Learn You a Haskellを読んだだけで理解できる DataKinds 拡張機能の説明を見つけようとしています。私が少し学んだことで意味をなす標準的なソースはありますか?

編集：たとえば、ドキュメントには

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

そして例を挙げます

data Nat = Ze | Su Nat

次の種類と型コンストラクターを生成します。

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

要点がわかりません。BOXどういう意味かはわかりませんが、ステートメントZe :: NatとステートメントSu :: Nat -> Natは、ghci で期待されるのとまったく同じように、Ze と Su が通常のデータ コンストラクターであるという通常のケースを述べているようです。

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

2 に答える 2

72

さて、基本から始めましょう

種類

Kinds は type* の型です。たとえば、

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

->は、種類レベルでも「関数」を意味するようにオーバーロードされていることに注意してください。*通常の Haskell 型も同様です。

GHCi に で何かの種類を出力するように依頼できます:k。

データの種類

独自の種類を作成する方法がないため、これはあまり役に立ちません。でDataKinds、私たちが書くとき

 data Nat = S Nat | Z

GHCはこれを促進して、対応する種類を作成しNat、

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

したがってDataKind、s はカインド システムを拡張可能にします。

用途

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 つの種類にまとめています。

于 2013-12-13T03:45:27.173 に答える
52

これが私の見解です：

次のタイプの長さのインデックス付きベクターを考えてみましょう。

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

data Zero
data Succ a

ここに Kind がありVec :: * -> * -> *ます。Int の長さゼロのベクトルを次のように表すことができるため:

Vect Zero Int

無意味な型を宣言することもできます：

Vect Bool Int

これは、型レベルで型付けされていない関数型プログラミングを行うことができることを意味します。したがって、データの種類を導入することでそのようなあいまいさを取り除き、そのような種類を持つことができます。

Vec :: Nat -> * -> *

これで、次のように宣言できるVec名前の DataKind を取得します。Nat

datakind Nat = Zero | Succ Nat

新しいデータの種類を導入することでVec、より制約された種類のシグネチャを持つようになったため、意味のない型を宣言することはできなくなりました。

于 2014-05-19T18:52:27.103 に答える