7.8. 種多相

この節では、種多相性と、-XPolyKindsによって有効になる拡張について記述する。これはTLDI 2012に現れた論文Giving Haskell a Promotionにより詳しく記述されている。

7.8.1. 種多相の概観

現在、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である。

7.8.2. 概観

一般的に言って、-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 -> * になる

7.8.3. 多相種再帰と完全な種シグネチャ

型推論の場合と同様に、再帰的な型についての種推論は単相再帰しか扱えない。以下の(人為的な)例を考えよ。

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 -> *

ユーザ指定の完全な種シグネチャにおいて、「::」の左側の装飾のない型変数はすべて種「*」を持つとみなされる。種多相性が必要なら種変数を指定しなければならない。