我正在尝试在Idris中编写一个zip函数,它将任意长度相同的矢量(len
)组合成一个HList
s矢量。
也就是说,我试图概括以下函数:
module Zip
import Data.Vect
%default total
zip2 : (Vect len a, Vect len b) -> Vect len (a, b)
zip2 ([], []) = []
zip2 ((x :: xs), (y :: ys)) = (x, y) :: zip2 (xs, ys)
我使用向量定义自己的qazxsw poi(“异构列表”):
HList
这是使用此data HList : Vect n Type -> Type where
Nil : HList []
(::) : (x : a) -> (xs : HList as) -> HList (a :: as)
的zip2
函数的变体:
HList
到现在为止还挺好。
现在一般情况。
任意多拉链矢量的类型签名变得更加复杂,但我相信我做对了。
zip2H : HList [Vect len a, Vect len b] -> Vect len (HList [a, b])
zip2H [[], []] = []
zip2H [(x :: xs), (y :: ys)] = [x, y] :: zip2H [xs, ys]
是拉链的矢量数。 n
是每个向量的长度:
len
现在我的问题是:我甚至不能写vects : (len : Nat) -> Vect n Type -> Vect n Type
vects len as = map (\type => Vect len type) as
-- Example:
-- `vects len [a, b] = [Vect len a, Vect len b]`
-- You cannot pattern-match on types in Idris, so you cannot get an `a` from an `Vect len a`. Instead, I go the other way around in `zip` and pass my `a`s implicitly.
zip : {types : Vect (S n) Type} -> {len : Nat} -> HList (vects len types) -> Vect len (HList types)
定义的左侧。类型检查器一直在抱怨。
一个例子:
zip
zip {n = Z} [xs] = ?zip_rhs1
zip xs = ?zip_rhs2
我错过了什么?我是否以错误的方式使用隐式参数?我需要写一些样张吗?有没有更好的方法来构建函数类型签名?
(我的伊德里斯版本是When checking left hand side of Zip.zip:
When checking an application of Zip.zip:
Type mismatch between
HList [a] (Type of [xs])
and
HList (Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\type =>
Vect len
type)
types) (Expected type)
Specifically:
Type mismatch between
[a]
and
Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\type =>
Vect len
type)
types
。)
编辑:使用HTNW的代码我仍然得到基本相同的错误:
1.3.1-git:a93d8c9
module Zip
import Data.Vect
%default total
data HList : Vect n Type -> Type where
Nil : HList []
(::) : (x : a) -> (xs : HList as) -> HList (a :: as)
vects : (len : Nat) -> Vect n Type -> Vect n Type
vects len as = map (\type => Vect len type) as
multiUnCons : {len : Nat} -> {types : Vect n Type} ->
HList (vects (S len) types) -> (HList types, HList (vects len types))
multiUnCons {types = []} [] = ([], [])
multiUnCons {types = t :: ts} ((x :: xs) :: xss) with (multiUnCons xss)
| (ys, yss) = (x :: ys, xs :: yss)
zip : {types : Vect n Type} -> {len : Nat} ->
HList (vects len types) -> Vect len (HList types)
zip {len = Z} _ = []
zip {len = S n} xss with (multiUnCons xss)
| (ys, yss) = ys :: zip yss
testVectors : HList [Vect 3 Nat, Vect 3 Char]
testVectors = [[1, 2, 3], ['a', 'b', 'c']]
解决方案:*zip> :t Zip.zip testVectors
(input):1:4-23:When checking an application of function Zip.zip:
Type mismatch between
HList [Vect 3 Nat, Vect 3 Char] (Type of testVectors)
and
HList (vects len types) (Expected type)
Specifically:
Type mismatch between
[Vect 3 Nat, Vect 3 Char]
and
Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\type =>
Vect len
type)
types
需要更多信息:
zip
*zip> the (Vect 3 (HList [Nat, Char])) (zip testVectors)
[[1, 'a'], [2, 'b'], [3, 'c']] : Vect 3 (HList [Nat, Char])
你也必须匹配*zip> zip {types=[Nat, Char]} testVectors
[[1, 'a'], [2, 'b'], [3, 'c']] : Vect 3 (HList [Nat, Char])
。通过在types
上进行匹配,你还可以揭示关于types
的一些东西,这就是让你在vects len types
论证上进一步匹配的原因。此外,对HList (vects len types)
的S n
长度要求是不必要和破坏的。最后,我认为你实际上需要首先在types
,然后在len
上。 types
的递归最好写成一个不同的函数:
types
而multiUnCons : {len : Nat} -> {types : Vect n Type} ->
HList (vects (S len) types) -> (HList types, HList (vects len types))
multiUnCons {types = []} [] = ([], [])
multiUnCons {types = t :: ts} ((x :: xs) :: xss) with (multiUnCons xss)
| (ys, yss) = (x :: ys, xs :: yss)
本身很简单:
zip