通用 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 ("heterogenous list"):

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

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

（我的 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

通用 zip 函数的左侧从不进行类型检查

Left hand side of a generalized zip function never typechecks

typechecking

idris