广义 zip 函数的左侧从不进行类型检查

Question

我正在尝试在 Idris 中编写一个 zip 函数，它将任意多个相同长度 (len) 的向量组合成一个 HLists 向量。

也就是说，我正在尝试概括以下功能：

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)

我使用向量定义了我自己的HList（“异构列表”）：

data HList : Vect n Type -> Type  where
  Nil : HList []
  (::) : (x : a) -> (xs : HList as) -> HList (a :: as)

这里是使用 HList 的 zip2 函数的变体：

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

我错过了什么？我是否以错误的方式使用隐式参数？我需要写一些证明吗？有没有更好的方法来构造函数类型签名？

（我的 Idris 版本是1.3.1-git:a93d8c9。）

编辑：使用 HTNW 的代码我仍然得到基本相同的错误：

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])

Answer 1

你也必须匹配types。通过匹配types，您还揭示了有关vects len types 的一些信息，这使您可以进一步匹配HList (vects len types) 参数。此外，types 上的 S n 长度要求是不必要的且已损坏。最后，我认为您实际上需要先递归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 本身非常简单：

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