この節では、種多相性と、-XPolyKindsによって有効になる拡張について記述する。これはTLDI 2012に現れた論文Giving Haskell a Promotionにより詳しく記述されている。
現在、Typeableの実装にはコードの重複が沢山ある(7.5.3. より広範なクラスについてのderiving節(Typeable、Dataなど))。
class Typeable (t :: *) where typeOf :: t -> TypeRep class Typeable1 (t :: * -> *) where typeOf1 :: t a -> TypeRep class Typeable2 (t :: * -> * -> *) where typeOf2 :: t a b -> TypeRep
種多相(-XPolyKindsで)は、これらのクラスを一つにまとめることを可能にする。
data Proxy t = Proxy class Typeable t where typeOf :: Proxy t -> TypeRep instance Typeable Int where typeOf _ = TypeRep instance Typeable [] where typeOf _ = TypeRep
データ型Proxyはforall k. k -> *という種を持っていることに注意(GHCによって推論される)。またこの新しいTypeableクラスの種はforall k. k -> Constraintである。
一般的に言って、-XPolyKindsの下では、GHCは装飾のない宣言について可能な限り多相的な種を推論する。例えば、
data T m a = MkT (m a) -- GHCが推論する種は T :: forall k. (k -> *) -> k -> *
項の世界と同様に、種シグネチャ(種注釈と呼ばれることもある)を使うことで多相性に制限を加えることができる (-XPolyKindsは-XKindSignaturesも有効にする)
data T m (a :: *) = MkT (m a) -- GHCが推論する種は T :: (* -> *) -> * -> * になる
種変数についての"forall"はない。代わりに、型変数を束縛する際、この束縛に対する種注釈の中で単に種変数に言及することができる。次のように。
data T (m :: k -> *) a = MkT (m a) -- GHCが推論する種は T :: forall k. (k -> *) -> k -> * になる
種についての"forall"は、その種変数に言及する型変数の束縛の中で最も外側にあるもののすぐ外側に置かれる。例を挙げる。
f1 :: (forall a m. m a -> Int) -> Int
-- f1 :: forall (k:BOX).
-- (forall (a:k) (m:k->*). m a -> Int)
-- -> Int
f2 :: (forall (a::k) m. m a -> Int) -> Int
-- f2 :: (forall (k:BOX) (a:k) (m:k->*). m a -> Int)
-- -> Int
ここで、f1では、この多相種変数に言及している種注釈がないので、kはf1のシグネチャの最上位で一般化され、これによってf1のシグネチャが目一杯多相的になる。しかし、f2の場合は、forall (a:k)という束縛の中で種注釈を与えているので、GHCは種のforallもちょうどその位置に置く。
(注意: これらの規則はややまわりくどく、ぎこちなさがある。もしかすると、GHCは明示的な種量化を許すべきなのかもしれない。しかし、暗黙の量化(例えば上のデータ型Tの宣言内のもの)は間違いなく非常に便利であり、明示的な量化の構文をどうすべきかも明らかでない)
型推論の場合と同様に、再帰的な型についての種推論は単相再帰しか扱えない。以下の(人為的な)例を考えよ。
data T m a = MkT (m a) (T Maybe (m a)) -- GHCが推論する種は T :: (* -> *) -> * -> *
Tが再帰的に使われることによって、第二引数の種が*に固定されている。しかし、型推論の場合と同様に、Tに完全な種シグネチャを付けることで多相再帰を実現できる。データ型に完全な種シグネチャを与えるには、次のようにGADT様式の宣言を使い、明示的な種シグネチャを付ける。
data T :: (k -> *) -> k -> * where MkT :: m a -> T Maybe (m a) -> T m a
このユーザ指定の完全な種シグネチャがTについて多相的な種を指定しており、再帰的なものを含めたTの呼び出し全てに利用される。特に、Tの再帰呼び出しは種*においてである。
型構築子の「ユーザ指定の完全な種シグネチャ」とみなされるのは正確に何か？以下のものである。
ヘッダに明示的な「::」を含むGADT様式のデータ型宣言
data T1 :: (k -> *) -> k -> * where ... -- 可 T1 :: forall k. (k->*) -> k -> * data T2 (a :: k -> *) :: k -> * where ... -- 可 T2 :: forall k. (k->*) -> k -> * data T3 (a :: k -> *) (b :: k) :: * where ... -- 可 T3 :: forall k. (k->*) -> k -> * data T4 a (b :: k) :: * where ... -- 可 T4 :: forall k. * -> k -> * data T5 a b where ... -- 非 種は推論される data T4 (a :: k -> *) (b :: k) where ... -- 非 種は推論される
「::」を置くのはどこでもいいが、どこかには置かなければならない。Haskell98様式のデータ型宣言を使って完全な種シグネチャを与えることはできない。GADT構文を使う必要がある。
開型族やデータ族宣言は、常にユーザ指定の完全な種シグネチャを持つ。「::」は必要ない。
data family D1 a -- D1 :: * -> * data family D2 (a :: k) -- D2 :: forall k. k -> * data family D3 (a :: k) :: * -- D3 :: forall k. k -> * type family S1 a :: k -> * -- S1 :: forall k. * -> k -> * class C a where -- C :: k -> Constraint type AT a b -- AT :: k -> * -> *
上の最後の例において、変数aは、クラス宣言に由来する暗黙の種変数注釈を持ち、この多相種は関連型族宣言の中にまで持ち込まれる。しかし、変数bは、デフォルトの*を与えられる。
ユーザ指定の完全な種シグネチャにおいて、「::」の左側の装飾のない型変数はすべて種「*」を持つとみなされる。種多相性が必要なら種変数を指定しなければならない。
開型族は全て完全なユーザ指定の種シグネチャを持つとみなされるが、閉型族については、等式上で種推論を行なうことができるので、この条件を緩めることができる。閉型族の型変数のうち、その種がパターン照合に使われないようなもの全てについて、GHCは種を推論する。種変数をパターン照合のために使いたいなら、その種変数は明示的に宣言しなければならない。
例をいくつか挙げる(-XDataKindsが有効になっていると仮定している)
type family Not a where -- Not :: Bool -> Bool Not False = True Not True = False type family F a where -- エラー: 種変数についてのパターン照合が必要 F Int = Bool F Maybe = Char type family G (a :: k) where -- G :: k -> * G Int = Bool G Maybe = Char type family SafeHead where -- SafeHead :: [k] -> Maybe k SafeHead '[] = Nothing -- kはパターン照合の際に必要とされないことに注意 SafeHead (h ': t) = Just h
以下の多相種クラスと、そのインスタンスを例として考えよ。
class C a where type F a instance C b where type F b = b -> b
このクラス宣言において、型aの種を制約するものは何もないので、これは種多相的な型変数(a :: k)になる。しかし、上のインスタンス宣言においては、関連型インスタンスの右辺であるb -> bが、bの種が*でなければならないことを示している。理論的には、GHCはこの情報をインスタンス頭部にまで伝播させ、このインスタンス宣言を、任意の種ではなく種*を持つ型のみに適用するようにすることができる。しかし、GHCはこれを行なわない。
要約すると、GHCは、クラスインスタンス宣言のメンバからインスタンス頭部へと種情報を伝播させることはしない。
この種の推論が行なわれないのは、単にGHC内部の工学上の問題であるが、これを動作させるには推論機構への大幅な変更が必要になり、これが割に合うかどうか明確でない。上のインスタンスでbの種を制限したいなら、単にインスタンス頭部の中で種シグネチャを使えばよい。