Haskell 型クラスと定理証明

Haskell

型レベルの数値と、引き算Sub, 型レベルのconsリスト、リストの長さを求める型クラスLengthと関数length_tを定義する。

data S n
data Z

class Sub n n' n''  | n n' -> n''
instance Sub n Z n
instance Sub n n' n'' => Sub (S n) (S n') n''

class Length xs n | xs -> n
instance Length () Z
instance Length xs n => Length (x, xs) (S n)

length_t :: Length xs n => xs -> n
length_t = undefined

リストxsのn番目の要素xを取得する関数(型クラス)

class Take n xs x | n xs -> x
instance Take Z (x, xs) x
instance Take n xs x' => Take (S n) (x, xs) x'

諸事情により、リストの後ろからn番目の要素を取得する関数を定義したい。

-- 後ろから n 番目の要素を取得
take_back :: (Length xs n', Sub n' (S n) n'', Take n'' xs x) => n -> xs -> x
take_back = undefined

これは使えるだろうか？ 長さnのリストの頭に型Boolを追加して、後ろからn番目を取得してみる。 

test xs = take_back n (True, xs)
  where n = length_t xs

Boolが返ってきてほしい。

*Main> :t test ()  
test () :: Bool
*Main> :t test (1, ())
test (1, ()) :: Bool
*Main> :t test (1, ("abc", ()))
test (1, ("abc", ())) :: Bool

オッケーだ。しかし test の型は？ どうみても test :: xs -> Bool みたいな型だけれども…

こうなる。

*Main> :t test
test :: (Length xs n, Sub n n n'', Take n'' (Bool, xs) x) => xs -> x

Sub n n n'' とある。 お前それどう見ても n'' = Z やないか… しかしHaskellはCHRに従ってコンテキストリダクションしてるだけなのでこれを解いてくれない。
Subで与えた引き算の規則がまずいのか。

こうしてみる：

instance Sub n n Z
instance Sub n n' n'' => Sub (S n) n' (S n'')

が…駄目…！

typeclass_inference.hs:103:0:
    Functional dependencies conflict between instance declarations:
      instance [overlap ok] Sub n n Z
        -- Defined at typeclass_inference.hs:103:0-17
      instance [overlap ok] (Sub n n' n'') => Sub (S n) n' (S n'')
        -- Defined at typeclass_inference.hs:104:0-44

苦肉の策として

instance Sub n n Z
instance Sub (S n) n (S Z)
instance Sub (S (S n)) n (S (S Z))
instance Sub (S (S (S n))) n (S (S (S Z)))
instance Sub (S (S (S (S n)))) n (S (S (S (S Z))))
instance Sub (S (S (S (S (S n))))) n (S (S (S (S (S Z)))))
instance Sub (S (S (S (S (S (S n)))))) n (S (S (S (S (S (S Z))))))

こうすれば、まあ解けるが… (実際には上の1つがあればよい)

*Main> :t test
test :: (Length xs n) => xs -> Bool