Idris Vect.fromList 与生成列表的用法

Question

我正在尝试进入依赖类型。基于下面 windowl 函数的逻辑，我想要 return 一个向量列表，其长度取决于提供的 size。

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 的文档时，我注意到它说

The length of the list should be statically known.

所以我假设类型错误与 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一直都是）。

Idris Vect.fromList 与生成列表的用法

Idris Vect.fromList usage with generated list

dependent-type

idris