Как отменить 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] 

, но я получаю

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 

Поскольку Data.Vect.reverse использует внутреннюю функцию go с аккумулятором, я написал свой собственный Vect.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 с на уровне типа это плохая идея. У меня нет проверки типов Идриса, но это должно быть просто адаптировать этот 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 в башне разворотов, а именно тот, который «меняет» число.

BTW, reverse для Vect s в библиотеке Идриса более активно, чем должно быть. Here - это версия без перезаписи. Ответ