1

タイプセーフな二項ヒープを実装しようとしています。このために、型エンコードされたインデックスによって要素型がパラメーター化される 2 つのデータ型があります。

data Zero
data Succ a = Succ

{-| A GADT representation of lists with type-encoded length.
    Unlike the most common implementation, the type paramater
    for values is of kind * -> *. Each element type is
    parametrized by its index (counting from the end of the vector),
    so the type-encoded numbers decrease from start to end.
-}
data Vec n a where
    Nil  ::                   Vec Zero a
    Cons :: a n -> Vec n a -> Vec (Succ n) a

{-| A GADT representation of lists whose values are of kind
    * -> *. Each element type is parametrized by its by its
    index (counting from the start of the vector), so the
    type-encoded numbers increase from start to end.
    Unlike Vec the type-encode number here doesn't represent
    the length, it can be arbitrary (just increasing).
-}
data RVec n a where
    RNil  ::                           RVec n a
    RCons :: a n -> RVec (Succ n) a -> RVec n a

Vec数値パラメーターが減少する値をエンコードします。最後の要素は常に によってパラメーター化されZeroます。RVec他の制限なしで増加する数値パラメーターで値をエンコードします (これが、任意の数値RNilを生成できる理由RVecです)。

これにより、（たとえば）型システムによってチェックされた、高さが増加/減少するツリーのリストを持つことができます。プロジェクトの大部分を実装した後、実装できなかった一見単純な関数が必要であることに気付きました。

vreverse :: Vec n a -> RVec Zero a

指定されたリストの順序を単純に逆にする必要があります。何か案は？前もって感謝します。

4

2 に答える 2

1

私は答えを見つけたと思います：

vreverse :: Vec n a -> RVec Zero a
vreverse v = f1 v RNil
  where
    f1 :: Vec n a -> (RVec n a -> RVec Zero a)
    f1 Nil = id
    f1 (Cons x xs) = f1 xs . RCons x
于 2012-08-17T21:38:15.570 に答える
0

参考までに、Monad.Reader の第 16 号の 3 番目の記事では、Haskell のタイプ セーフな二項ヒープと、それらを正しく実装する方法について説明しています。

于 2012-08-18T19:12:25.193 に答える