带有生成列表的 Idris Vect.fromList 用法

Question

我正在尝试进入依赖类型。根据下面windowl函数的逻辑，我想返回一个向量列表，其长度取决于提供的大小。

window : (n : Nat) -> List a -> List (Vect n a)
window size = map fromList loop
  where
    loop xs = case splitAt size xs of
      (ys, []) => if length ys == size then [ys] else []
      (ys, _) => ys :: loop (drop 1 xs)

windowl : Nat -> List a -> List (List a)
windowl size = loop
  where
    loop xs = case List.splitAt size xs of
      (ys, []) => if length ys == size then [ys] else []
      (ys, _) => ys :: loop (drop 1 xs)

当我尝试将该函数加载到 Idris 时，我得到以下信息：

When checking argument func to function Prelude.Functor.map:
    Type mismatch between
            (l : List elem) -> Vect (length l) elem (Type of fromList)
    and
            a1 -> List (Vect size a) (Expected type)
    
    Specifically:
            Type mismatch between
                    Vect (length v0) elem
            and
                    List (Vect size a)

在阅读fromList上的文档时，我注意到它说

列表的长度应该是静态已知的。

所以我假设类型错误与 Idris 不知道列表的长度对应于指定的大小有关。

我被卡住了，因为我什至不知道这是否是我想要做的不可能的事情，或者我是否可以指定列表的长度与我想要生成的向量的长度相对应。

有没有办法做到这一点？

Answer 1

由于在您的情况下无法静态知道长度，因此我们需要一个可能在运行时失败的函数：

total
fromListOfLength : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
fromListOfLength n xs with (decEq (length xs) n)
  fromListOfLength n xs | (Yes prf) = rewrite (sym prf) in Just (fromList xs)
  fromListOfLength n xs | (No _) = Nothing

fromListOfLength将长度列表转换为长度n向量n或失败。现在让我们结合它并windowl获得window.

total
window : (n : Nat) -> List a -> List (Vect n a)
window n = catMaybes . map (fromListOfLength n) . windowl n

观察该window函数的类型仍然是我们所用的输入列表做一个标示不足，因为没有什么阻止我们总是返回空的列表（如果这可能发生fromListOfLength返回Nothing所有的时间）。