Why is filter based on dependent pair?

Question

In the Idris Tutorial a function for filtering vectors is based on dependent pairs.

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')

But why is it necessary to put this in terms of a dependent pair instead of something more direct such as?

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

In both cases the type of p must be determined, but in my supposed alternative the redundancy of listing p twice is eliminated.

My naive attempts at implementing filter' failed, so I was wondering is there a fundamental reason that it can't be implemented? Or can filter' be implemented, and perhaps filter was just a poor example to showcase dependent pairs in Idris? But if that is the case then in what situations would dependent pairs be useful?

Thanks!

Answer 1

The difference between filter and filter' is between existential and universal quantification. If (a -> Bool) -> Vect n a -> Vect p a was the correct type for filter, that would mean filter returns a Vector of length p and the caller can specify what p should be.

Answer 2

Kim Stebel's answer is right on the money. Let me just note that this was already discussed on the Idris mailing list back in 2012 (!!):

• filter for vector, a question - Idris Programming Language

What raichoo posted there can help clarifying it I think; the real signature of your filter' is

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

from which it should be obvious that this is not what filter should (or even could) do; p actually depends on the predicate and the vector you are filtering, and you can (actually need to) express this using a dependent pair. Note that in the pair (p ** Vect p a), p (and thus Vect p a) implicitly depends on the (unnamed) predicate and vector appearing before it in its signature.

Expanding on this, why a dependent pair? You want to return a vector, but there's no "Vector with unknown length" type; you need a length value for obtaining a Vector type. But then you can just think "OK, I will return a Nat together with a vector with that length". The type of this pair is, unsurprisingly, an example of a dependent pair. In more detail, a dependent pair DPair a P is a type built out of

1. A type a
2. A function P: a -> Type

A value of that type DPair a P is a pair of values

1. x: a
2. y: P a

At this point I think that is just syntax what might be misleading you. The type p ** Vect p a is DPair Nat (\p => Vect p a); p there is not a parameter for filter or anything like it. All this can be a bit confusing at first; if so, maybe it helps thinking of p ** Vect p a as a substitute for the "Vector with unknown length" type.