gpt4 book ai didi

idris - 如何在 Idris 中反转 HVect?

转载 作者:行者123 更新时间:2023-12-05 00:56:17 25 4
gpt4 key购买 nike

我是 Irdis 的新手。是否可以反转 HVect ?如果我在 HVect [String, Int] 上调用 reverse它应该返回一个 HVect [Int, String]如果我在 HVect [String, Int, Day] 上调用 reverse它应该返回一个 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

最佳答案

user3237465 在 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]

您在不同的反向中使用相同的结构有正确的想法,但尝试了更困难的结构。

关于idris - 如何在 Idris 中反转 HVect?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36430390/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com