Haskell 型クラスで型推論を制御 (zipWith編)

Haskell

型レベル計算で、zipWith をやりたい。 ちなみに zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] で、まあそういう関数だ。

しかし まともに使える関数を作るには、陽に型を指定せずとも型が推論されてくれないと困る。

そこで zipWithに渡す関数の種類を、引数戻り値のどれか1つの型がわからなくても勝手に推論してくれるものに限定する。
以下のように実装した。

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts, EmptyDataDecls #-}
{-# LANGUAGE UndecidableInstances #-}

-- 引数(2つ)と戻り値の型のうち、どれか2つが決まれば 残り1つの型も決まる
class Bijection2 f x y z | f x y -> z, f y z -> x, f z x -> y

-- 型レベルの真偽値
data T = T
data F = F

-- 例えば xor は 2つ決まれば残り1つも決まる
data Xor
instance Bijection2 Xor T F T
instance Bijection2 Xor F T T
instance Bijection2 Xor F F F
instance Bijection2 Xor T T F
xor :: Xor
xor = undefined

-- 型レベル zipWith
-- 型レベルのリストを (head, tail) のタプルで表現している () は空リスト
class ZipWith f ls ls' ls'' | f ls ls' -> ls'', f ls' ls'' -> ls, f ls ls'' -> ls'
instance ZipWith f () () ()
instance (Bijection2 f x y z, ZipWith f xs ys zs) => ZipWith f (x, xs) (y, ys) (z, zs)

zipwith :: ZipWith f ls ls' ls'' => f -> ls -> ls' -> ls''
zipwith = undefined

-- 型レベル zipWith xor
xorlist xs ys = zipwith xor xs ys

テスト

b1 = xorlist (T, (F, (T, (T, ())))) (F, (T, (F, (F, ())))) -- 引数2つの型を決める
-- *Main> :t b1
-- b1 :: (T, (T, (T, (T, ())))) -- 戻り値の型が決まる


b2 x = (xorlist (T, (F, (T, (T, ())))) x) :: (T, (T, (T, (T, ())))) -- 第1引数の型を決め，さらに戻り値の型を陽に指定する
-- *Main> :t b2
-- b2 :: (F, (T, (F, (F, ())))) -> (T, (T, (T, (T, ())))) -- 第2引数の型が決まる

問題

結果の型が () (空リスト) の時は どちらの引数も空リストのはずだが、それは推論できない。

b3 x y = xorlist x y :: ()
-- *Main> :t b3
-- b3 :: (ZipWith Xor ls ls' ()) => ls -> ls' -> ()

もちろん型検査は働くので、ひとたび誤った引数に適用すればちゃんと型エラーになる。念のため:

*Main> :t b3 (T, ()) (F, ())

Top level:
    Couldn't match expected type `()' against inferred type `(z, zs)'
    When using functional dependencies to combine
      ZipWith f (x, xs) (y, ys) (z, zs),
        arising from the instance declaration at typeclass_inference.hs:24:0
      ZipWith Xor (T, ()) (F, ()) (),
        arising from a use of `b3' at <interactive>:1:0-17

しかし情報は多いに越したことはないので、引数戻り値の型のどれかが () に推論された時は、残りの型も決めてしまいたい。

解法

おなじみのアレを使う。

class TCast t t' | t -> t', t' -> t
instance TCast t t

TCast t1 t2が型文脈にあるとき、 t1=t2となるように型推論がうごく。

もとのZipWithをZipWith2 という名前に変える。

class ZipWith2 f ls ls' ls'' | f ls ls' -> ls'', f ls' ls'' -> ls, f ls ls'' -> ls'
instance ZipWith2 f () () ()
instance (Bijection2 f x y z, ZipWith2 f xs ys zs) => ZipWith2 f (x, xs) (y, ys) (z, zs)

ZipWith に、型を refine する別の型クラス Refine をしかけておく。

class ZipWith f ls ls' ls''
instance (ZipWith2 f ls ls' ls'', Refine ls ls', Refine ls' ls'', Refine ls'' ls) => ZipWith f ls ls' ls''

ここで Refine はこんな型クラスだ：

class Refine ls ls'
instance TCast ls () => Refine () ls
instance (TCast ls (x,xs)) => Refine (y,ys) ls

Refineの左手側が決まれば、インスタンスが選択され、TCastで右手側の型がrefineされる。 リストの要素の型は異なる場合があるため ls -> ls' ではないことに注意。

テスト2

*Main> :t b3
b3 :: () -> () -> ()

期待通り、推論してくれた。

余

instance (TCast ls (x,xs), Refine ys xs) => Refine (y,ys) ls

にすれば、こんなこともできた：

*Main> :t \x -> \y -> (xorlist x y :: (T,(T,(T,(T,())))))
\x -> \y -> (xorlist x y :: (T,(T,(T,(T,()))))) :: (Bijection2 Xor x y T,
                                                    Bijection2 Xor x1 x4 T,
                                                    Bijection2 Xor x2 x5 T,
                                                    Bijection2 Xor x3 x6 T) =>
                                                   (x, (x1, (x2, (x3, ()))))
                                                   -> (y, (x4, (x5, (x6, ()))))
                                                   -> (T, (T, (T, (T, ()))))
*Main>

要するに、リストの構造のみrefineする方法が必要だったわけだ。 fundepsはリストの中身まで依存を張ってしまうのでそれができなかった。

(あと今気づいたけど本来のzipWithは引数のリストの長さが異なっても良いのですよね。)