型族
型族
TypeFamilies
MonoLocalBinds, KindSignatures, ExplicitNamespaces拡張を含む
6.8.1以降
添字付き型とデータ族の使用と定義を許可する.
添字付き型族は,型レベルのプログラミングを容易にするための拡張を形成する.型族は関連データ型AssocDataTypes2005と関連型シノニム AssocTypeSyn2005を一般化したものでる.型族自体はSchrijvers 2008 TypeFamilies 2008 で説明されている.型族は基本的に型添字付きデータ型と型に関する名前付き関数を提供する.これはジェネリックプログラミングや高度にパラメータ化されたライブラリインタフェース,さらには依存型と同様に,インターフェースにより多くの静的な情報を与えるのに役立つ.それらはまた,関数従属に代わるものと見なされるかもしれないが,関数従属のリレーショナルなスタイルよりもより関数的な型レベルプログラミングのスタイルを提供する. 添字付き型族,または略して型族は,型の集合を表す型コンストラクタである.集合の要素は,型添字と呼ばれる型パラメータを型族コンストラクタへ与えることによって表される.通常のパラメータ化された型コンストラクタと型族コンストラクタの違いは,パラメトリック多相関数と(アドホック多相)型クラスのメソッドの間の違いによく似ている.パラメトリック多相関数はすべての型インスタンスで同じように動作するが,クラスメソッドはクラス型パラメータに応じて振る舞いを変えることができる.同様に,通常の型コンストラクタは,すべての型に対して同じデータ表現を示すが,型族コンストラクタは,異なる型インデックスに対して異なる表現型を持つことができる.
添字付き型族には,データ族,開いた型シノニム族,閉じた型シノニム族の3つの種類がある.それらは,それぞれ代数データ型および型シノニムの添字付き族の亜種である.データ族のインスタンスは,データ型とnewtypeになる.
AssocDataTypes2005 “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. AssocTypeSyn2005 “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. TypeFamilies2008 “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. データ族
データ族には2つの種類がある.(1)トップレベルで定義できるか,(2)型クラスの中にある(この場合,それらは関連型と呼ばれる).前者はより一般的だ.なぜならそれは型インデックスがクラスパラメータと一致するという要件を欠いているからである.しかし,後者は,いくつかの型インスタンスが(場合によっては,間違って)省略された場合,より明確に構造化されたコードとコンパイラの警告につながる可能性がある.以下では,最初に一般的なトップレベルの形式について最初に説明し,次に関連型に課される追加の制約について説明する.
データ族宣言
添字付きデータ族は,次のようにシグネチャによって導入される.
code: tf1.hs
data family GMap k :: Type -> Type
familyキーワードは,族を標準のデータ宣言と区別する.結果の種注釈はオプションであり,いつもどおり,省略した場合はデフォルトでTypeになる.例えば,
code: tf2.hs
data family Array e
必要に応じて,名前付き引数に明示的な種シグネチャを付けることもできる.GADT宣言と同様に,名前付き引数は完全にオプションであるため,代わりに次のようにArrayを宣言することができる.
code: tf3.hs
data family Array :: Type -> Type
通常のデータ定義とは異なり,データ族の結果の種は必ずしもTypeである必要はない.代わりに(PolyKindsを使用して)種変数にすることもできる.ただし,データインスタンスの種はTypeで終わらなければない.
データインスタンス宣言
dataとnewtype族のインスタンス宣言は,標準のdataとnewtype宣言と非常によく似ている.二つだけ違うことは,キーワードdataまたはnewtypeの後にinstanceが続くこと,および型引数の一部または全部が変数でない型でもよいが,forall型または型シノニム族であってはならないことである.ただし,一般にデータ族は型引数の中にあっても良い.また,型シノニムも完全に適用され,合法な型に展開される限り型引数の中に現れても良い.これはクラスインスタンスのパラメータに型シノニムの出現が許可される条件と同じである.たとえば ,GMapのEitherインスタンス次のようになる.
code: tf4.hs
-- 訳注:v is non-variable type
data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
この例では,宣言には1つのヴァリアント(GMapEither)しかないが,一般的には,いくつあっても良い.
-Wunused-type-patternsフラグが有効になっていると,左辺で宣言されているが右辺で使用されていない型変数が報告される.左辺に複数回現れる変数も使用されていると見なされる.警告を表示しないようにするには,未使用の変数をアンダースコアで置換するか,アンダースコアを前に付ければよい.それ以外の場合,アンダースコア(例えば_x)で始まる型変数は通常の型変数として扱われる.
これは,部分的型シノニムで使用できるワイルドカードに似ている.ただし,いくつか違いがある.推論された型を報告するエラーメッセージは生成されず,PartialTypeSignatures拡張の影響もない.
dataとnewtypeのインスタンス宣言は,適切な族宣言がスコープ内にある場合にのみ許可される.ちょうどクラスインスタンス宣言がクラス宣言が可視であることを要求するのと同様である.さらに,各インスタンス宣言は,その族宣言によって決定される種に準拠する必要がある.つまり,インスタンス宣言のパラメータの数が族の種によって決まるアリティと一致するということである.
データ族のインスタンス宣言は,通常のdataまたはnewtype宣言の持つ表現力を完全に使用できる.
データ族はキーワード「data」で導入されているが,データ族インスタンスはdataまたはnewtypeのどちらも使用でき,両者の混合であっても良い.例えば,
code: ts5.hs
data family T a
data instance T Int = T1 Int | T2 Bool
newtype instance T Char = TC Bool
データ族のインスタンスは,データコンストラクタのためのGADT構文を使用することができ,実際GADTを定義することができる.例えば,
code: ts6.hs
data family G a b
data instance G a b where dataのインスタンス宣言またはnewtypeのインスタンス宣言にderiving句を使用できる.
データ族がトップレベルの宣言として定義されている場合でも,族インスタンスごとに異なる計算を実行する関数は,型クラスのメソッドとして定義する必要がある.特に,次は不可能である.
code: ts7.hs
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を書く必要があるだろう.
code:tf8.hs
class Foo a where
foo :: T a -> Int
instance Foo Int where
foo A = 1
instance Foo Char where
foo B = 2
GADT(一般化された代数データ型)によって提供される機能を考えると,上記(ts7.hs)のような定義が実行可能であるべきであると思うかも知れない.ただし,GADTとは対照的に,型族は開かれている.つまり,新しいインスタンスはいつでも追加できるし,他のモジュールでも追加される可能性がある.異なるデータインスタンスにわたるパターンマッチングをサポートするには,拡張可能なcase構造の形式が必要になる.
データインスタンスの重複
単一のプログラムで使用されるデータ族のインスタンス宣言は,それらが関連型か否かにかかわらず,まったく重複してはならない.型クラスのインスタンスとは対照的に,これは一貫性の問題だけでなく,型安全の問題だ.
シノニム族
型族には3つの種類がある.(1)トップレベルでは開いた族として定義できる.(2)トップレベルでは閉じた族として定義できる.(3)型クラスの中に配置できる(この場合,関連型シノニムとして知られている).トップレベルの型族は,型インデックスがクラスパラメータと一致する必要がないため,より一般的である.しかし,関連型シノニムは,型インスタンスが(ことによると誤って)省略された場合,より明確に構造化されたコードとコンパイラの警告につながる可能性がある.以下では,最初に一般的なトップレベルの形式について説明し,次に関連型に課される追加の制約について説明する.なお,閉じた関連型シノニムは存在しない.
型族の宣言
開いた添字付き型族は,次のようなシグネチャによって導入される.
code: tf9.hs
type family Elem c :: Type
キーワードfamilyは,族を標準の型宣言と区別する.結果の種の注釈はオプションであり,いつもどおり,省略した場合はデフォルトでTypeになる.例えば,
code: tf10.hs
type family Elem c
必要ならば,パラメータに明示的な種シグネチャを与えることもできる.型族宣言の中のパラメータの数をその族のアリティと呼び,その型族のすべての適用はそのアリティに関して完全に飽和していなければない(訳注:完全適用である必要があるということ).この要件は通常の型シノニムとは異なり,型族の種を知っただけでは情報が不十分でその族のアリティを決められないため,一般には型族適用が正しい形式を持つ(well-fromed)(訳注:この訳は型システム入門による)かどうかも判断できない.例として,次の宣言を考えよう.
code: tf11.hs
type family F a b :: Type -> Type
-- F's arity is 2,
-- although its overall kind is Type -> Type -> Type -> Type
この宣言が与えられたとき,以下は適切な形式と不正な形式の例である.
code: tf12.hs
F Char Int -- OK! Kind: Type -> Type F Char Int Bool -- OK! Kind: Type F IO Bool -- WRONG: kind mismatch in the first argument
F Bool -- WRONG: unsaturated application
結果の種の注釈はオプションであり,省略した場合はデフォルトでTypeになる(引数の種類と同様である).種多相な型族は,種注釈のパラメータを使用して宣言できる.
code: tf13.hs
type family F a :: k
この場合,種別パラメータkは,実際には型族の暗黙のパラメータである.
型インスタンス宣言
型族のインスタンス宣言は,標準の型シノニム宣言と非常によく似ている.唯一の2つの違いは,キーワードのtypeの後にinstanceが続くこと,型引数の一部または全部が変数でない型でも良いが,forall型または型シノニム族を含んではならないことである.ただし,一般にデータ族は型引数の中にあってもよく,型シノニムは完全に適用され,合法な型に展開される限り型引数の中にあらわれても良い.これらはデータインスタンスの場合とまったく同じ制限である.たとえば,Elemの[e]インスタンスは
code: tf14.hs
引数の名前が関係ない場合は,型引数をアンダースコア(_)に置き換えることができる.これは一意な名前で型変数を書くのと同じである.未使用の型引数は,-Wunused-type-patternsフラグが有効になっている場合の警告を回避するために,アンダースコアで置き換えたり前に付けることができる.つまり,データインスタンス宣言と同じ規則が適用される.
型族インスタンス宣言は,適切な族宣言が有効範囲内にある場合にのみ正当である. これは,クラスインスタンスがクラス宣言が可視であることを要求するのと同様である.さらに,各インスタンス宣言は,その族宣言によって決定された種に準拠する必要があり,インスタンス宣言内の型パラメータの数は,族宣言内の型パラメータの数と一致しなければならない.最後に,型インスタンスの右側は単型(monotype)でなければならず,(つまり,forallを含んではならない),すべての飽和した通常の型シノニムの展開後,族シノニム以外のシノニムは残らないかもしれない.
閉型族
型族はwhere節で宣言することもでき,その場合,その型族の等式を全て定義する.例えば,
code: tf15.hs
type family F a where
F Int = Double
F Bool = Char
F a = String
閉じた型族の適用を単純化(訳注:simplifyingの訳:ここでの意味は型族Fに具体的な型を与えたときに対応する型へ変換をすることを言っている)するときは,上から下に向かって順に閉じた型族の等式を試す.この例では,我々は,F intをDoubleに,F BoolをCharに,IntでもBoolでもない他の任意の型aをStringに単純化するように,Fのインスタンスを宣言している. 最後の場合,GHCはaがIntまたはBoolへ単純化できないことを確認できなければならない.プログラマがコードの中で,単にF aだけを指定した場合,GHCは型を単純化することができないだろう.後でaがIntにインスタンス化されるかもしれないからである.
閉じた型族の等式には,開いた型族のインスタンスの等式と同等の制限がある.
閉じた型族は等式部分なしで宣言することができる.そのような閉じた型族は,決して縮小されないであろう不明瞭な型レベルの定義であり,(空のデータ型とは違って)必ずしも単射ではなく,どのようなインスタンスも与えることもできない.これは,hsファイルで与えられた等式がある場合とない場合があるので,(構文where ..を使用する)hs-bootファイルで閉じた型族の等式を省略するのとは異なる話である.
型族の例
許される型インスタンスとそうでない型インスタンスの例をいくつか挙げる.
code: tf16.hs
type family F a :: Type
type instance F Int = Int -- OK! type instance F String = Char -- OK!
type instance F (F a) = a -- WRONG: type parameter mentions a type family
type instance
F (forall a. (a, b)) = b -- WRONG: a forall type appears in a type parameter
type instance
F Float = forall a.a -- WRONG: right-hand side may not be a forall type
type family H a where -- OK!
H Int = Int
H Bool = Bool
H a = String
type instance H Char = Char -- WRONG: cannot have instances of closed family
type family K a where -- OK!
type family G a b :: Type -> Type
type instance G Int = (,) -- WRONG: must be two type parameters
type instance G Int Char Float = Double -- WRONG: must be two type parameters
型族の等式間の互換性と分離性
曖昧な書き換え系を定義しないように,型族の方程式にはいくつかの制限がなければならない.そのため,開いた型族の等式は互換性を要求される.2つの型パターンは,以下が成り立つなら,互換性を持つ.
パターン内のすべての対応する型と暗黙の種が分離的である(apart).
2つのパターンの単一化(unification)により代入を作り,右辺はその代入の下で等しい.
(訳注:ここでの単一化(unification)とは,2つの型を等しくする最も小さな代入を見つけること)
(訳注:ここでの代入(subsitution)とは型代入のことで,型変数から型への写像である)
2つの型が分離的であるとみなされるのは,すべての可能な代入に関して,型が同じ簡約結果にならない場合である.
「互換性がある」の最初の条件はより明快なものだ.それは,2つの異なる型族のインスタンスのパターンが重複してはならないということを言っている.たとえば,以下は許されない.
code: tf17.hs
type instance F Int = Bool
type instance F Int = Char
2番目の条件はもう少しおもしろい.それは,重複する領域で右辺が一致するなら,2つの重複する型族のインスタンスは許されるということだ.例えば,
code: tf18.hs
type instance F (a, Int) = a type instance F (Int, b) = b -- overlap permitted type instance G (a, Int) = a type instance G (Char, a) = a -- ILLEGAL overlap, as Char /= Int この互換性条件は,型族が関連型であるか否かにかかわらず,一貫性の問題だけでなく型安全の問題でもあることに注意せよ.
種多相な型族の場合,種は型と同じように分離性がチェックされる.例えば,以下のものは許される.
code: tf19.hs
type family J a :: k
type instance J Int = Bool
type instance J Int = Maybe
これらのインスタンスは,暗黙の種パラメータが異なるので互換性がある.具体的に言うと,最初のインスタスのkはTypeであり,2番目のkはType - > Typeである.
「互換性」の定義は「分離性」の概念を利用し,「分離性」の定義は今度は型族の簡約に依存している.前述のように,この「分離性」の条件は検査できないので,「2つの型が潜在的に無限の単一化子によってさえ単一化できないとき,この2つの型が分離的であるとみなす」という保守的な近似を使用する.単一化子が無限であることを許すと,次の2つのインスタンスは許されなくなる.
(訳注:単一化子(unifier)は型システムの文脈(もっと言えばHM推論の文脈)のものである.詳しくは型システムの教科書を参照せよ)
code: tf20.hs
type instance H x x = Int
type instance H x x = Bool この2つの型パターンは,xをリストの無限の入れ子に置き換えれば,同等だ.このようなインスタンスを棄却することは,型の健全性を維持するために必要である.
互換性は閉じた型族にも影響する.閉じた型族の適用を単純化するとき,GHCは互換性のない前の等式が決して適用されないことが確実であるときだけ式を選択する.ここではいくつかの例を示す.
code: tf21.hs
type family F a where
F Int = Bool
F a = Char
type family G a where
G Int = Int
G a = a
Fの定義では,2つの等式は両立しない.なぜなら,2つのパターンは分離されておらず,しかもそれらの右辺は一致しないからである.したがって,GHCが2番目の式を選択する前に,最初の式が適用できないことを確認する必要がある.よって,型F aは単純化されない.F Doubleのような型だけがCharに単純化される.一方,Gの2つの等式は互換性がある.したがって,GHCは2番目の式を見たときに最初の式を無視することができる.したがって,G aはaに単純化される.
型シノニムインスタンスの決定可能性
UndecidableInstances
型シノニム族のインスタンスの決定可能性に対する制限を緩和する.
型族の存在下での型推論が決定可能であることを保証するために,型インスタンス宣言の形式にいくつかの追加の制限を加える必要がある(c.f. 「開いた型関数による型検査」の定義5(緩和条件)も参照せよ).インスタンス宣言の一般的な形式は次のとおりである.
code: tf22.hs
type instance F t1 .. tn = t
ここで,t中のすべての型族適用(G s1 .. sm)に対して,以下のことを要求する.
s1 .. smは型族コンストラクタを一つも含まない.
s1 .. sm内のシンボル(データ型コンストラクタと型変数)の総数は,t1 .. tnよりも厳密に少ない.
すべての型変数aについて,aがs1 .. smで登場する回数がt1 .. tnで登場する回数を超えない.
これらの制限は簡単に検査することができ,型推論の終了を確実にする.しかし,a ~ [F a]のような,型変数の再帰的発生が族適用と値コンストラクタ適用のすぐ下にある,いわゆる「ループ同値性」("loopy equalities")のもとでの型推論の完全性を保証するのにはこの制限では足りない.
UndecidableInstances拡張下では,上記の制限は適用されず,型推論中に型族の正規化を確実に終了させることは,プログラマの責任になる.
データと型族のインスタンスの左辺のワイルドカード
データ型宣言または型インスタンス宣言の型引数の名前が重要でない場合は,アンダースコア(_)に置き換えることができる.これは,一意の名前で型変数を書くのと同じである.
code: tf23.hs
data family F a b :: Type
data instance F Int _ = Int
-- Equivalent to data instance F Int b = Int
type family T a :: Type
type instance T (a,_) = a
-- Equivalent to type instance T (a,b) = a
型パターンでのワイルドカードでのアンダースコアの使用は,項言語(訳注:値レベルでのという意味の模様?)でのパターンマッチングとまったく同じだが,部分的型シグネチャのでのアンダースコアの使用とはかなり違う(Type Wildcardsを参照).
アンダースコアで始まる型変数は,型またはデータインスタンス宣言では特別に扱われない.例えば,
code: tf24.hs
data instance F Bool _a = _a -> Int
-- Equivalent to data instance F Bool a = a -> Int
これは,型シグネチャ内の名前付きワイルドカード(名前付きワイルドカードを参照せよ)の特別な扱いとは対照的である.
関連型と型族
データまたは型シノニム族は,型クラスの一部として宣言できる.
code: tf25.hs
class GMapKey k where
data GMap k :: Type -> Type
...
class Collects ce where
type Elem ce :: Type
...
この場合,(任意に)familyキーワードを削除してもよい.
型パラメータはすべて型変数である必要があり,そのうちいくつか(必ずしもすべてではないが)がクラスパラメータになっても良い.各クラスパラメータは,関連型ごとに高々1回しか使ってはならないが,使われないものがあっても良いし,クラス宣言の先頭と違う順序にすることもできる.したがって,次のようなわざとらしい例は認められる.
code:tf26.hs
class C a b c where
type T c a x :: Type
ここでcとaはクラスパラメータだが,型は第三のパラメータxでも添字付けされている.
関連型のインスタンス
関連データ族または関連型シノニム族のインスタンスが型クラスのインスタンス内で宣言されている場合,(オプションで) 族のインスンタンスのinstanceキーワードを削除してもよい.
code:tf27.hs
instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
...
instance Eq (Elem e) => Collects e where ...
関連型のデータ族または型族のインスタンスは,クラスパラメータに対応する型添字がインスタンス宣言の先頭で指定された型とまったく同じでなければならないという規則に従う必要がある.例えば,
code:tf28.hs
class Collects ce where
type Elem ce :: Type
instance Eq (Elem e) => Collects e where -- Choose one of the following alternatives:
type Elem x = x -- BAD; 'x' is different to 'e' from head type Elem x = x -- BAD; 'x' is different to 'e' 次の点に注意せよ.
関連族のインスタンスは,クラスのメソッドと同様に,そのクラスが宣言されたクラスのインスタンス宣言の一部としての登場する.
型族の等式の右辺の型変数は,通常どおり,左辺で明示的に束縛されなければなない.しかし,右辺では暗黙的に束縛されている種変数について言及することが許可されているため,この制限は種変数では緩和される.たとえば,これらは合法である.
code:tf29.hs
data family Nat :: k -> k -> Type
-- k is implicitly bound by an invisible kind pattern
newtype instance Nat :: (k -> Type) -> (k -> Type) -> Type where
Nat :: (forall xx. f xx -> g xx) -> Nat f g
class Funct f where
type Codomain f :: Type
instance Funct ('KProxy :: KProxy o) where
-- o is implicitly bound by the kind signature
-- of the LHS type pattern ('KProxy)
type Codomain 'KProxy = NatTr (Proxy :: o -> Type)
関連型のインスタンスは,クラスインスタンスでは省略できる.その場合,デフォルトのインスタンスがない限り(関連タイプの同義語のデフォルトを参照 ),対応するインスタンスの型はuninhabitedである(値が内在しない).つまり,undefinedなどの,発散する式だけがこの型を取ることができる.
不自然だが,単一のインスタンス宣言の中に,関連族に対して複数のインスタンスが存在することが(現在は)許されている.たとえば,以下は合法である.
code:tf30.hs
instance GMapKey Flob where
data GMap Flob Int = G2 Int
...
このコードでは,最後のパラメータが[v]であるデータインスタンス宣言とIntであるデータインスタンス宣言の2つを与えている.(GMap Flob ...)にこれ以降にどんなインスタンスも続けて指定することもできないので,この機能は,自由に添字付けられたパラメータの種が(Typeとは異なり)有限個の選択肢を持つ場合に最も便利だ.
(訳注:tf30.hsではType -> Typeの種を持つ[v]と,Typeの種を持つIntの2つの種を持つパラメータをとるデータ族となっている.)
関連型シノニムのデフォルト
関連型を定義するクラスが,関連型インスタンスのデフォルト実装を指定することは可能である.ゆえに,例えば,これは合法だ,
code:tf31.hs
class IsBoolMap v where
type Key v
type instance Key v = Int
lookupKey :: Key v -> v -> Maybe Bool
lookupKey = lookup
型クラスのinstance宣言の中で,明示的なtype instance宣言が関連型について全く与えられていなければ,デフォルトの宣言が代わりに用いられる.これは型クラスのメソッドのデフォルト実装と同様である.
次の点に注意せよ.
キーワードinstanceはなくともよい.
関連型シノニムには,最大1つのデフォルト宣言しか許されない.
デフォルトの宣言は,関連データ型には許可されていない.
デフォルトの宣言では,左辺に型変数のみを記述し,右辺には,左辺で明示的に束縛されている型変数のみを記述する必要がある.ただし,右辺には,暗黙的に左辺で束縛されている種変数を記述できるため,この制限は種変数に対しては緩和されている.
関連型族の宣言自体とは異なり,デフォルトのインスタンスの型変数は親クラスの型変数から独立してる.
以下にいくつかの例を示す.
code:tf32.hs
class C (a :: Type) where
type F1 a :: Type
type instance F1 a = a -- OK type instance F1 a = a -> a -- BAD; only one default instance is allowed
type F2 b a -- OK; note the family has more type
-- variables than the class
type instance F2 c d = c -> d -- OK; you don't have to use 'a' in the type instance
type F3 a
type F3 b = b -- BAD; only type variables allowed on the LHS type F4 a
type F4 b = a -- BAD; 'a' is not in scope in the RHS
type F5 a = ('[] :: x) -- OK; the kind variable x is implicitly -- bound by an invisible kind pattern
-- on the LHS
type F6 a
type F6 a =
Proxy ('[] :: x) -- BAD; the kind variable x is not bound, -- even by an invisible kind pattern
type F7 x = ('[] :: a) -- OK; the kind variable a is implicitly -- bound by the kind signature of the
-- LHS type pattern
クラスパラメータのスコープ
関連族インスタンスの右辺にあるクラスパラメータが見える範囲は,その族のパラメータにのみ依存する.例として,以下の単純なクラス宣言を考えよう.
code:tf33.hs
class C a b where
data T a
2つのクラスパラメータのうちの1つだけがデータ族へのパラメータである.したがって,次のインスタンス宣言は違法である.
code:tf34.hs
data T c = MkT (c, d) -- WRONG!! 'd' is not in scope ここで,データインスタンスの右辺には,左辺には現れない型変数dがある.そのようなデータインスタンスは型安全性を危うくするので,そのようなものを認めることはできない.
関連族インスタンスの右辺には,(PolyKinds拡張を使用することで)種パラメータを含めることも可能であることに留意せよ.たとえば,この型クラスとインスタンスは完全に許容される.
code:tf35.hs
class C k where
type T :: k
instance C (Maybe a) where
type T = (Nothing :: Maybe a)
ここで,右辺 (Nothing :: Maybe a) は左辺に登場しない種変数aに言及しているが,これは許容可能である.なぜなら,aはTの種パターンによって暗黙的に束縛されているからである.
次の例に示すように,種変数は左辺の型パターンで暗黙的に束縛することもできる.
code:tf36.hs
class C a where
instance C (Maybe a) where
('[] :: [Maybe a])では,種変数aが左辺の型パターンxの種シグネチャによって暗黙に束縛されている.
インスタンスのコンテキストと関連型とデータインスタンス
関連型とデータインスタンスの宣言は,それに纏わるインスタンスで指定されたコンテキストを継承しない.というのも,型インスタンス宣言の場合,コンテキストがどのような意味になるかが不明になってしまい,データインスタンス宣言の場合,ユーザがすべての値コンストラクタに対してコンテキストを繰り返し書きたいと考えることはまずないからである.コンテキストが役立つ可能性がある唯一の場所は,関連データインスタンスのderiving句内にある.しかしながら,ここでも,外部インスタンス(訳注:outer instances 関連型定義されているモジュールと違うモジュールでされるインスタンス宣言ということ?)のコンテキストの役割は曖昧である.そのため,わかりやすくするために,上記の「(関連型に纏わる)インスタンスのコンテキストは無視される」という規則に従う.派生インスタンスで非自明なコンテキストを使用する必要がある場合は,(トップレベルで)standalone deriving句を使用する.
インポートとエクスポート
エクスポートリストの規則(Haskell Language Report Section 5.2)は型族のために調整する必要がある.
Tはデータ族の名前とすると,T (..)という形式は,Tのデータインスタンスであるコンストラクタの(修飾付きにしろ修飾付きでないにしろ)うちスコープ内のものすべてを表す.
Tをデータ族とすると,T(.., ci, .., fj, ..)という形式は,通常のように,Tと指定されてコンストラクタciとフィールドfjを指名する.コンストラクタ名とフィールド名はTの何らかのデータインスタンスに属する必要があるが,同一のインスタンスに属する必要はない.
Cをクラスとすると,C(..)という形式は,クラスCとその全てのメソッドと関連型を指名する.
Cをクラスとすると,C(.., mi, .., type Tj, ..)という形式は,クラスCと,(指定|規定)されたメソッドmiと関連型Tjを指名する.型には,値コンストラクタと区別するためのキーワードtypeが必要である.
エクスポートリストがなく,データインスタンスが定義されている場合は常に,データ族がローカルで定義されているか別のモジュールで定義されているかに関係なく,対応するデータ族型コンストラクタが新しい値コンストラクタとともにエクスポートされる.
例
(訳注: コンパイルエラーになったりする状態と対比しての)動くGMapKeyクラスの例を思い出してみよう.
code:tf37.hs
class GMapKey k where
data GMap k :: Type -> Type
insert :: GMap k v -> k -> v -> GMap k v
lookup :: GMap k v -> k -> Maybe v
empty :: GMap k v
instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
...method declarations...
エクスポートリストとその意味は次のとおりである.
code:tf38.hs
module GMap( GMapKey )
クラス名のみをエクスポートする.
code:tf39.hs
module GMap( GMapKey(..) )
クラス,関連型GMap,およびメンバ関数 empty,lookup,insertをエクスポートする.GMapの値コンストラクタ(この場合はGMapEither)はエクスポートされない.
code:tf40.hs
module GMap( GMapKey( type GMap, empty, lookup, insert ) )
前の項目と同じである.typeキーワードに注意.
code:tf41.hs
module GMap( GMapKey(..), GMap(..) )
前の項目と同じだが,GMapのすべての値コンストラクタ,つまり GMapEitherもエクスポートする.
code:tf42.hs
module GMap ( GMapKey( empty, lookup, insert), GMap(..) )
前の項目と同じである.
code:tf43.hs
module GMap ( GMapKey, empty, lookup, insert, GMap(..) )
前の項目と同じである.
気をつけるべき2つのこと:
GMapKey(type GMap(..)) と書くことはできない.つまり,サブコンポーネントの指定を入れ子にすることはできない.GMapの値コンストラクタを指定するには,それを個別に列挙する必要がある.
次の例を考えよう.
code: tf44.hs
module X where
data family D
module Y where
import X
data instance D Int = D1 | D2
モジュールYは,Yで定義された全てのエンティティ,すなわち値コンストラクタD1およびD2,をエクスポートするのみならず,暗黙的に データ族Dをもエクスポートする(それがXで定義されているにもかかわらず).つまり ,以下のように明示的なエクスポートリストを指定することなく,import Y( D(D1,D2) ) と書くことができる.
code: tf45.hs
module Y( D(..) ) where ...
or module Y( module Y, D ) where ...
インスタンス
族インスタンスは,クラスインスタンスと同様に,暗黙的にエクスポートされる.ただし,これはインスタンス宣言の先頭にのみ適用され,インスタンスが定義する値コンストラクタには適用されない.
型族とインスタンス宣言
型族を導入したことにより,「インスタンス宣言先頭の制約の緩和」で説明したインスタンス宣言の先頭の形式に対する制約を拡張する必要がある.具体的には,
データ型族はインスタンス宣言の先頭に現れうる.
型シノニム族は,インスタンス宣言の先頭に(まったく)登場しなくともよい.
後者の制約の理由は,インスタンスの決定する方法がないためである.以下の例を考えよう.
code:tf46.hs
type family F a
type instance F Bool = Int
class C a
instance C Int
instance C (F a)
この場合,制約(C (F Bool))は両方のインスタンスにマッチする.F Boolの型インスタンスは他のモジュール,あるいはまだ書かれていないモジュールの中にあるかもしれないので,これは特にマズい状況である.
ただし,データ族のインスタンスの型クラスのインスタンスは,他のデータ型と同じように定義できる.たとえば,
code:tf47.hs
data instance T Int = T1 Int | T2 Bool
instance Eq (T Int) where
(T1 i) == (T1 j) = i==j
(T2 i) == (T2 j) = i==j
_ == _ = False
と書くことができる.
クラスインスタンスは常にデータ族の特定のインスタンスに対するものであり,族全体に対するものでは決してない.これは,単一の型族の異なるインスタンスの値コンストラクタでパターンマッチを実行するトップレベル関数を定義できないのと本質的に同じ理由によるものである.そのような定義がもしできたとしたならば,それは一種の拡張可能なcase構文を(訳注:パターンマッチのために)必要とするだろう.(訳注:しかしそんなものは無いので,できない)
データインスタンス宣言は,deriving句を持つこともできる.例えば,
code:tf48.hs
data GMap () v = GMapUnit (Maybe v)
deriving Show
と書ける.これは以下のようなインスタンスを暗黙に定義する.
code:tf49.hs
instance Show v => Show (GMap () v) where ...
単射性型族
TypeFamilyDependencies
TypeFamilyDependenciesを含む
8.0.1以降
型族に対する関数従属注釈を許可する.これにより,単射型族を定義することができる.
GHC 8.0の型族から始めて,単射性情報を注釈で付けることができる.この情報は,型変数が型族適用の下にのみ現れる状況で型のあいまいさを解決するために型検査中にGHCによって使用される.次のわざとらしい例を考えてみよう.
code:tf50.hs
type family Id a
type instance Id Int = Int
type instance Id Bool = Bool
id :: Id t -> Id t
id x = x
ここでidの定義は拒否される.これは,型変数tが型族の適用の下にしか現れず,したがってあいまいなためである.しかし,このコードは,Idが単射であること(これは,引数の型から呼び出し場所でtを推論することが可能になることを意味する)をGHCに伝えれば受け入れられる.
code:tf51.hs
type family Id a = r | r -> a
単射性型族は,-XTypeFamilyDependencies言語拡張で有効になる.この拡張は-XTypeFamiliesを含む.
単射性注釈の構文
単射性注釈は型族の先頭の後に追加され,2つの部分から構成される.
型族の返り値(訳注:返り"型"な気もするが,意味が通るので返り値を使った)を指す型変数.構文: = tyvarまたは= (tyvar :: kind).型変数はフレッシュでなければない.
| A -> Bという形式の単射性注釈.ここでAは返り値の型変数(前項を参照),Bは単射性型族の種変数と型変数の引数のリストである.型族がそれらの中で単射ではない場合,いくつかの変数を省略することができる.
例:
code:tf52.hs
type family Id a = result | result -> a where
type family F a b c = d | d -> a c b
type family G (a :: k) b c = foo | foo -> k b where
開いた型族と閉じた型族では,結果に名前を付けて単射性注釈を飛ばしても問題ない.単射性注釈なしの結果を示す名前が関連型シノニムのデフォルト実装として解釈されるため,これは関連型シノニムには当てはまらない.
型族の等式の単射性注釈の検証
ユーザが型族を単射であると宣言したら,GHCはこの宣言が正しいこと,つまり型族の等式が単射性注釈に違反しないことを検証しなければない.大まかに言えば,少なくとも1つの等式(下記の箇条書き(1), (2), (3))または一対の等式(下記の箇条書き(4), (5))が単射性注釈に違反する場合,ユーザが主張する方法では型族が単射ではないとして,エラーとすることである.以下の箇条書きの中で,「右辺」は型族の等式の右辺が単射性について検査されていることを示す.「左辺」はその型族の等式の引数を参照する.以下は,型族の単射性を検査するときに従う規則である.
1. 型族の等式の右辺が型族適用である場合,GHCはその型族は単射ではないと報告する.
2. 型族の等式の右辺が裸の型変数である場合,すべての左辺の変数(暗黙の種変数を含む)も裸である必要がある.言い換えれば,これはその型族の唯一の等式でなければならず,それはすべての可能なパターンをカバーしなければない.パターンがカバーしきれていない場合,GHCは型族は単射ではないと報告する.
3. 単射として宣言されている左辺の型変数が右辺の「単射位置」に記載されていない場合,GHCはその型族は単射ではないと報告する.「単射位置」とは,型コンストラクタへの引数,または型族への単射性に関わる引数を意味する.
4. 開いた型族は,段階的に型検査される.つまり,モジュールがインポートされると,そのモジュールに含まれる型族のインスタンスは,すでにインポートされているモジュールに存在するインスタンスに対して検査される.
一対の開いた型族の等式は,それらの右辺を単一化しようとすることによって検査される.右辺が単一化されない場合,このペアは単射性注釈に違反しない.単一化が(型)代入で成功する場合,単一化された等式の左辺はその(型)代入のもとで同一でなければない.それらが同一でなければ,GHCは型族は単射ではないと報告する.
5. 閉じた型族ではすべての等式が順序よく,一箇所にある.等式もペアごとに検査されるが,このとき,等式をすべての前の等式とペアにする必要がある.もちろん,一つの式しかない閉じた型族は自明に単射である(上記の(1), (2), (3)で単射でない場合を除く).
一対の閉じた型族の等式を調べるとき,GHCはそれらの右辺を単一化しようとした.それらが単一化されないのであれば,この一対の等式は単射性注釈に違反しない.もし右辺がある(型)代入のもとで単一化される(空であってもよい)場合,左辺が同じ(型)代入のもとで単一化されるか,後者の式の左辺が先の式によって包含される.どちらの条件も満たされない場合,GHCは型族は単射ではないと報告する.
(4)と(5)の単射性検査の目的のために,GHCは型族が適用可能ならば何でも単一化するように扱う単一化アルゴリズムの特別な変種を使用することに注意せよ.