型の族

添字付けされた型の族は、型レベルのプログラミングを容易にするための新しいGHC拡張である。型の族は、関連データ型(“Associated Types with Class”, M. Chakravarty, G. Keller, S. Peyton Jones, and S. Marlow. In Proceedings of “The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05)”, pages 1-13, ACM Press, 2005)および関連型シノニム(“Type Associated Type Synonyms”. M. Chakravarty, G. Keller, and S. Peyton Jones. In Proceedings of “The Tenth ACM SIGPLAN International Conference on Functional Programming”, ACM Press, pages 241-253, 2005)の一般化である。型の族自体は論文“Type Checking with Open Type Functions”, T. Schrijvers, S. Peyton-Jones, M. Chakravarty, and M. Sulzmann, in Proceedings of “ICFP 2008: The 13th ACM SIGPLAN International Conference on Functional Programming”, ACM Press, pages 51-62, 2008 Functional Programming”, ACM Press, pages 241-253, 2005)に記述されている。型の族は、要するに、型で添字付けされたデータ型と、型についての名前の付いた関数を提供する。これらは、総称(generic)プログラミングや高度にパラメタ化されたライブラリインタフェース、さらには、依存型と同様に、インタフェースにより多くの静的な情報を与えるのに有用である。また、型の族は関数従属の代わりとなるものとも見なされている。関数従属では型レベルのプログラミングを関係的に行うのに対して、型の族はより関数的な様式を可能にする。

添字付けされた型の族(indexed type family)、短くいうと型族(type family)は、型の集合を表すような型構築子である。集合の要素は、型族構築子に型引数(型添字と呼ぶ)を与えることで記述される。通常のパラメタ付きの型構築子と族構築子との違いは、パラメタ多相な関数と型クラスの(アドホック多相な)メソッドとの違いによく似ている。パラメタ多相な関数はあらゆる具体的な型に対して等しく振る舞うのに対し、クラスのメソッドはクラスの型パラメタに依存して振る舞いを変える。同様に、通常の型構築子はあらゆる具体的な型に対して同じデータ表現を使うことになるが、型族構築子は異なる型添字に対して異なる表現型を持つことができる。

添字付けされた型の族には二つの系統がある。データ族型シノニム族である。これらは、それぞれ代数的データ型と型シノニムを添字付けされた型の族にしたものである。データの族のインスタンスとしてはデータ型とnewtypeがありえる。

型の族は-XTypeFamiliesフラグによって有効になる。GHCで型の族を使うことについてのさらなる情報が型の族についてのHaskell wikiのページにある。

データ族

データ族には次の二つの系統がある。(1)最上位で定義されるもの (2)型クラスの中に現れるもの(この場合、これは関連型と言われる)。前者の方が一般性の高い系統である。なぜなら、型添字がクラスのパラメタと一致する必要がないからである。一方、後者の方が明確に構造化されたコードにつながりやすく、なんらかの型インスタンスが(もしかすると意図せずに)省略された場合、コンパイラが警告を発する。以下では常に、まず一般的な最上位の形式について議論し、その後で関連型に課せられる追加の制約を扱う。

データ族宣言

添字付けされたデータ族は次のようなシグネチャによって導入される。

data family GMap k :: * -> *

この特別なfamilyが、族を標準的なデータ宣言から区別する。結果の類注釈は省略可能であり、省かれた場合は通常同様に*が使われる。例を示す。

data family Array e

名前の付いた引数にも必要なら明示的な類シグネチャを与えることができる。[http://www.haskell.org/ghc/docs/latest/html/users_guide/gadt.html GADT宣言]の場合と同様、名前付き引数は完全に省略可能なので、Arrayを次のように宣言することもできる。

data family Array :: * -> *
関連データ族宣言

データ族が型クラスの一部として宣言される場合、特別子familyは使わない。GMapの宣言は次のような形をとる。

class GMapKey k where
  data GMap k :: * -> *
  ...

最上位の宣言とは対照的に、型添字として使われる予定の全ての型パラメタについて、名前付き引数が用いられねばならない。さらに、それらの引数名はクラスのパラメタでなければならない。それぞれのクラスパラメタは一つの関連型につき一回しか使えないが、使われないクラスパラメタがあってもよく、順序はクラス頭部と異っていてもよい。従って、以下の人為的な例は正当である。

  class C a b c where
  data T c a :: *

データインスタンス宣言

データとnewtypeの族についてのインスタンス宣言は、通常のデータおよびnewtypeの宣言と良く似ている。違いが二つだけあって、dataあるいはnewtypeキーワードの後にinstanceが書かれることと、型引数の一部または全てが変数でない型であってもよいということである。ただし、これにforall型や型シノニム族が含まれていてはいけない。しかし、一般にデータ族が型パラメタ中にあってもよく、型シノニムも、それが完全に適用されていて、しかも展開結果が合法であるなら、認められる。これはクラスインスタンスのパラメタにおいて型シノニムが現れてよい条件と全く同じである。例として、GMapEitherインスタンスは次のようになる。

data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)

