7.25. 役割

-XGeneralizedNewtypeDeriving (7.5.5.1. deriving節の一般化)を使うと、プログラマは、既存のクラスインスタンスを、newtypeのクラスインスタンスへと「持ち上げる」ことができる。しかし、これは常に安全なわけではない。以下の例を考えよ。

newtype Age = MkAge { unAge :: Int }

type family Inspect x
type instance Inspect Age = Int
type instance Inspect Int = Bool

class BadIdea a where
  bad :: a -> Inspect a

instance BadIdea Int where
  bad = (> 0)

deriving instance BadIdea Age    -- これはだめ!

仮にこの自動導出インスタンスが許可されたとすると、badの型は何になるだろうか。Age -> Inspect Ageになりそうで、この型はAge -> Intと同等である。しかし、Intのインスタンスの実装を単純に再利用しようとすると、badの実装がBoolを返すことになる。これは問題である。

このような状況を発見する方法は、データ型、クラス、型シノニムの型変数に役割を割り当てることである。

GHCでの役割の実装は、POPL 2011で公開されたGenerative type abstraction and type-level computationに記述されている成果を単純化したものである。

7.25.1. 名目、表現、幽霊

役割システムの目的は、二つの型が同じ表現で表されるのがどのような場合か判断することである。上の例では、AgeIntは同じ表現を持っている。しかし、これらに対応するBadIdeaのインスタンスは同じ表現を持てないbadの実装の型の表現が異なるからである。

ある型構築子を、一箇所だけ異なる二通りのパラメータ群で使うことを考えよう。(たとえば、なんらかの型TについてT Age Bool cT Int Bool c。)型パラメタの役割は、これらの二つの型が同じ表現を持つために、二つの型引数について何を知らねばならないかを述べる(上の例では、T Age Bool cT Int Bool cが同じ表現を持つために、AgeIntについて何が成り立たねばならないか)。

GHCは、型パラメタの役割として三つのものに対応している。nominal(名目)、representational(表現)、phantom(幽霊)である。型パラメタの役割がnominalである場合、この二つの型は完全に一致しなければならない。これらは(型族を簡約した後で)同一でなければならない。型パラメタの役割がrepresentationalである場合、この二つの型は同じ表現を持たねばならない。(Tの最初のパラメタの役割がrepresentationalであれば、T Age Bool cT Int Bool xは同じ表現を持つことになる。AgeIntの表現が同じだからである)型パラメタの役割がphantomである場合、これ以上の情報は必要ない。

例をいくつか挙げる。

data Simple a = MkSimple a          -- aの役割はrepresentational

type family F
type instance F Int = Bool
type instance F Age = Char

data Complex a = MkComplex (F a)    -- aの役割はnominal

data Phant a = MkPhant Bool         -- aの役割はphantom

Simpleのパラメタの役割はrepresentationalであり、これは一般にもっともよくある場合である。Simple AgeSimple Intと同じ表現を持つことになる。一方、型Complexのパラメタの役割はnominalである。Complex AgeComplex Intは同じでないからである。最後に、Phantom AgePhantom Boolは、AgeBoolが無関係であるにもかかわらず、同じ表現を持つ。

7.25.2. 役割推論

ある型パラメタが与えられたとき、それが持つべき役割は何であろうか。GHCは、あらゆるパラメタについて、その正しい役割を決定するために役割推論を行なう。出発点は次に挙げる事実である。すなわち、(->)は二つのrepresentationalパラメタを持ち、(~)は二つのnominalパラメタを持つ。全ての型族のパラメタはnominalである。全てのGADT的パラメタはnominalである。次に、これらの型が使われるあらゆる場所に、これらの事実が伝播する。データ型とシノニムについては、デフォルトの役割はphantomである。クラスについては、デフォルトの役割はnominalである。よって、データ型やシノニムでは、右辺で使われていないパラメタ(や、phantomの位置でしか使われていない型変数)はphantomになる。パラメタがrepresentationalの位置(すなわち、構築子の型引数として使われていて、その構築子の対応する変数がrepresentationalである)で使われている場合、その役割はrepresentationalに引き上げられる。同様に、パラメタがnominalの位置で使われている場合、その役割はnominalに引き上げられる。役割がnominalからrepresentationalやphantomへ、あるいはrepresentationalからphantomへと引き下げられることはない。このようにすることで、それぞれのパラメタについて最も一般的な役割が推論される。

