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

Question

在Idris教程中,用于过滤矢量的函数基于从属对.

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只是在伊德里斯展示依赖对的一个不好的例子？但如果是这种情况那么在什么情况下依赖对会有用呢？

谢谢!

Answer 1

之间的区别filter,并filter'为生存和通用量化之间.如果(a -> Bool) -> Vect n a -> Vect p a是正确的类型filter,那意味着filter返回长度为p的Vector,调用者可以指定p应该是什么.

Answer 2

金·斯特贝尔的答案是正确的。让我注意一下，早在2012年（Idris）就已在Idris邮件列表中进行了讨论（!!）：

• 矢量过滤器，一个问题-Idris编程语言

什么raichoo贴有能帮助澄清它，我认为; 您的真实签名filter'是

filter' : {p : Nat} -> {n: Nat} -> {a: Type} -> (a -> Bool) -> Vect a n -> Vect a p

从中可以明显看出，这不是过滤器应该（甚至不能）执行的操作；p实际上取决于谓词和要过滤的向量，您可以（实际上需要）使用一个依赖对来表达它。请注意，在（）中(p ** Vect p a)，p（因此Vect p a）隐含地依赖于（未命名）谓词和向量在其签名之前出现。

对此进行扩展，为什么要有一对依赖？您想返回一个向量，但是没有“ Vector长度未知”的类型。您需要一个长度值来获取Vector类型。但是，您可以认为“好吧，我将返回一个Nat带有该长度的向量”。毫无疑问，该对的类型是相关对的示例。更详细地讲，从属对DPair a P是基于

1. 一种 a
2. 功能 P: a -> Type

该类型的值DPair a P是一对值

1. x: a
2. y: P a

在这一点上，我认为这只是语法，可能会误导您。类型p ** Vect p a 是 DPair Nat (\p => Vect p a) ; p没有用于filter或类似参数的参数。起初，所有这些可能会使您感到困惑。如果是这样，也许可以帮助您考虑p ** Vect p a替代“ Vector长度未知”类型。