1

我正在尝试实现类型安全的二项式堆。为此，我有两种数据类型，它们的元素类型由它们的类型编码索引参数化：

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 期的第三篇文章……嗯，我写的……讨论了 Haskell 中的类型安全二项式堆，以及如何正确实现它们。

于 2012-08-18T19:12:25.193 回答