5

静的に型指定された長さのリストが与えられた場合 (例としてこれを取り上げます):

data Zero

data Succ nat

data List el len where
    Nil  ::                      List el Zero
    Cons :: el -> List el len -> List el (Succ len)

通常の再帰ではなく静的型付けを使用して長さを計算する長さ関数を書くことは可能ですか?

これまでの私の努力は、それを繰り返すために型情報を「持ち上げる」必要があるため、それは不可能であるという結論に私を導きました:

class HasLength a where
    length :: a -> Natural

instance HasLength (List el Zero) where
    length _ = 0

instance HasLength (List el (Succ len)) where
    length _ = 1 + *how to recur on type of len*

しかし、私は型で可能なすべての魔法について学び始めたばかりなので、解決策を考えられないからといって、解決策が存在しないことを意味するわけではないことはわかっています。

アップデート

length は Natural を返すため、間違って と書きlength _ = 1 + ...ました。正しいインスタンス (以下の回答を使用) は次のとおりです。

instance HasLength (List el len) => HasLength (List el (Succ len)) where
    length _ = succ $ length (undefined :: List el len)
4

2 に答える 2

8

たとえば、次のようにします。

instance HasLength (List el len) => HasLength (List el (Succ len)) where
    length _ = 1 + length (undefined :: List el len)

注: これにはScopedTypeVariables拡張が必要です。

于 2012-11-26T00:05:07.973 に答える