Why is the filter based on a dependent pair?

Question

In the Idris Tutorial, the 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 should we put this in terms of a dependent pair instead of something more direct, for example?

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

In both cases, the type pmust be defined, but in my proposed alternative, listing redundancy is eliminated p.

My naive attempts to realize filter'failed, so I was wondering if there is a fundamental reason that it cannot be realized? Or could it be implemented filter', and perhaps filterwas just a bad example for a showcase of dependent couples in Idris? But if so, in which situations can dependent pairs be useful?

Thank!

Answer 1

. , Idris 2012 (!!):

• , -

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 ,

• 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 2

filter filter' . (a -> Bool) -> Vect n a -> Vect p a filter, , filter p, , p.