クラスについては、クラスインスタンスの整合性を促進するため、デフォルトの役割はnominalになっている。C Intがデータ型の中に保存されている場合、それがどこかでC Ageへと変わるのはかなり問題である。C Ageの別のインスタンスが宣言されている場合は特にそうである。

一つ、説明を要する難しいケースがある。

data Tricky a b = MkTricky (a b)

Trickyの役割は何になるべきか?abはどちらも右辺で使われており、どちらも型族に関係していないので、一見すると両方ともrepresentationalであるべきなように思える。しかし、以下の例が示すようにこれは間違っている。

data Nom a = MkNom (F a)   -- 上の例から取った型族F

Tricky Nom Ageの表現はTricky Nom Intと同じだろうか?そうではない。前者がCharを持つのに対して、後者はBoolを持つ。この問題の解決策は、型変数の型パラメタの役割が全てnominalであることを要請することである。よって、GHCはaについてはrepresentationalを推論するが、bにはnominalを推論する。

7.25.3. 役割注釈

プログラマがこの推論仮定に制約を与えたいこともある。例えば、baseライブラリには以下の定義がある。

data Ptr a = Ptr Addr#

問題は、aが本来はrepresentationalのパラメタであるべきなのに、役割推論によればphantomが割り当てられることである。これは、それなりに理屈が通っている。Intへのポインタは、実際にBoolへのポインタと同じ表現を持っている。しかし、我々はこんなふうにPtrを使いたい訳ではない!よって、以下のように言うことができてほしい。

type role Ptr representational
data Ptr a = Ptr Addr#

このtype role (-XRoleAnnotationsによって有効になる)宣言は、パラメタaにphantomでなくrepresentationalの役割を強制的に与える。すると、GHCは、このユーザ指定の役割がいかなる約束も破らないことを検査する。例えば、ユーザがBadIdeaの役割をrepresentationalにできると問題である。

別の例として、型aOrdインスタンスに沿って順序の付いたデータの集合を表現するSet aという型を考えることができる。aの役割がrepresentationalであると考えても一般には型安全ではあるが、newtypeは元の型とは別のOrdインスタンスを持っていることがある。これは実行時の誤動作につながる。よって、Setデータ型の作者は、そのパラメタをnominalにしたいと思うだろう。これは以下の宣言によって可能である。

type role Set nominal

もしプログラマがクラスにrepresentational(あるいはphantom)の役割を持たせたいと思った場合、それも役割注釈で可能である。

役割注釈が必要になる他の場所はhs-bootファイル(4.7.9. 相互再帰的なモジュールをコンパイルするには)である。ここでは、定義の右辺が省略可能である。hs-bootファイルで宣言された型やクラスはhsファイルでの定義と役割も含めて一致しなければならない。hs-bootファイルにおけるデフォルトの役割は、よくある場合であるrepresentationalである。

役割注釈を与えることは、data、newtype、classの宣言について許される。役割注釈はtype roleで始まり、その後に各パラメタにつき一つの役割指定が置かれる。(ここでのパラメタには、GADT様式のdataやnewtype宣言において、種シグネチャによって暗黙に指定されたパラメタも含まれる)役割指定は、役割(nominalrepresentationalphantom)か、_である。_を使うと、GHCがその役割を推論するべきだと言ったことになる。役割注釈は、そのデータ型やクラスの定義と同じモジュール内であれば、どこに置いてもよい(これは値水準の型シグネチャと同様である)。例をいくつか挙げる。

type role T1 _ phantom
data T1 a b = MkT1 a     -- bは使われてない。注釈は問題ないが、不要である

type role T2 _ phantom
data T2 a b = MkT2 b     -- エラー: bは使われており、phantomにはなれない

type role T3 _ nominal
data T3 a b = MkT3 a     -- OK: nominalは必要以上に高いが、安全である

type role T4 nominal
data T4 a = MkT4 (a Int) -- OKだが、nominalは必要以上に高い

type role C representational _
class C a b where ...    -- OK。bはnominalの役割を得る

type role X nominal
type X a = ...           -- エラー: 型シノニムに役割注釈を与えることはできない