4

以下のコードの * -> * 部分を説明したり、リンクを提供したりできますか?

data BinaryTree t :: * -> * where
   Leaf :: BinaryTree Empty a
   Branch :: a -> BinaryTree isempty a -> BinaryTree isempty' a -> BinaryTree NonEmpty a

どうもありがとう。

4

3 に答える 3

5

親切な署名。これらは、型コンストラクターのアリティを明示的に定義するために使用できます。は*「任意の型」を意味し、残りは通常の関数型のように機能します。この場合、部分的なアプリケーションもあります。

BinaryTree t :: * -> *

BinaryTree t「型から型への関数」を意味します。これは、別の型に適用できるため、意味があります。

f :: (BinaryTree t) a -> (BinaryTree t) b
         * -> *     *        * -> *     *

BinaryTree tパーツが type に適用され、typeが得aられますBinaryTree t a :: *。(BinaryTree t)alone はまだ完全には適用されていません* -> *。f 1(これは when still has type Int -> Intwhenと同じように機能しますf :: Int -> Int -> Int)

ここで行われているように、暗黙的な型のパラメーターと種類の署名に言及する通常の「アリティ宣言」を混在させることができることに注意してください。BinaryTree次のように書くこともできます。

data BinaryTree t a  -- normal variant

またはこのように：

data BinaryTree :: * -> * -> *  -- fully "kinded"

どちらの場合も、コンパイラBinaryTreeは が 2 つの型パラメーターを取ることを認識しています。

そして、それは何のためですか？まず、リンクに記載されているように、型がとるべき型パラメーターの数を明示的に宣言する必要がある、または宣言したい場合があります。(別名DataKinds )よりも異なる種類を使用すると、別の興味深いケースが発生する可能性があります。これを見てください：*

data Empty = Empty | NonEmpty
data BinaryTree (t :: Empty) (a :: *) :: * where 
   -- ...

ああ、確信が持てない場合に備えて、ghci では種類を調べることができます。以下と同じように機能し:tます。

Prelude> :k Either
Either :: * -> * -> *
于 2013-05-06T07:51:53.683 に答える