種多相
TypeInType
PolyKinds，DataKinds，KindSignatures
8.0.1以降
過去には，この拡張は高度な型レベルのプログラミング手法を可能にするために使用されていた．今では他のいくつかの拡張機能の省略形である．
PolyKinds
KindSignatures含む
7.4.1以降
種多相な型を許可する．
この節では，バージョン8.0以降でのGHCの種システムについて説明する．
ここで説明されている種システムは，拡張があってもなくても常に有効だが，標準のHaskellを超えた保守的な拡張である．上記の拡張は単純に構文を有効にし，推論アルゴリズムを微調整してユーザーがGHCの種システムの追加の表現力を利用できるようにする．
種多相の概要
以下の種を推論することを考えてみよう．
code: kp1.hs
data App f a = MkApp (f a)
Haskell 98では，Appの推論される種は(Type -> Type) -> Type -> Typeである．しかしこれは必要以上に具体的である．というのも，なぜならHaskell98(の仕様)に適するもう一つのAppの種として((Type -> Type) -> Type) -> (Type -> Type) -> Typeがあるからである．ここでaに割り当てられる種はType -> Typeとなっている。実際に，種シグネチャ(KindSignatures拡張)がないと，Haskellコンパイラに2番目の種を推論させるためにダミーのコンストラクタを使う必要がある．種多型(PolyKinds)を使えば，GHCは，Appの種として，最も一般的な種であるforall k. (k -> Type) -> k -> Type種を推論する．
したがって，種多相の主な利点は，これらの最も一般的な種を推論し，さまざまな種でAppを使えるようにすることである．
code: kp2.hs
App Maybe Int -- k is instantiated to Type
data T a = MkT (a Int) -- a is inferred to have kind (Type -> Type)
App T Maybe -- k is instantiated to (Type -> Type)
Type-in-Typeの概要
GHC 8は，型と種が実際にはまったく同じものであると宣言することによって，種の多相性の概念を拡張する．GHCの中では型と種を区別するものは何もない．これについて考えるもう一つの方法は，型Boolと「昇格された種」Boolは実際には同一であるということである(項Trueは式の中で使われ，型'Trueは型の中で使われるので，項Trueと型'Trueは未だに違うことに注意せよ)．この型と種の区別のなさは，依存型付き言語の特徴である．完全依存型付き言語は式と型の違いをも取り除くが，GHCでそれを行うことはまたの日の話である．
型と種を組み合わせることによって可能になる1つの単純化は， Typeの型が単なるTypeであるということである．Type :: Type公理が非決定性につながる可能性があるのは事実だが，型と式の両方でプログラムを非決定にする方法が他にもあるため，これはGHCでは問題にない．この決定(他にも多数あるが)は，GHCの型システムの表現力にもかかわらず，Haskellで書いた「証明」は反論の余地のない数学的証明ではないことを意味している．GHCは部分的な正当性のみを保証する．あなたのプログラムがコンパイルされて完全に実行されるなら，それらの結果は確かに割り当てられた型を持つ．有限時間内に終了しないプログラムについては何も言わない．
この決定と内部でのGHCの設計についてもっと学びたければ， この種システムをGHC / Haskellに導入した論文を参照せよ． 種推論の原則
一般的に言って，PolyKindsが有効なとき，GHCは宣言での最も一般的な種を推論しようとする．多くの場合(例えば，データ型宣言の中で)，定義は種推論を知らせる右辺を持つ．しかし，必ずしもそうとは限らない．次の例を考えてみよう．
code: kp3.hs
type family F a
型族宣言には右辺はないが，それでもGHCはFに対して種を推論しなければない．制約がないので，F :: forall k1 k2. k1 -> k2と推論することもできようが，これは多相的すぎるように見える．そのため，GHCはこれらの全く制約のない種変数の種のデフォルトをTypeにし，F :: Type - > Typeを得る．種シグネチャを使って，Fを種多相に宣言することもできる．
code: kp4.hs
type family F1 a -- F1 :: Type -> Type
type family F2 (a :: k) -- F2 :: forall k. k -> Type
type family F3 a :: k -- F3 :: forall k. Type -> k
type family F4 (a :: k1) :: k2 -- F4 :: forall k1 k2. k1 -> k2
一般的な原則は以下の通りである．
右辺があるとき，GHCは右辺と整合する最も多相的な種を推論する．例：通常のデータ型とGADT宣言，クラス宣言など．クラス宣言の場合，「右辺」の役割はクラスのメソッドのシグネチャによって行われる．
右辺がないとき，型シグネチャでそうでないと指定されない限り，GHCは引数と結果の種をデフォルトで Typeにする．例：データ族と開いた型族の宣言．
code: kp5.hs
class C a where -- Class declarations are generalised
-- so C :: forall k. k -> Constraint
data D1 a -- No right hand side for these two family
type F1 a -- declarations, but the class forces (a :: k)
-- so D1, F1 :: forall k. k -> Type
data D2 a -- No right-hand side so D2 :: Type -> Type
type F2 a -- No right-hand side so F2 :: Type -> Type
クラス宣言からの種多相でD1は種多相になるが，D2はそうはならない．F1とF2についても同様である．
完全なユーザ指定の種シグネチャと多相再帰
型推論と同様に，再帰型の種推論では単相再帰のみ使用できる．次の(わざとらしい)例を考えてみよう．
code: kp6.hs
data T m a = MkT (m a) (T Maybe (m a))
-- GHC infers kind T :: (Type -> Type) -> Type -> Type
Tを再帰的に使用すると，2番目の引数はType種に強制される．ただし，型推論の場合と同様に，Tに完全なユーザ指定の種シグネチャ(complete user-supplied kind signature, CUSK)を与えることで，多相再帰を実現できる．CUSKとは，推論の必要がない，すべての引数の種と結果の種が分かるようにしたときのことをいう．例えば，
code:kp7.hs
data T (m :: k -> Type) :: k -> Type where
MkT :: m a -> T Maybe (m a) -> T m a
完全なユーザ指定の種シグネチャはTの多相的な種を指定し，このシグネチャは再帰的なものも含めてTへのすべての呼び出しに使用される．特に，Tの再帰的な使用にはTypeが使われる．
型コンストラクタの「完全なユーザ指定の種シグネチャ」とは正確には何だろうか？次の形式のことである．
データ型の場合は，すべての型変数に種注釈が付いている必要がある．GADTスタイルの宣言では，(トップレベルの::がヘッダにある)種シグネチャがあってもよいが，この注釈の有無は，宣言が完全なユーザ指定の種シグネチャを持つかどうかには影響しない(訳注：kp8.hsの例ではT1, T2, T3, T5がトップレベルの種注釈を持っている．しかし，CUSKを持つのはT1 - T4なので，注釈の有無とCUSKを持つかどうかは全く関係ないことがわかる)．
code:kp8.hs
data T1 :: (k -> Type) -> k -> Type where ...
-- Yes; T1 :: forall k. (k->Type) -> k -> Type
data T2 (a :: k -> Type) :: k -> Type where ...
-- Yes; T2 :: forall k. (k->Type) -> k -> Type
data T3 (a :: k -> Type) (b :: k) :: Type where ...
-- Yes; T3 :: forall k. (k->Type) -> k -> Type
data T4 (a :: k -> Type) (b :: k) where ...
-- Yes; T4 :: forall k. (k->Type) -> k -> Type
data T5 a (b :: k) :: Type where ...
-- No; kind is inferred
data T6 a b where ...
-- No; kind is inferred
トップレベルの::を持つデータ型については，::の後に導入されたすべての種変数は明示的に量化する必要がある．
code:kp9.hs
data T1 :: k -> Type -- No CUSK: k is not explicitly quantified
data T2 :: forall k. k -> Type -- CUSK: k is bound explicitly
data T3 :: forall (k :: Type). k -> Type -- still a CUSK
型クラスの場合は，すべての型変数に種注釈が付いていることが必要である．
型シノニムでは，すべての型変数と結果の型に種注釈を付ける必要がある．
code:kp10.hs
type S1 (a :: k) = (a :: k) -- Yes S1 :: forall k. k -> k
type S2 (a :: k) = a -- No kind is inferred
type S3 (a :: k) = Proxy a -- No kind is inferred
S2とS3においては，右辺の種はかなり明らかであるが，それでも完全なシグネチャを持っているとはみなされない．というのも， シグネチャが検出されるまではいかなる推論もすることができないためである．
関連型を除く開いた型族，またはデータ族の宣言には常にCUSKがある．注釈なしの型変数は，Type種に初期化される．
code:kp11.hs
data family D1 a -- D1 :: Type -> Type
data family D2 (a :: k) -- D2 :: forall k. k -> Type
data family D3 (a :: k) :: Type -- D3 :: forall k. k -> Type
type family S1 a :: k -> Type -- S1 :: forall k. Type -> k -> Type
関連型またはデータ族の宣言は，それを囲むクラス(訳注：関連型，関連データ族が定義されている型クラスのこと)がCUSKを持っていれば，そしてそのときに限り，CUSKを持つ．
code:kp12.hs
class C a where -- no CUSK
type AT a b -- no CUSK, b is defaulted
class D (a :: k) where -- yes CUSK
type AT2 a b -- yes CUSK, b is defaulted
閉じた型族は，そのすべての型変数に注釈が付けられ，(トップレベル::を持つ)返り種が指定されている場合，完全なユーザ指定の種シグネチャを持つ．
構文的には(上記の規則によれば)CUSKを持つが，何らかの推論を必要とするデータ型を書くことは可能である．非常にわざとらしい例として，次の例を考えよう．
code:kp13.hs
data Proxy a -- Proxy :: forall k. k -> Type
data X (a :: Proxy k)
上記の規則によると，XにはCUSKがある．しかし，kの種は未定である．これは，ゆえに量化され直され，Xにforall k1 (k :: k1). Proxy k -> Typeという種を与える．
閉じた型族における種推論
すべての開いた型族は完全なユーザ指定の種シグネチャを持つと見なされるが，閉じた型族の場合，(訳注：型インスタンスに対応する部分の)等式上で種推論を行うことができるので，この条件を緩和することができる．GHCは，閉じた型族の引数と結果の型の種を推論する(訳注：等式上で推論できるのは，閉じた型族はあとからインスタンスが追加されないため)．
GHCは，種上の族としても型上の族としても適するような種添字付き型族をサポートする(訳注：種添字付け型族は，定義された族が返すものが型でも種でも整合性をもつということ．これはGHCでは種と型がほぼ同等に扱われているためである)．GHCは，完全なユーザ指定の種類シグネチャがないと，まれに主要ではない型を推論するかもしれないので，この動作を推論しない．確かに，種添字付けは多相再帰の形式として見ることができる．そこでは，型はそれ自身の定義で最も一般的なもの以外の種で使われる．例えば以下の例がある．
(訳注：主要型(principal type)とは，型システムにおける，その条件下で導き出される最も一般的な型のこと．詳しくは型システム入門を読もう！)
code:kp14.hs
type family F1 a where
F1 True = False
F1 False = True
F1 x = x
-- F1 fails to compile: kind-indexing is not inferred
type family F2 (a :: k) where
F2 True = False
F2 False = True
F2 x = x
-- F2 fails to compile: no complete signature
type family F3 (a :: k) :: k where
F3 True = False
F3 False = True
F3 x = x
-- OK
クラスインスタンス宣言における種推論
次の多層的な種付き型クラスとそのインスタンスの例を考えてみよう．
code: kp15.hs
class C a where
type F a
instance C b where
type F b = b -> b
型クラス宣言では，型aの種を制限するものは何もないので，多相的な種付き型変数(a :: k)になる．しかし，インスタンス宣言では，関連型のインスタンスの右辺のb -> bは，bはType種でなければならないことを示している．GHCは理論的には，この情報をインスタンス宣言の先頭に伝播し，そのインスタンスの宣言を，任意の種の型とは対照的に，Type種の型にのみ適用することもできよう．しかし，GHCはこれをしない．
一言で言えば，GHCはクラスインスタンス宣言のメンバからインスタンス宣言の先頭に種の情報を伝播しない．
このような種推論の欠如は，単にGHC内の技術的な問題だが，それを機能させることは推論基盤にかなりの変更を加えることになり，そこまでするほどその見返りに価値があるかは明らかではない．上記のインスタンスでbの種を制限したい場合は，インスタンス宣言先頭に種シグネチャをつけること．
型シグネチャにおける種推論
型の種検査をするとき，GHCはその型の種を一般化する方法を見つけ出すときに，その型に書かれているものだけを考慮する．
例えば，次の定義を考えてみよう(ScopedTypeVariables拡張を使用している)．
code: kp16.hs
data Proxy a -- Proxy :: forall k. k -> Type
p :: forall a. Proxy a
p = Proxy :: Proxy (a :: Type)
GHCはエラーを吐き，aの種はTypeではなく種変数kであるべきだと言ってくる．これは，型シグネチャforall a. Proxy aを見て，GHCはaの種が一般化されるべきでType種に制限されるべきではないと見なすからである．そしてその後，関数定義はその型シグネチャよりも具体的であるとして拒否される．
明示的な種の量化
PolyKindsによって有効になる機能だが，GHCは以下のように明示的な種の量化をサポートする．
code: kp17.hs
data Proxy :: forall k. k -> Type
f :: (forall k (a :: k). Proxy a -> ()) -> Int
二つ目の例は，kの種と型変数aの種kの両方を束縛しているforallがあることに注意せよ．一般に，この種の依存関係がどれだけ深くネストされた状態で機能するかの制限はない．ただし，依存関係はwell-scopedでなけらばならない．例えば，forall (a :: k) k . ...はエラーである．
後方互換性のために，型がforallで始まっていても，種変数は明示的に束縛される必要はない．
したがって，より高階の文脈における種の量化の規則はわずかに変更されている．GHC 7では，トップレベル以外のforallで束縛された変数の種の中で，種変数が初めて言及された場合，その種変数もそこで束縛されていた．つまり，f :: (forall (a :: k). ...) -> ... では，kはaと同じforallで束縛されていた．しかしGHC 8では，型の中で言及されているすべての種変数は最も外側のレベルで束縛されている．より高階のforallで束縛したいならば，それを明示的に含めなくてはならない．
種添字付きGADT
以下の型を考えてみよう．
code:kp18.hs
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
このデータ型Gは，その種と型の両方においてGADTに似ている．a :: kとしてg :: G aがあるとしよう．そして，パターンマッチすることでgが実はGMaybeであったということを発見することによって，k ~ (Type -> Type)であることとa ~ Maybe であることを知ることになる．Gの定義にはPolyKindsが有効であることを必要とするが，Gに対してパターンマッチするにはGADTを超えた拡張を必要としない．これが機能するのは，実は通常のGADTを単純に拡張したものであり，種と型が同じという事実の結果である．
データ型Gはその本体内で複数の種で使用されていること，そしてその結果として種添字付きGADTは多相再帰の形式を使用していることに留意せよ．したがって，この機能を使用できるのは，データ型に対して完全なユーザー指定の種シグネチャ(完全なユーザー指定の種シグネチャと多相再帰)を指定した場合に限られる．
高ランク種
RankNTypesと連携して，GHCはより高階の種をサポートする．一例は以下の通りである．
code:kp19.hs
-- Heterogeneous propositional equality
data (a :: k1) :~~: (b :: k2) where
HRefl :: a :~~: a
class HTestEquality (t :: forall k. k -> Type) where
hTestEquality :: forall k1 k2 (a :: k1) (b :: k2). t a -> t b -> Maybe (a :~~: b)
hTestEqualityは，型変数tに適用される型を持つ2つの引数を取り，それらの種が異なることに留意せよ．その型変数は，ゆえに多相的な種である必要がある．従って，HTestEquality(クラス)の種は(forall k. k -> Type) -> Constraintであり，これは高階の種である．
高階の種と高階の型の大きな違いとして，高階の種ではforallを移動させることができないというのがある．これは例を示すのが最良の説明である．(:~~:)に対するHTestEqualityのインスタンスを作成したいとしよう．
code:kp20.hs
instance HTestEquality ((:~~:) a) where
hTestEquality HRefl HRefl = Just HRefl
上記のように(:~~:)を宣言したことにより，(:~~:)は種forall k1 k2. k1 -> k2 -> Typeを得る．ゆえに，型(:~~:) aは，何らかのk2に対して，種k2 -> Typeを持つ．そしてその後に(お望みのとおりに)この種を再び一般化してforall k2. k2 -> Typeにすることは，GHCにはできない．したがって，インスタンスはill-kindedとして拒否される．
そのようなインスタンスを可能にするためには，(:~~:)を次のように定義する必要があるだろう．
code:kp21.hs
data (:~~:) :: forall k1. k1 -> forall k2. k2 -> Type where
HRefl :: a :~~: a
この再定義では，(:~~:)に明示的な種を与え，最初の引数(a)が与えられるまでk2の選択が延期される．この(:~~:)の宣言では，(訳注：kp20.hsの)HTestEqualityのインスタンスが受け入れられる．
高階の種と型の間のもう1つの違いは，推論された型変数およびユーザ指定の型変数の扱いにある．次のプログラムを考えよう．
code:kp22.hs
newtype Foo (f :: forall k. k -> Type) = MkFoo (f Int)
data Proxy a = Proxy
foo :: Foo Proxy
foo = MkFoo Proxy
Fooのパラメータの種はforall k. k -> Typeだが，Proxyの種はforall {k}. k -> Typeである(ここで{k}は，種変数kは推論されるものであって，ユーザによって指定されるものではないことを表している)(「推論される」と「指定される」の区別の詳細については，Visible type applicationを参照せよ)．GHCはforall k. k -> Type と forall {k}. k -> Typeを種レベルで同一であるとは考えないため，Foo Proxyをill-kindedとして拒否する． 種における制約
種と型は同じであるため，種には(PolyKindsを使用する場合)型制約を含めることができる．ただし，現在サポートされているのは等価制約のみである．将来的には他の制約も使用できるようになると考えられる．
次は制約付きの種の例である．
code: kp23.hs
type family IsTypeLit a where
IsTypeLit Nat = 'True
IsTypeLit Symbol = 'True
IsTypeLit a = 'False
data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where
MkNat :: T 42
MkSymbol :: T "Don't panic!"
上記の宣言は許される．しかし，MkOther :: T Intを追加すると，Intは型リテラルではないので，等価制約が満たされないというエラーが発生する．ここで，forall aを使用して明示的に量化する必要はないことに注意せよ．
Type種
StarIsType
8.6.1以降
修飾されていない*型演算子の使用は，nullaryな（引数を取らない）演算子として扱われ，Data.Kind.Typeの代用として扱われる．
Type種(Data.Kindからインポートされる)は普通の型を分類する． StarIsType(現在はデフォルトで有効)があれば，*はTypeへと脱糖されるが，このレガシー構文を使用することはTypeOperatorsとの衝突を理由に非推奨である．これは★(Unicodeにおける*の変種)にも適用される．
データ型宣言における依存関係の推論
データ型，型クラス，または型族の宣言内の型変数aが，同じ宣言内の別のそのような変数kに依存している場合，次の2つの性質が成り立つ必要がある．
宣言の中で，aはkの後に現れなければならない．
kはその宣言内のなんらかの型変数の種の中で明示的に現れなければならない．
最初の条件は，単に依存関係の範囲が厳密(well-scoped)でなければならないことを意味している．2番目の条件は，依存関係を推論するGHCの能力に関するものである．この依存関係を推論することは困難であり，GHCは現在依存関係を明示的にすることを要求している．つまり，kは型変数の中に現れなければならないということである．例えば，
code:kp24.hs
data Proxy k (a :: k) -- OK: dependency is "obvious"
data Proxy2 k a = P (Proxy k a) -- ERROR: dependency is unclear
2番目の宣言では，GHCはkが従属変数であるべきだとすぐに言うことはできないので，宣言は拒否される．
この制限が将来緩和される可能性はあるが，この状況を取り巻く問題が理論的なものか(この依存関係を推論することは私たちの型システムに主要型がないことを意味する)それとも単なる実用上のものなのか(GHCの実装を考えると，この依存関係を推論するのは難しい)は(この文書が書かれている現在では)明らかでない．故に，GHCは簡単な方法を取り，ユーザからの少しの助けを必要とするのである．
ユーザ記述のforall下での依存関係の推論
プログラマは，新しい量化された型変数を導入するために型内でforallを使用することができる．これらの変数は変数同士が依存していてもよく，同じforallの中でさえこれは許される．しかし，GHCは，依存関係がforallの本体から推論可能であることを要求する．以下がいくつかの例である．
code:kp25.hs
data Proxy k (a :: k) = MkProxy -- just to use below
f :: forall k a. Proxy k a -- This is just fine. We see that (a :: k).
f = undefined
g :: Proxy k a -> () -- This is to use below.
g = undefined
data Sing a
h :: forall k a. Sing k -> Sing a -> () -- No obvious relationship between k and a
h _ _ = g (MkProxy :: Proxy k a) -- This fails. We didn't know that a should have kind k.
最後の例では，aがforallの本体(つまり，Sing k -> Sing a -> （）)からkに依存していることを知ることは不可能である．故にGHCはそのプログラムを拒否する．
PolyKindsを使わない場合の種のデフォルト
PolyKindsがなければ，GHCは種変数について一般化することを拒否する．したがって，可能であれば，型変数のデフォルトはTypeになり，これが不可能な場合は，エラーが出される．
例は以下の通りである．
code:kp26.hs
{-# LANGUAGE PolyKinds #-} import Data.Kind (Type)
data Proxy a = P -- inferred kind: Proxy :: k -> Type
data Compose f g x = MkCompose (f (g x))
-- inferred kind: Compose :: (b -> Type) -> (a -> b) -> a -> Type
-- separate module having imported the first
{-# LANGUAGE NoPolyKinds, DataKinds #-} z = Proxy :: Proxy 'MkCompose
最後の行では，我々は昇格されたコンストラクタ'MkComposeを使っている．'MkComposeの種は次のとおりである．
code:kp27.hs
forall (a :: Type) (b :: Type) (f :: b -> Type) (g :: a -> b) (x :: a).
f (g x) -> Compose f g x
今度はzの型を推論しなければならない．種変数を一般化せずにそれを行うには，'MkComposeの種変数をデフォルトする必要がある．簡単にaやbをTypeにデフォルトすることができるが，fとgはデフォルトするとill-kindedになってしまう．したがってzの定義はエラーである．
種多相の存在下でのプリティプリンティング
種多相では，Haskellプログラマには見えないかもしれない舞台裏でかなりのことが起こっている．GHCは，エラーメッセージとGHCiプロンプトで型をどのように表示するかを制御するいくつかのフラグをサポートしている．詳細はtype pretty-printingオプションの議論 を参照せよ．もしあなたが種多相を使っていて，なぜGHCがあなたのプログラムを拒絶する(あるいは受け入れる)のかについて混乱しているなら，これらのフラグ，特に-fprint-explicit-kindsを有効にすることを推奨する．