型クラスの Coherence と Orphan Instance
Posted on 金 20 3月 2020 in プログラミング言語
Haskell には型クラスと呼ばれる重要な機能がある.これは名前の通り,型をクラス分けするための機能で,その型に対してある操作が構成できることをその型の性質とみなし,性質に名前がつけられる機能だ.この機能は,アドホック多相,つまりは型による静的なオーバーロードを実現する仕組みとしての側面もある.型クラスに対しては,型ごとにそのインスタンス,つまり操作の実装を与えることができ,ある型がある型クラスに所属していることを型注釈で表明することができる.その表明は,コンパイラによるインスタンスの自動検索で解決され,解決できなかった場合は型エラーになる.
さて,型クラスの仕組みは coherence という,かなり強い性質を要求する.今回は,この coherence がどういう役割を持つかを,Haskell を例に見ていく.また,orphan インスタンスと呼ばれる特殊なインスタンスと coherence の関係性について言及する.
型クラス
型クラスとは,その名の通り型のクラスのことだ.例えば,ある型 A の全ての要素同士について等価性が判定可能なことは,Haskell では以下のように表明できる:
1 | instance Eq A where ... |
これは,型 A が Eq 型クラスに所属するということを表す.Eq 型クラスは,
1 2 | class Eq a where (==) :: a -> a -> Bool |
のように書け,A が二分木構造を持つデータとすると,上記の表明の完成形は,以下のようになる:
1 2 3 4 5 6 7 8 9 | data A = Leaf | Node A A instance Eq A where (==) = go where go x y = case (x, y) of (Leaf , Leaf ) -> True (Leaf , _ ) -> False (_ , Leaf ) -> False (Node x1 x2, Node y1 y2) -> go x1 y1 && go x2 y2 |
つまり,等価性判定の方法を具体的に与えることで,等価性判定可能であることを保証するわけだ.ところで,この仕組みは,型ごとのオーバーロードと見なすこともできる.Haskell での利用は多くの場合,後者の役割が期待されている場合が多い.上記の例では,様々な型でそれぞれ異なる等価性判定を (==) という同じ名前の演算子で参照できる.例えば,以下のようにだ:
1 2 | f :: Eq a => a -> a -> a -> Bool f x y z = x == y && y == z |
型クラスで導入された操作をメソッドと呼び,メソッドはそれぞれ型制約のついた関数として参照できる.例えば,(==) は,(==) :: Eq a => a -> a -> Bool という型を持つ演算子として参照できる.型制約を持つ型は,その検査の際型制約に関する保証,つまりスコープ内に何らかのインスタンスが必ずあることを求める.f 内での (==) の呼び出しは,f の型制約によって Eq a というインスタンスがあることが保証されるため,問題なく使用できるが,f :: a -> a -> a -> Bool のような型にすると型エラーになる.ただ,保証は呼び出し元の型制約だけによるものではない.例えば,
1 2 | g :: A -> A -> A -> Bool g x y z = x == y && y == z |
と書いた場合,g は特に型制約を必要としない.この場合,A に関するインスタンスがあることから,直接保証が得られる.Haskell の型クラスの仕組みの面白い点は,インスタンスの解決方法と型推論の方法さえ与えられれば,型クラスを持たない言語に elaboration するだけ [1] で実行の意味論を与えられる点だ.この方法は辞書渡しという名前で知られていて,
1 2 3 4 5 6 7 8 | class C a where m1 :: a -> a instance C A where m1 x = x f :: C a => a -> a f = m1 . m1 |
というようなプログラムを,
1 2 3 4 5 6 7 8 9 10 11 | data DictC a = DictC { m1 :: a -> a } instDictC_A :: DictC A instDictC_A = DictC { m1 = \x -> x } f :: DictC a -> a -> a f d = m1 d . m1 d |
というように,型クラスに対応する辞書と呼ばれるデータ型を作り,その型の値を明示的に渡していくことで実現される.GHC では,この elaboration による実行時表現をそのまま採用しており,内部は辞書渡しにより実現されている.
型クラスの Coherence
ところで,Haskell の型クラスのインスタンスには,以下のような制約がある.
A type may not be declared as an instance of a particular class more than once in the program.
プログラム中において,特定のクラスに対し,ある型をそのインスタンスとして一度より多く (複数回) 定義することはできません.
この制限は時折物議を醸すわけで,実際この制限を緩和する GHC の言語拡張も幾つか存在する.しかし,言語拡張でも完全にこの制限が取り払えるわけでは無い.では,具体的に何が問題になるかを考えてみる.次のようなプログラムを考えてみよう:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 | class C1 a where m1 :: a class C1 a => C2 a where m2 :: a -> a instance C1 Int where m1 = 0 instance C2 Int where m2 x = x + 1 f :: (C1 a, C2 a) => a f = m2 m1 g :: Int g = f |
このプログラムでは,型クラスの継承が行われている.継承とは,型があるクラスに所属している場合にのみ,そのクラスのインスタンスを定義できるという制約をかける機能で,いわばある型クラスの部分クラスを定義できる機能だ.この場合の elaboration によって得られるプログラムは,
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 | data DictC1 a = DictC1 { m1 :: a } data DictC2 a = DictC2 { superC1 :: DictC1 a , m2 :: a -> a } instDictC1_Int :: DictC1 Int instDictC1_Int = DictC1 { m1 = 0 } instDictC2_Int :: DictC2 Int instDictC2_Int = DictC2 { superC1 = instDictC1_Int , m2 = \x -> x + 1 } f :: DictC1 a -> DictC2 a -> a f d1 d2 = m2 d2 (m1 d1) g :: Int g = f instDictC1_Int instDictC2_Int |
のように elaboration される.そうとは限らなくね?と思った人は正しくて,実は elaboration はもう一つやり方がある.それは次の部分を変えるやり方だ:
1 2 3 4 | f :: DictC1 a -> DictC2 a -> a - f d1 d2 = m2 d2 (m1 d1) + f _ d2 = m2 d2 (m1 d1) where + d1 = superC1 d2 |
関数 f における制約から C1 a のインスタンスを保証する方法は,制約中の C1 a から直接保証する方法と,C2 a からその上位クラスが C1 a であることを導きそこから保証する方法の2通りあり,前者が最初に示した方法,後者がその次に示した方法ということになる.ところで,この2通りの elaboration について,もし Int の C1 に対するインスタンスが複数定義できた場合を考えてみる.この場合,elaboration において DictC2 の superC1 にその内の1つが入り,g の呼び出し時に f に渡す DictC1 a の値は別のものが入ると,2通り示した elaboration の方法のどちらを採用するかによって,g の結果が変わる可能性がある.
また,もう1つ別の例を見てみよう:
1 2 | h :: (Int, Int) h = (m1, m1) |
この例は次のように elaboration される:
1 2 | h :: (Int, Int) h = (m1 instDictC1_Int, m1 instDictC1_Int) |
さて,この例は,Int に対する C1 のインスタンスの定義が1つだから,何も考えずに instDictC1_Int を渡すことができているわけだ.しかし,インスタンスが複数あった場合は,もちろん次のような elaboration があり得るかもしれない:
1 2 | h :: (Int, Int) h = (m1 instDictC1_Int, m1 instDictC1_Int') |
つまり,それぞれ異なるインスタンスが適用されるわけだ.この例だとあまり問題に対して直感的では無いかもしれないが,例えば等価性をあるプログラムで2回使った場合,等価性のためのインスタンスが2種類あった場合,最初の使用と2回目の使用で異なる等価性のアルゴリズムが動くということがあり得るということだ.これは,多くの人にとってあまり嬉しい仕様では無いだろう.この例は先ほどの例に比べたら些細な例だと思えるかもしれない.多くの場合インスタンス解決のアルゴリズムが,このような狭いスコープで異なるインスタンスを選ぶことはまずない [2].ただ,次のような状況を考えてみるとどうだろう?
1 2 3 4 5 6 7 8 9 10 11 | instance C1 Int where m1 = 0 h1 :: Int h1 = m1 instance C1 Int where m1 = 1 h2 :: (Int, Int) h2 = (m1, h1) |
この場合,h1 での m1 と,h2 での m1 で異なるインスタンスを使う可能性は十分ありうる.これを是とするかどうかは,おそらく意見の分かれるところだと思う.ただ,Haskell では equational reasoning に基づく変形が好まれるため,h1 を直接 m1 に置き換える変形ができないことは,1つの問題点となりうる.
一般に,型クラスのインスタンス解決は型システムに組み込まれることが多い.その場合,型検査の際インスタンス解決が行われる.そして,型検査において作られた型の導出木に対する変換により elaboration が行われる.このような変換の枠組みは,型クラス以外でも採用されることがある.具体的には,暗黙の型変換やレコード型などだ.そして,それらの場合にも上記で挙げた複数のインスタンスがある場合に起こる問題と似たような問題が起こることがある.この問題は,次のように形式化される:
型の導出木から言語への変換があった時,ある型の異なる2つの導出木において,変換を行った結果が意味論同値にならない.
例えば,h の例では2つの m1 に対してそれぞれ同じインスタンスを使っても異なるインスタンスを使っても,どんなインスタンスを使っても,それが Int に対する C1 のインスタンスであれば型検査は通るのが一般的だ.しかし,その場合使ったインスタンスに対する elaboration した結果は,他のインスタンス解決を行ってから elaboration した結果と振る舞いが変わる場合がある.逆にこのような問題がなければ,型システムに対して一定の保証が与えられる.この保証,つまり上記で形式化した問題が成り立たない型システムと elaboration の性質のことを,一般に coherence と呼ぶ [3].coherence を保証する方法論は幾つかあるが,Haskell では型クラスのインスタンスを1つしか定義できないようにすることで,coherence を保証している [4].
orphan インスタンス
さて,Haskell では coherence を保証するため,型クラスのインスタンスは型に対して1つしか定義できないようにしている.ところで,この「型クラスのインスタンスは型に対して1つしか定義できないようにする」というのは,言うだけなら単純に見えるが,幾つかの課題もある.特に著名な問題が,orphan インスタンスである.GHC では,ある型 T の C のインスタンス宣言において,その宣言が T の宣言または C の宣言と同じモジュールにあるかないかで,インスタンスに関する扱いが変わる.特に同じモジュールにない場合は,orphan インスタンスと呼ばれ,警告が表示されるようになっている.なぜこのような区分があるのだろうか?
まず,Haskell ではインスタンスが暗黙的にモジュール間を伝搬する.これは,以下のように規定されている:
All instances in scope within a module are always exported and any import brings all instances in from the imported module. Thus, an instance declaration is in scope if and only if a chain of import declarations leads to the module containing the instance declaration.
モジュールにおいて,スコープ内の全てのインスタンスは常にエクスポートされ,任意の import は,インポートしたモジュールから全てのインスタンスを取り込みます.したがって,インスタンス宣言がスコープ内にあるということは,import 宣言のチェインがそのインスタンス宣言を含むモジュールにたどり着くということと同値です.
—Haskell Language Report 5.4 Importing and Exporting Instance Declarations
私たちにこの伝搬を止めることはできないし,制御することもできない.これは,そもそもプログラム中でインスタンスは型に対して1つしか定義できないため制御する必要が特に生じないからだ [5].ところで,こういう規定があるのはいいとして,実際問題として Haskell のコンパイラは,インスタンスの解決をこの規定に従って行わなければならない.もちろん,どのモジュールにインスタンスがあるか分からないため,最悪全てのモジュールを調べる必要がある.ユーザ側にとってもこの規定は問題だ.もし,重要な2つのモジュールがそれぞれある型に対しての別々のインスタンス定義を保有している場合,それらのモジュールが import チェインに入ってる全てのモジュールがインスタンスの競合により使用できなくなる.
ところで,ある型のあるクラスのインスタンスを使用する場合,その型とクラスに関する情報が無いとどうしようもないので,それぞれの宣言があるモジュールの情報は必ず見に行くことになる.そして,第三者がそのモジュールをいじると言うことは起こり得ない.つまり,そのいずれかのモジュールにインスタンス宣言が含まれているなら,コンパイラにとって必要な情報を見るついでにインスタンスも見れ,またユーザ側にとってももしインスタンス競合が起こったならそもそもその型やクラスを読み込めないことになるため,逆に型やクラスが読み込めればインスタンス競合がないことが保証でき嬉しい.そこで,Haskell ではある型のあるクラスに対するインスタンス宣言は,その型またはクラス宣言と同じモジュールに置くことが推奨されている.逆に独立したモジュールにあるインスタンスは orphan インスタンスと呼ばれ,なるべく控えるように勧告されている.そのため,ある型に対して独立にインスタンスが作りたい場合,newtype によって新たにインスタンスの意味論だけを変える型を作り,その型に対するインスタンス宣言を行うということが行われている.
なお,GHC では,orphan インスタンスがあるモジュールは内部でマークされていて,モジュールのインターフェースファイルにはそのモジュールが依存する orphan インスタンスのあるモジュールが列挙されている.そして,コンパイル時にそのリストにあるモジュールの全てのインターフェースファイルを読みに行くようになっている.よって,一旦 orphan インスタンスを作ってしまうと,そのインスタンスがあるモジュールのインターフェースファイルは,そのモジュールに依存する全てのモジュールが再コンパイルされる際,どのような変更だろうと読み込まれることになる.よって,orphan インスタンスはコンパイル時間にも悪影響を与える [6].
まとめ
というわけで,型クラスのコヒーレンスと orphan インスタンスの関係性について紹介した.一応,インスタンスが型に対して1つしか作れないのと,インスタンスが暗黙に伝搬してしまうのには理由があるんだよと言う話でした.最近 Haskell のフォークみたいな言語を作ろうとしてて,そういやこの辺まとまった記事ないなあと思って書いた.ezyang 先生の Type classes: confluence, coherence and global uniqueness はよくまとまってるので,この辺もよかったら参照すると良さそう.
なお,別の話題として型クラスの elaboration って要は暗黙的な引数の elaboration と見做せるよねと言う話題が古くからある.ただ,暗黙的引数とみるからには明示的に適用したくなるわけで,その辺の機能を入れた場合に coherence をどう考えるかという話題があったりする.この辺は一昨年の Haskell Symposium で Coherent explicit dictionary application for Haskell というセッションがあったりする.この辺も近いうちに紹介できたらなと思う (思ってるだけ).
[1] | なお,素の Haskell には落とせなくて,ランク2多相ぐらいが必要になる. |
[2] | もちろん故意にそのようなアルゴリズムを作る場合は別だが. |
[3] | みんな読んでる TaPL では,15.6 で触れられてるっぽい.ここでは,subtyping を例にとってる. |
[4] | ところで,GHC では INCOHERENT プラグマというものが用意されており,名前の通り coherence を捨てる代わりに複数のインスタンス定義をできるようにするプラグマだ.当然の帰結ながら,GHC ユーザの間ではあまり使わないほうがいいプラグマとして扱われている. |
[5] | と言ってみたものの,制御する方はそれでいいとして,伝搬を止める方は実は問題があるのかよく分かってない.coherence が成り立たなくなるような気が直感的にするんだけど,インスタンスが消えるということは,型の導出がそもそもできない気がしていて,それは大丈夫そうな気もする? ただ,equational reasoning による変形がモジュール跨ぐとできなくなる場合が生じるという点では問題. |
[6] | と言っても他の要素に比較すればそれほど大した時間ではないが. |