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

Question

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

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

供大家参考，Monad.Reader第16期的第三篇文章...其中，嗯，我写了...讨论了 Haskell 中的类型安全二项式堆，以及如何正确实现它们。