この例では、宣言にただ一つのvariantしかないが、一般にはいくつあってもよい(訳注: データ構築子が複数あってもいいということ?)。

データインスタンス宣言およびnewtypeインスタンス宣言は適切な族宣言がスコープにある場合のみ認められる。これはちょうど、クラスインスタンス宣言にクラス宣言が可視であることが必要なのと同じである。さらに、各インスタンス宣言は、その族宣言によって決まる類に準拠していなければならない。つまり、インスタンス宣言のパラメタの個数は、その族の類から決まるアリティと一致するということである。

データ族インスタンス宣言は、通常のdatanewtype宣言が持つ表現力を完全に利用できる。

  • データ族は「data」キーワードを使って導入されるが、族のインスタンスdataであってもnewtypeであってもよく、両者の混合であってもよい。例を示す。

    data family T a
    data    instance T Int  = T1 Int | T2 Bool
    newtype instance T Char = TC Bool
    
  • data instanceはデータ構築子にGADT構文を使うことができ、また実際にGADTを定義することができる。例。

    data family G a b
    data instance G [a] b where
       G1 :: c -> G [Int] b
       G2 :: G [a] Bool
    
  • data instancenewtype instance宣言にderiving節を使うことができる。

型族が最上位の宣言によって定義されている場合でも、異なる族インスタンスに対して異なる計算を行う関数は相変らず型クラスのメソッドとして定義されねばならないことがある。特に、以下は不可能である。

data family T a
data instance T Int  = A
data instance T Char = B
foo :: T a -> Int
foo A = 1             -- 間違い: この二つの等式をいっしょにすると...
foo B = 2             -- ...型エラーが発生する

代わりに、fooをクラスの演算として書かなければならないだろう。

class C a where 
  foo :: T a -> Int
instance Foo Int where
  foo A = 1
instance Foo Char where
  foo B = 2

(GADT(一般化代数的データ型)の提供する機能を見ると、上のような定義が可能であるべきだと思えるかもしれない。しかし、型族は、GADTとは対照的に、開かれている。つまり、常に新しいインスタンスを加えることが可能な(しかも別モジュールでかもしれない)のである。異なるデータインスタンスに跨がるパターン照合に対応するには、一種の拡張可能なcase構造が必要になることだろう。)

関連データインスタンス

関連データ族インスタンスが型クラスインスタンスの中で宣言される場合、族インスタンスにおけるinstanceキーワードは使わない。そのため、GMapEitherインスタンスは次のようになる。

instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
  data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
  ...

関連族インスタンスに関して最も重要な点は、クラスパラメタに対応する型添字が、インスタンス頭部で与えられる型と同一でなければならないということである。この例ではこれはGMapの第一引数であるEither a bであるが、これは(一つしかない)クラスパラメタと同じになっている。族構築子の引数のうち、クラスパラメタに対応しないものは、すべてのインスタンスにおいて変数でなければならない。ここではこれは変数vである。

関連族のインスタンスは、その族が宣言されたクラスのインスタンス宣言の一部としてしか、現れることができない。これはクラスのメソッドの等式についてと同じである。また、これもメソッドの扱いと対応するが、クラスインスタンスにおいて関連型の宣言を省略することができる。関連族インスタンスが省略された場合、それに対応するインスタンス型は無内容(not inhabited)になる。すなわち、undefinedなどの発散する式のみがその型を持てる。

クラスパラメタのスコープ規則

多引数の型クラスの場合、クラスパラメタが関連族インスタンスの右辺から可視かどうかは、そのデータ族のパラメタによってのみ決まる。例として、次の単純なクラス宣言を考える。

class C a b where
  data T a

二つのクラスパラメタのうち一つだけがデータ族のパラメタになっている。このため、次のインスタンス宣言は不正である。

instance C [c] d where
  data T [c] = MkT (c, d)    -- 間違ってるよ!!  「d」はスコープにない

