長さ付きリスト

Haskell

id:msakaiさんが、sized-list の appendで長さ付きのリストを扱う方法を解説してくれている。すばらしい。
しかし型関数なんていうかっちょいいものがあったのかー。型関数の意味とか能力はさっぱりわからんけど、こんな風にかけてしまうとはおどろきである。参考文献をあとで読んでみることにしよう。

で、とりあえず専用の型クラスを使う方法をやってみた。id:msakaiさんのオリジナルのものとは若干違う気がするが。関数名は適当。

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
data S n
data Z
data NON
data List n a where
    Nil :: List Z a
    Cons :: a -> List n a -> List (S n) a
instance (Show a) => Show (List n a) where
    show Nil = "[]"
    show (Cons x xs) = show x ++ ":" ++ show xs

class Append m n l | m n -> l where
    append :: (List m a) -> (List n a) -> (List l a)
instance Append Z n n where
    append Nil ys = ys
instance Append n m o => Append (S n) m (S o) where
    append (Cons x xs) ys = Cons x (append xs ys)

test :: List (S (S (S (S Z)))) Int
test = append (Cons 1 $ Cons 2 Nil) (Cons 3 $ Cons 4 Nil)

class Inter a b | a -> b where
    inter :: x -> (List a x) -> (List b x)
instance Inter Z Z where
    inter _ Nil = Nil
instance Inter m n => Inter (S m) (S (S n)) where
    inter a (Cons x xs) = Cons x $ Cons a $ inter a xs

x = inter 0 $ Cons 1 $ Cons 2 Nil

interは、要素の間に指定した要素を挟み込む関数のつもり。これだと常に長さが2倍になるので、型はそういうふうに宣言した。変なinterの定義をするとちゃんと怒られる。すばらしい。ところが、

case x of
  [] -> ...
  [x] -> ...
  x:xs -> ...

みたいな場合分けを書こうとして困った。インスタンス宣言がかぶってしまう。

class Inter a b | a -> b where
    inter :: x -> (List a x) -> (List b x)
instance Inter Z Z where
    inter _ Nil = Nil
instance Inter (S Z) (S Z) where
    inter a (Cons x Nil) = Cons x Nil
instance Inter m n => Inter (S m) (S (S n)) where
    inter a (Cons x xs) = Cons x $ Cons a $ inter a xs

    Functional dependencies conflict between instance declarations:
      instance Inter (S Z) (S Z)
        -- Defined at /Users/sho/tmp/haskell/append.hs:(27,0)-(28,36)
      instance (Inter m n) => Inter (S m) (S (S n))
        -- Defined at /Users/sho/tmp/haskell/append.hs:(29,0)-(30,53)
Failed, modules loaded: none.

これはそのうち考える。

問題その２。この長さ付きリストに対してフィルターすることを考える。リストの長さは実行時までわからないので、フィルタ関数filtの型はNONとかにしたい。NONは長さのよくわかんないリストを表す型で、NONなものに対してなにかの操作をしても常にNONになるようにしたい。とりあえず思いつきで。

class Filter a where
    filt :: (x -> y) -> List a x -> List NON y
instance Filter Z where
    filt f Nil = Nil
instance (Filter n) => Filter (S n) where
    filt f (Cons x xs) = Cons (f x) $ filt f xs

あたりまえだが怒られる。Nilの型はNONじゃなくてZだからね。はてさてどうしよう。
型に関しての知識がなんにもないから、Haskellの型システムがどんだけ頑張れるかよくわからないんだよねー。