7.8. 種多相と昇格

標準のHaskellには豊かな型言語が備わっている。型は式を分類し、多くのよくあるプログラミング上の間違いを避けるのに役立つ。一方で、Haskellの種言語(訳注: kind language; 型の型の言語)は比較的単純であり、持ち上げられた型(種*)と型構築子(たとえば種* -> * -> *)と持ち上げられていない型(7.2.1. 非ボックス化型 )を区別するのみである。特に型族(7.7. 型の族)やGADT(7.4.7. 一般化代数データ型(GADT))などの高度な型システムの機能を使う場合、この単純な種システムでは不十分であり、単純な間違いを防ぐことができない。例として、型水準の自然数と、長さによって添字付けられたベクトルを考えよ。

data Ze
data Su n

data Vec :: * -> * -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

Vecの種は* -> * -> *である。これば、例えばVec Int Charが種の正しい型であることを意味する。長さによって添字付けられたベクトルを定義するときにこれを意図している訳ではないにもかかわらずである。

-XPolyKindsおよび-XDataKindsフラグによって、より豊かな種言語の利用が可能になる。-XPolyKindsは種多相を有効にし、-XDataKindsはデータ型の昇格を通してユーザが種を定義することを可能にする。-XDataKindsを使うと、上の例は次のように書き直せる。

data Nat = Ze | Su Nat

data Vec :: * -> Nat -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

この改善されたVecの種のもとでは、Vec Int Charのようなものは今や種が間違っており、GHCはエラーを報告するだろう。

この節では、この新しい種システムの使い型の例を少し示す。この拡張は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である。

現在の実装にはいくつか制約がある。

種に関して抽象化したり、種変数に言及することは(まだ)できない。よって以下のものは全て拒絶される。
```
data D1 (t :: k)

data D2 :: k -> *

data D3 (k :: BOX)
```
型族の戻り種は常にデフォルトの*が使われる。よって以下のものは拒絶される。
```
type family F a
type instance F Int = Maybe
```

7.8.2. データ型の昇格

-XDataKindsを使うと、GHCは全ての適したデータ型を種へと昇格させ、その(値)構築子を型構築子へと昇格させる。以下の型は、

data Nat = Ze | Su Nat

data List a = Nil | Cons a (List a)

data Pair a b = Pair a b
 
data Sum a b = L a | R b

以下の種と型構築子を生み出す。

Nat :: BOX
Ze :: Nat
Su :: Nat -> Nat

List k :: BOX
Nil  :: List k
Cons :: k -> List k -> List k

Pair k1 k2 :: BOX
Pair :: k1 -> k2 -> Pair k1 k2

Sum k1 k2 :: BOX
L :: k1 -> Sum k1 k2
R :: k2 -> Sum k1 k2

例えばListがBOX -> BOXという種を得ないことに注意。種はそれ以上区別されないからである。全ての種はBOXというソートを持つ。

昇格には以下の制約が適用される。

我々は* -> ... -> * -> *という形の種を持つデータ型しか昇格させない。特に、data Fix f = In (f (Fix f))のような高階の種を持つデータ型や、Vec :: * -> Nat -> *のように昇格後の型が関わっている種を持つデータ型を昇格させることはしない。
構築子が種多相であったり、制約が関わっていたり、存在量化を使っていたりするデータ型は昇格させない。

7.8.2.1. 型と構築子の区別

昇格があると、構築子と型が同じ名前空間を共有するので、型名が曖昧になることがある。

data P          -- 1

data Prom = P   -- 2

type T = P      -- 1か、それとも昇格した2か？

このような場合には、昇格した構築子に言及したい場合、名前に引用符を前置する必要がある。

type T1 = P     -- 1

type T2 = 'P    -- 昇格した2

昇格したデータ型は名前の付いた種を生み出すことに注意。これらが曖昧になることはないので、種名に引用符を付けることは認めていない。

7.8.2.2. 昇格したリスト型とタプル型

Haskellのリストおよびタプル型は言語レベルで種へと昇格されており、引用符を前置する必要があるものの型水準でも同じ便利な記法が使える。

data HList :: [*] -> * where
  HNil  :: HList '[]
  HCons :: a -> HList t -> HList (a ': t)

data Tuple :: (*,*) -> * where
  Tuple :: a -> b -> Tuple '(a,b)

これは-XTypeOperatorsを必要とすることに注意。

7.8.3. 現在の実装の欠点

GHC 7.4のリリースに際しては、我々は新しい種多相的なcoreが既存のあらゆる(種多相を使っていない)プログラムを扱えるようにすることに焦点を置いた。-XPolyKindsに関して既に多くものが正しく動作するが、動かないものもあることを予想している。もし困難に陥ったら、どうかバグ報告をしてほしい！