ここでは、データインスタンスの左辺に現れない型変数dが右辺で言及されている。このようなデータインスタンスを認めると型安全性を犠牲にすることになるので、これは認められていない。

族インスタンスについての型クラスインスタンス

データ族のインスタンスについての型クラスインスタンスは通常と同じように定義できる。特に、データインスタンス宣言はderiving節を持つことができる。例えば、以下のように書くことができる。

data GMap () v = GMapUnit (Maybe v)
               deriving Show

これは、以下のような形のインスタンスを暗黙に定義する。

instance Show v => Show (GMap () v) where ...

クラスインスタンスは常にデータ族の特定のインスタンスを対象にするのであって、族全体を対象にするのではないことに注意。この理由は、本質的には、一つの型族の異なるインスタンスのデータ構築子についてパターン照合を行う最上位の関数を定義できない理由と同じである。これには、一種の拡張可能なcase構造が必要になるだろう。

データインスタンスの重複

一つのプログラムの中で、あるデータ族のインスタンス宣言に少しでも重複部分があってはならない。このことは関連族であるかそうでないかによらない。型クラスのインスタンスの場合と異なり、これは単なる整合性の問題ではなく、型安全性の問題である。

インポートとエクスポート

型族とデータ構築子の関連は、通常のデータ型やnewtypeの宣言の場合と比べて動的である。通常の場合、インポートリストやエクスポートリストにおけるT(..)という記法は、その型構築子と、その宣言で導入された全てのデータ構築子を記述するものである。一方、族宣言はデータ構築子を導入することがない。代わりにデータ構築子は族インスタンスによって導入される。結果として、ある型族にどのデータ構築子が関連しているかは、その族についてのインスタンス宣言として今どれが可視であるかに依存する。従って、T(..)という形のインポート/エクスポート項目は、その族構築子と、それのデータ構築子のうちで現在可視であるもの全てを表す。エクスポート項目の場合、これにはそのモジュールにインポートされたものも、そのモジュールで定義されたものも含まれる。GMap(GMapEither)のように、データ構築子を明示的に列挙したエクスポート/インポート項目の扱いも同様である。

関連族

期待される通り、C(..)という形式のインポート/エクスポート項目は、そのクラスのメソッドと関連型全てを示す。しかし、クラス項目の中の項目として関連型が明示的に列挙される場合、なんらかの新しい構文が必要になる。なぜなら、クラス項目の中に出現する大文字の項目は通常データ構築子であって型構築子ではないからである。ここでは、型を示しているということを明確にするために、個々の関連型の名前の前にtypeを置く必要がある。よって、例えば、GMapKeyクラスの内容を明示的に列挙する場合、GMapKey(type GMap, empty, lookup, insert)と書く。

ここまで使ってきたGMapKeyクラスの例を使って、エクスポートリストとその意味をいくつか見てみよう。

  • module GMap (GMapKey) where...: クラス名だけをエクスポートする。

  • module GMap (GMapKey(..)) where...: クラスと、関連型GMapと、メンバ関数emptylookupinsertをエクスポートする。データ構築子は全くエクスポートされない。

  • module GMap (GMapKey(..), GMap(..)) where...: 上と同じだが、データ構築子GMapIntGMapCharGMapUnitGMapPairGMapUnitをもエクスポートする。

  • module GMap (GMapKey(empty, lookup, insert), GMap(..)) where...: 上と同じ。

  • module GMap (GMapKey, empty, lookup, insert, GMap(..)) where...: 上と同じ。

最後に、GMapKey(type GMap)と書くことで、クラスGMapKeyとその関連型GMapの両方を表すことができる。しかし、GMapKey(type GMap(..))と書くことはできない。つまり、内容指定は入れ子にできないのである。GMapのデータ構築子を指定するなら、GMapを(訳注: GMapKeyとは)別に書かねばならない。

インスタンス

クラスインスタンスと同様に、族インスタンスは暗黙にインポートされる。ただし、これはインスタンスの頭部についてだけで、インスタンスが定義するデータ構築子には適用されない。

シノニム族

型族が出現する方法には二通りの系統がある。(1)最上位で定義されるか、(2)型クラスの内部に出現する(この場合、これは関連型シノニムと言われる)かである。前者の系統は、型添字がクラスパラメタと一致しなければならないという制限がないので、より一般性が高い。一方、後者の方が明確に構造化されたコードにつながりやすく、なんらかの型インスタンスが(もしかしたら意図せず)省略された場合、コンパイラが警告を発する。以下では常に、まず一般的な最上位の形式について議論し、その後で関連型に課せられる追加の制約を扱う。

