IdrisでHVectを反転させるには？

Question

私はIrdisを初めて利用しています。 HVectを取り消すことはできますか？ HVect [String, Int]で逆を呼び出すと、HVect [Int, String]が返され、HVect [String, Int, Day]で逆に呼び出すとHVect [Day, Int, String]が返されます。

私はData.Vect.reverse（Gist）

module reverse_hvect 

import Data.HVect 

reverse : HVect ts -> HVect (reverse ts) 
reverse [] = [] 
reverse (x::xs) = (reverse xs) ++ [x] 

を再利用しようとしたが、私はData.Vect.reverseは、アキュムレータと内部機能goを使用しているので、私は同じ構造でVect.reverse私自身が書いた

Type checking .\reverse_hvect.idr 
reverse_hvect.idr:7:9:When checking right hand side of reverse_hvect.reverse with expected type 
     HVect (reverse (t :: ts)) 

Type mismatch between 
     HVect (Data.Vect.reverse, go Type k ts [] ts ++ [t]) (Type of reverse xs ++ [x]) 
and 
     HVect (Data.Vect.reverse, go Type (S k) (t :: ts) [t] ts) (Expected type) 

Specifically: 
     Type mismatch between 
       Data.Vect.reverse, go Type k ts [] ts ++ [t] 
     and 
       Data.Vect.reverse, go Type (S k) (t :: ts) [t] ts 
Holes: reverse_hvect.reverse 

を取得私のHVect.reverse（Gist）

module reverse_hvect 

import Data.Vect 
import Data.HVect 

myReverse : Vect n a -> Vect n a 
myReverse [] = [] 
myReverse {n = S k} (x::xs) = rewrite plusCommutative 1 k in (myReverse xs) ++ [x] 

reverse : HVect ts -> HVect (myReverse ts) 
reverse [] = [] 
reverse (x::xs) = (reverse xs) ++ [x] 

が、私は

Type checking .\reverse_hvect.idr 
reverse_hvect.idr:12:9:When checking right hand side of reverse_hvect.reverse with expected type 
     HVect (myReverse (t :: ts)) 

Type mismatch between 
     HVect (myReverse ts ++ [t]) (Type of reverse xs ++ [x]) 
and 
     HVect (replace (sym (replace (sym (replace (sym (plusZeroRightNeutral k)) Refl)) (replace (sym (plusSuccRightSucc k 0)) Refl))) (myReverse ts ++ [t])) (Expected type) 

Specifically: 
     Type mismatch between 
       myReverse ts ++ [t] 
     and 
       replace (sym (replace (sym (replace (sym (plusZeroRightNeutral k)) Refl)) (replace (sym (plusSuccRightSucc k 0)) Refl))) (myReverse ts ++ [t]) 
Holes: reverse_hvect.reverse 

Answer 1

user3237465の答え：

import Data.Vect 
import Data.HVect 

nreverse : Nat -> Nat 
nreverse Z = Z 
nreverse (S n) = nreverse n + 1 

vreverse : Vect n a -> Vect (nreverse n) a 
vreverse [] = [] 
vreverse (x :: xs) = vreverse xs ++ [x] 

hreverse : HVect ts -> HVect (vreverse ts) 
hreverse [] = [] 
hreverse (x :: xs) = hreverse xs ++ [x] 

あなたは異なるが逆転で同じ構造を持つ正しい考えを持っていましたが、より困難な構造を試してみました。

Answer 2

は、タイプレベルでrewrite Sを有する別のエラーが出る悪い考えです。私はイドリスタイプチェッカーを持っていないが、このAgdaコードを適応するのは簡単でなければなりません：

open import Data.Nat.Base 
open import Data.Vec hiding (reverse) 

infixr 5 _∷ₕ_ _++ₕ_ 

nreverse : ℕ -> ℕ 
nreverse 0  = 0 
nreverse (suc n) = nreverse n + 1 

vreverse : ∀ {n α} {A : Set α} -> Vec A n -> Vec A (nreverse n) 
vreverse []  = [] 
vreverse (x ∷ xs) = vreverse xs ++ (x ∷ []) 

data HList : ∀ {n} -> Vec Set n -> Set where 
    []ₕ : HList [] 
    _∷ₕ_ : ∀ {n A} {As : Vec Set n} -> A -> HList As -> HList (A ∷ As) 

_++ₕ_ : ∀ {n m} {As : Vec Set n} {Bs : Vec Set m} -> HList As -> HList Bs -> HList (As ++ Bs) 
[]ₕ  ++ₕ ys = ys 
(x ∷ₕ xs) ++ₕ ys = x ∷ₕ xs ++ₕ ys 

reverseₕ : ∀ {n} {As : Vec Set n} -> HList As -> HList (vreverse As) 
reverseₕ []ₕ  = []ₕ 
reverseₕ (x ∷ₕ xs) = reverseₕ xs ++ₕ (x ∷ₕ []ₕ) 

すなわち、あなたはちょうど逆の塔の中にお互いを必要とします。すなわち、番号を「逆転させる」ものです。reverse

reverseVectについては、Idrisライブラリの方が関係が深いです。 Hereは書き換えのないバージョンです。イドリスで