转换其元素类型参数化其类型编码索引的列表

Question

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

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

它应该简单地颠倒给定列表的顺序。有任何想法吗？提前致谢。

Answer 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

Answer 2

供您参考，third article of Issue 16 of the Monad.Reader...嗯，我写的...讨论了 Haskell 中的类型安全二项式堆，以及如何正确实现它们。