型族宣言

添字付けされた型族は次のようなシグネチャによって導入される。

type family Elem c :: *

この特別なfamilyによって、通常の型宣言と族宣言が区別される。結果の類注釈は省略可能であり、通常と同様に、省略された場合は*が使われる。例えば次のようになる。

type family Elem c

必要ならパラメタにも明示的な類シグネチャを付けることができる。型族宣言におけるパラメタの数をその族のアリティと呼び、その型族の適用は全てそのアリティに対して完全に飽和していなければ(訳注: つまり部分適用であっては)ならない。この制限は通常の型シノニムにはないものである。これにより、型族の類を知っただけではその族のアリティを決定できないので、型族の適用が正しいものかどうかも一般的には判断できない。例として、次の宣言を考える。

type family F a b :: * -> *   -- Fの類は全体として見れば * -> * -> * -> *
                              -- しかし、アリティは2である

この宣言のもとで、以下に正しい型と間違った型の例を示す。

F Char [Int]       -- 正 類: * -> *
F Char [Int] Bool  -- 正 類: *
F IO Bool          -- 誤 最初の引数で類が不一致
F Bool             -- 誤 適用が飽和していない
関連型族宣言

型族が型クラスの一部として宣言される場合、family特別子は使わない。Elemの宣言は次のような形になる。

class Collects ce where
  type Elem ce :: *
  ...

型族の引数名はクラスパラメタでなければならない。各クラスパラメタは一つの関連型について一回しか出現してはならないが、一回も出現しないものがあったり、クラスの頭部と異なる順序であっても良い。よって、以下の人為的な例は認められる。

class C a b c where
  type T c a :: *

これらの規則は関連データ族の場合とまったく同じである。

型インスタンス宣言

型族のインスタンス宣言は通常の型シノニム宣言によく似ている。違いは、typeキーワードの後にinstanceが書かれることと、型引数の一部または全部が変数でなくてもよいことの二点だけである。ただし、型引数は、forall型や型シノニム族を含んでいてはならない。一方、一般にデータ族はあってもよく、型シノニムも、完全に適用されており、かつ展開結果が合法であるなら認められる。これらはデータインスタンスの場合と全く同じ制限である。例として、[e]Elemインスタンスは次のようになる。

type instance Elem [e] = e

型族インスタンス宣言は、適切な族宣言がスコープにあるときのみ認められる。これはちょうど、クラスインスタンスにはクラス宣言が可視であることが必要なのと同じである。さらに、個々のインスタンス宣言は、その族宣言によって決まる類に準拠していなければならず、インスタンス宣言の型パラメタの数は族宣言の型パラメタの数と一致していなければならない。最後に、型インスタンスの右辺は単相型でなければ(つまり、forallを含んでいては)ならず、また飽和した通常の(訳注: vanilla; 型シノニム族でない)型シノニムを全て展開した時点で、族シノニム以外のシノニムが残っていてはならない。許される型インスタンスとそうでない型インスタンスの例をいくつか挙げる。

type family F a :: *
type instance F [Int]              = Int         -- OK!
type instance F String             = Char        -- OK!
type instance F (F a)              = a           -- 誤: 型パラメタが型族に言及している
type instance F (forall a. (a, b)) = b           -- 誤: 型パラメタの中にforall型がある
type instance F Float              = forall a.a  -- 誤: 右辺がforall型であってはならない

type family G a b :: * -> *
type instance G Int            = (,)     -- 誤: 引数は二つでないといけない
type instance G Int Char Float = Double  -- 誤: 引数は二つでないといけない
関連型インスタンス宣言

型クラスインスタンスの中で関連族インスタンスを宣言するときは、族インスタンス中にinstanceキーワードを使わない。よって、Elem[e]インスタンスは次のようになる。

instance (Eq (Elem [e])) => Collects ([e]) where
  type Elem [e] = e
  ...

関連族インスタンスに関して最も重要なのは、クラスパラメタに対応する型添字が、インスタンス頭部で与えられたものと同一であることである。これはここでは[e]であり、一つしかないクラスパラメタと一致している。

関連族のインスタンスは、その族が宣言されたクラスについてのインスタンス宣言の一部としてしか現れ得ない。クラスのメソッドの等式とちょうど同じである。また、同じくメソッドの扱いに対応することとして、クラスインスタンス中での関連型の宣言を省くことができる。関連型族インスタンスが省かれた場合、対応するインスタンス型は無内容(not inhabited)になる。すなわち、undefinedのような発散する式以外に、その型を持てる式は存在しない。

