種類署名

Question

私はハスケルのwikiの本を経由しています。GADTS

https://en.wikibooks.org/wiki/Haskell/GADTガイドです。

コンスコンストラクタの制約付きタイプを一般化するKindシグネチャが追加されるまで、かなりうまくトラッキングしていました。私は安全と危険の両方MarkedListsに対して構築する短所コンストラクタを使用してパターンマッチすることができます種類の署名で

data Safe 
data NotSafe 

data MarkedList    :: * -> * -> * where 
    Nil      :: MarkedList t NotSafe 
    Cons      :: a -> MarkedList a b -> MarkedList a c 

safeHead     :: MarkedList a Safe -> a 
safeHead (Cons x _)   = x 


silly 0      = Nil 
silly 1      = Cons() Nil 
silly n      = Cons() $ silly (n-1) 

。私は何が起こっているのか理解していますが、残念なことに、Kind Signatureがこれをどのように許可しているかについての直感を築くのは難しいです。なぜ私はKind Signatureが必要なのですか？カインドシグネチャは何をしていますか？

Answer 1

タイプシグネチャが値に対して機能するのと同じように、種別シグネチャはタイプに対して機能します。

f :: Int -> Int -> Bool 
f x y = x < y 

ここで、fは2つの引数値をとり、結果値を生成します。タイプの等価は以下のようになります。

data D a b = D a b 

タイプD（それは* -> * -> *である）2つの引数の型を取り、結果の型を生成します。たとえば、D Int Stringはタイプ（これは種類が*です）です。部分アプリケーションD Intは、部分アプリケーションf 15のタイプがInt -> Boolであるのとまったく同じ方法で、種類が* -> *です。

だから我々は、上記のように書き換えることができます：

GHCiの中

data D :: * -> * -> * where 
    D :: a -> b -> D a b 

、あなたがタイプと種類を照会することができます

> :type f 
f :: Int -> Int -> Bool 
> :kind D 
D :: * -> * -> *