日々の流転

λ. sized-list の append

PPL2008の懇親会でzyxwvさん、yoshihiro503さんと話していたときに出た話(の一つ)。

以下で定義される、サイズ情報を型に持つようなリスト型があったとする。

data Z
data S n

data List n a where
    Nil :: List Z a
    Cons :: a -> List n a -> List (S n) a

このリスト型に対して連結(append)を定義したいのだが、どうやって型を付けるかというのが自明ではない。

関数従属性を使う方法 (ダメな方法)

class Plus m n o | m n -> o
instance Plus Z n n
instance Plus m n o => Plus (S m) n (S o)

append :: Plus m n o => List m a -> List n a -> List o a
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

これは一見うまくいきそうだが、第一引数がNilの場合であっても、GHCは List n a と List o a が同じ型であることを認識してくれず、型エラーとなる。 これは関数従属性の落とし穴と同じ問題。

GADT の type refinement を利用する方法

data Plus m n o where
    PlusZ :: Plus Z n n
    PlusS :: Plus m n o -> Plus (S m) n (S o)

append :: Plus m n o -> List m a -> List n a -> List o a
append PlusZ Nil ys = ys
append (PlusS n) (Cons x xs) ys = Cons x (append n xs ys)

関数従属性の場合と違って、GADTのパターンマッチ時にはちゃんと type refinement が起こるので、型付け出来る。 が、適用する際にわざわざPlus型の値を与えなくてはならないのが面倒くさい。

専用の型クラスを使う方法

class Append a b c  where
    append :: a -> b -> c

instance Append (List Z a) (List n a) (List n a) where
    append Nil ys = ys

instance Append (List n a) (List m a) (List o a) =>
         Append (List (S n) a) (List m a) (List (S o) a) where
    append (Cons x xs) ys = Cons x (append xs ys)

そりゃ出来るけどさぁ……何か色々負けた気分。

もう少し賢い定義も出来るけど、本質的にはあまり変わらないと思う。

型関数を使う方法

type family Plus m n
type instance Plus Z n = n
type instance Plus (S m) n = S (Plus m n)

append :: List m a -> List n a -> List (Plus m n) a
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

GHCの開発版に導入されている型関数(type function)を使う方法が一番スマートか。GHCの型関数の詳細については Towards open type functions for Haskell と GHC/Type families - HaskellWiki を参照。