型クラス、Functional Dependencies、静的型キャスト、Constraint Handling Rules

Strongly typed heterogeneous collectionsの論文では、Haskellの型クラスで使える種々のテクニックが解説されている。

なかでも、型クラスTypeCastで型推論の向きをプログラマが指定する(type improvement)というテクニックがとてもおもしろい (8節の直前)。

しかしながら、この論文は Functinoal Dependenciesの意味をConstraint Handling Rulesで定式化したUnderstanding functional dependencies via constraint handling rulesより以前に書かれている。 そこで、CHRベースでTypeCastを説明してみたい。

問題

FunDepsを使わない型クラスColを次の通り定義する．

class Col a b where
  inCol :: a -> b
instance Col a [a] where
  inCol x = [x]

ここで，head $ inCol True のような式は型Boolを持つことを期待したい(インスタンスのオーバーラップを許さない場合)が，そうはならない．

*Main> :t head $ inCol True

<interactive>:1:0:
    No instance for (Col Bool [a])
      arising from a use of `it' at <interactive>:1:0-16
    Possible fix: add an instance declaration for (Col Bool [a])
    In the first argument of `print', namely `it'
    In the expression: print it
    In a 'do' expression: print it

実際には、head $ inCol True :: Col Bool [a] => a という型をもつ．この型変数aがBoolであってほしいのだが，そうはなっていない．そして，型シグニチャがないため悪名高いMonomorphism Restrictionのために型付けに失敗しているのだ．(-fno-monomorphisim-restrictionオプションを付ければ，この型エラーは出ない)

(ここで次のとおりFunDepsを使えば，期待通りの結果が得られる．

class Col a b | a->b where
  inCol :: a -> b
instance Col a [a] where
  inCol x = [x]

*Main> :t head $ inCol True
Bool

)

TypeCastの効用

インスタンスでTypeCastを使えば，クラス宣言でFunDepsを使わなくても，同様の効果が得られる：

class TypeCast a b | a->b, b->a where
  typeCast :: a->b
instance TypeCast a a where
  typeCast = id

class Col' a b where
  inCol' :: a -> b
instance TypeCast a b => Col' a [b] where -- ここがポイント
  inCol' x = [typeCast x]

*Main> :t head $ inCol' True
Bool

Understanding functional dependencies via constraint handling rules

FunDepsを伴う型クラスの解決には，Constraint Handling Rules(CHR)という制約論理プログラミングの意味が用いられる．詳細は，Understanding functional dependencies via constraint handling rulesを参照してください．

ここで用いているCHRは，元のCHRからガード式等を取り除いたサブセットである．

型クラスからの変換

rule Col a [a] <==> true.  (ColのインスタンスCHR)

rule Col' a [b] <==> TypeCast a b. (Col'のインスタンスCHR)
rule TypeCast a b ==> a=b.  (TypeCastのインスタンス improvement CHR)
rule TypeCast a a <==> true. (TypeCastのインスタンスCHR)

変換についてはUnderstanding.. を参照． <==> はsimplification rule, ==> は propagation ruleとよび，それぞれ論理的同値，含意を意味します．個々のルールに出現する変数はそれぞれで全称修飾されていて，全ての規則が論理積で結ばれているのがCHRプログラムの意味です．

ゴール(もとの型文脈)に対してCHRプログラムを適用した結果出てくる制約が簡約された型文脈になり，その時に導出できた型変数の同値性で型推論がimproveされます．

head $ inCol True の型について (Col Bool [c] => c) の文脈の簡約をこころみる．Col Bool [c]をゴールとして，CHRで計算するのだけど，このゴールは規則rule Col a [a] <==> true.のヘッド(Col a [a])と一致させることはできず([c/a]かつ[Bool/a]となるような代入は存在しない)，CHRの計算がここで止まる．そのまま (head $ inCol True :: Col Bool [c] => c) という型になる．

（この事実はてきとうなCHR処理系で確かめることも出来る．）

いっぽう， head $ inCol' True は，(Col' Bool [c] => c) から始まる． 規則 rule Col' a [b] <==> TypeCast a b よりゴールが TypeCast Bool c となる．さらに rule TypeCast a b ==> a=b より Bool=c が導ける．(TypeCast Bool c, c=Bool)をさらに計算して (true, c=Bool) となりここで計算が止まる． (c=Bool => c) という型はBool型なので (head $ inCol' True :: Bool) が導けた．

ポイントは

SimplificationやPropagationでは，ヘッドに何らかの代入をかけることでゴールとの単一化を試みるが，その逆ではない．(つまり，ゴールに何か代入したら単一化できそう(たとえばCol Bool [c] で[Bool/c]とやればいけそう)でも，それがゴールに追加されることはない．) instance Col a [a] というのは 制約であって単一化を駆動してくれるわけではない． 一方 TypeCastはインスタンスimprovement CHRでゴールにc=Boolといった制約を追加してくれるのでそれが型推論に効いてくる．

そのほか

Understanding.. でのCHRの操作的意味論の説明の所で θ(c')=c となっているが θ(c)=c' の間違いではなかろうか．ヘッドに代入をかけてゴールと単一化するのであってその逆ではないと思った．