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

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 returns 一个长度为 p 的 Vector 并且调用者可以指定 p 应该是什么。

Answer 2

Kim Stebel 的是对的。请注意，早在 2012 年就已经在 Idris 邮件列表中讨论过这个问题 (!!):

filter for vector, a question - Idris Programming Language

我认为 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）隐式依赖于其签名中出现在它之前的（未命名的）谓词和向量。

在此展开，为什么是依赖对？您想要 return 一个向量，但是没有“Vector 长度未知”类型；您需要长度 value 才能获得 Vector 类型。但是你可以想想"OK, I will return a Nat together with a vector with that length"。毫不奇怪，这一对的类型是依赖对的一个例子。更详细地说，依赖对 DPair a P 是由

构建的类型

A型a
函数P: a -> Type

该类型 DPair a P 的值是对值

x: a
y: P a

在这一点上，我认为这只是可能误导您的语法。类型p ** Vect p a是DPair Nat (\p => Vect p a)； p 没有过滤器参数或类似参数。所有这些一开始可能有点令人困惑；如果是这样，也许它有助于将 p ** Vect p a 视为“Vector 未知长度”类型的替代品。

Answer 3

不是答案，而是额外的上下文

Idris 1 文档 - https://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#dependent-pairs

Idris 2 文档 - https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html?highlight=dependent#dependent-pairs

在 Idris 2 中定义的依赖对 here

与 Exists and Subset 相似，但它的两个值都不会在运行时被删除

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

Why is filter based on dependent pair?

idris