Wie man einen HVect in Idris umkehrt?

Question

Ich bin neu bei Irdis. Ist es möglich, eine HVect umzukehren? Wenn ich auf einer HVect [String, Int] umgekehrte rufe, sollte es eine HVect [Int, String] zurückgeben, und wenn ich rückwärts auf HVect [String, Int, Day] rufe, sollte es eine HVect [Day, Int, String] zurückgeben.

Ich versuchte Data.Vect.reverse (Gist)

module reverse_hvect 

import Data.HVect 

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

aber ich

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 

Seit Data.Vect.reverse verwendet, schrieb ich meine eigenen Vect.reverse mit der gleichen Struktur eine innere Funktion go mit einem Akkumulator erhalten wiederzuzuverwenden als mein 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] 

aber ich bekomme einen anderen Fehler

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 Antwort in Idris:

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] 

Sie hatte die richtige Idee mit den gleichen Strukturen in den verschiedenen Rückschlägen, aber versucht, die schwierige Struktur.

Answer 2

rewrite s auf der Typebene zu haben, ist eine schlechte Idee. Ich habe nicht die Art Kontrolleur Idris, aber es sollte diesen Agda Code anzupassen einfach sein:

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 ∷ₕ []ₕ) 

D.h. Sie brauchen nur noch reverse im Turm der Umkehrungen, nämlich derjenige, der eine Zahl "reversiert".

BTW, reverse für Vect s in der Idris-Bibliothek ist mehr beteiligt, als es sein sollte. Here ist eine umschreibefreie Version.