型シノニムインスタンスの重複

ある一つのプログラム内で使われる型族のインスタンス宣言に関して、重複が許されるのは、重複するインスタンスの右辺が共通部分の型に対しては一致する場合だけである。より形式的に言うと、二つのインスタンス宣言が重複するとは、インスタンスの左辺を構文的に一致させるような代入(substitution)が存在するときである。これに該当する場合は必ず、この同じ代入のもとでインスタンスの右辺も構文的に同じにならなければならない。この条件は族が関連族であるかどうかに拠らない。また、これは単なる整合性の問題ではなく、型安全性の問題である。

重複が許される条件を説明するために二つの例を用意した。

type instance F (a, Int) = [a]
type instance F (Int, b) = [b]   -- 重複が許される

type instance G (a, Int)  = [a]
type instance G (Char, a) = [a]  -- 非合法な重複、[Char] /= [Int]であるため
型シノニムインスタンスの決定可能性

型族の存在下での型推論が決定可能であることを保証するため、型インスタンス宣言の形式に追加で制限を課す必要がある。(“Type Checking with Open Type Functions”のDefinition 5 (Relaxed Condition)も参照)。インスタンス宣言の一般形式は次の通りである。

type instance F t1 .. tn = t

ここで、t中のすべての型族適用(G s1 .. sm)に対して、以下のことを要求する。

  1. s1 .. smに、型族構築子が一つも含まれない。

  2. s1 .. sm中のシンボル(データ型構築子および型変数)の数が、t1 .. tnにおける数よりも厳密に小さい。

  3. 全ての型変数aについて、aがs1 .. smに現れる回数が、t1 .. tnに現れる回数を超えない。

これらの制限は容易に検査することができ、型インスタンスが停止することを保証する。しかし、a ~ [F a]のように、型構築子が族適用とデータ構築子適用の下にある、いわゆる「ループ的同値」の存在下では、型推論の完全性を保証するのに足りない。詳細については上で挙げた論文を参照のこと。

-XUndecidableInstancesオプションがコンパイラに渡されると、上記の制約は強制されず、型推論中に型族の正規化が停止することを保証するのはプログラマの責任になる。

同値性制約

型文脈にはt1 ~ t2という形の同値性制約を含めることができる。これは、t1t2の二つの型が同じでなければならないということを示す。型族の存在下では、一般に二つの型が等しいかどうかを局所的に決めることは出来ない。このため、次の例のように、関数のシグネチャの文脈に同値性制約が使われることがある。

sumCollects :: (Collects c1, Collects c2, Elem c1 ~ Elem c2) => c1 -> c2 -> c2

ここでは、c1c2の要素の型が同じであることを要求している。一般に、同値性制約におけるt1t2は任意の単相型であってよい。単相型であるというのは、ランクの高い型が有効になっているかどうかにかかわらず、量化子を含んでいてはならないということである。

同値性制約は、クラスとインスタンスの文脈でも使うことができる。前者によって、関数従属を使うプログラムから、代わりに族シノニムを使うプログラムへの、単純な翻訳が出来るようになる。一般的な考え方として、次のような形のクラス宣言があったとする。

class C a b | a -> b

これを、以下のように書き換える。

class (F a ~ b) => C a b where
  type F a

つまり、すべてのa1 .. an -> bという関数従属性(FD)について、これをF a1 .. anというFD型族とF a1 .. an ~ bというスーパークラス文脈の同値性で表現することで、実質的に関数従属性に名前を与えている。クラスインスタンスでは、FD族の型インスタンスをクラス頭部に沿った形で定義する。この過程でメソッドのシグネチャは影響を受けない。

注意: スーパークラス文脈における同値性はGHC 6.10では完全には実装されていない。

型族とインスタンス宣言

型族のもとでは、インスタンス頭部の形式についての規則(7.6.3.1. インスタンス頭部に関する規則の緩和で与えられている)を拡張する必要がある。特に、

  • データ型族はインスタンス頭部に現れてもよい

  • 型シノニム族はインスタンス頭部に(全く)現われてはいけない

後者の制約があるのは、これを検査する方法がないからである。次の例を考えよ。

   type family F a
   type instance F Bool = Int

   class C a

   instance C Int
   instance C (F a)

ここで、(C (F Bool))という制約は両方のインスタンスに適合する。F Boolの型インスタンスは別のモジュールにあるかもしれず、さらにはまだ書かれていないモジュールにあることさえあり得るので、この状況は特にまずい。