Converting lists whose elements' types are paramertized their type-encoded indexes

Question

I'm trying to implement a type-safe binomial heap. For this, I have two data types whose element types are parametrized by their type-encoded indexes:

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 encodes values with decreasing number parameter, where the last element is always parametrized by Zero. RVec encodes values with increasing number parameter with no other restriction (this is why RNil can produce RVec of any number).

This allows me (for example) to have a list of trees with increasing/decreasing heights, checked by the type system. After implementing a large part of my project, I realized I need a seemingly simple function, which I wasn't able to implement:

vreverse :: Vec n a -> RVec Zero a

It should simply reverse the order of the given list. Any ideas? Thanks in advance.

Answer 1

For your reference, the third article of Issue 16 of the Monad.Reader...which, um, I wrote...discusses type-safe binomial heaps in Haskell, and how to implement them correctly.

Answer 2

I believe I found an answer:

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