idris - 为什么过滤器基于依赖对？

Question

在 Idris Tutorial过滤向量的函数基于依赖对。

filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter f [] = (_ ** [])
filter f (x :: xs) with (filter f xs )
  | (_ ** xs') = if (f x) then (_ ** x :: xs') else (_ ** xs')

但是为什么有必要把它放在依赖对的角度而不是更直接的东西，比如？

filter' : (a -> Bool) -> Vect n a -> Vect p a

在这两种情况下 p 的类型必须确定，但在我假设的替代方案中，列表 p 的冗余性两次被淘汰。

我天真地尝试实现 filter'失败了，所以我想知道它无法实现是否有根本原因？或者可以 filter'实现，也许 filter在 Idris 中展示依赖对只是一个糟糕的例子吗？但如果是这种情况，那么在什么情况下依赖对是有用的？

谢谢!

Answer 1

filter的区别和 filter'介于存在量化和全称量化之间。如 (a -> Bool) -> Vect n a -> Vect p a是 filter 的正确类型，这意味着 filter返回一个长度为 p 的向量，调用者可以指定 p 应该是什么。