title: Why is filter based on dependent pair?
body: <p>In the <a href="http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html" rel="noreferrer">Idris Tutorial</a> a function for filtering vectors is based on dependent pairs.</p>
  
  <pre><code>filter : (a -&gt; Bool) -&gt; Vect n a -&gt; (p ** Vect p a)
  filter f [] = (_ ** [])
  filter f (x :: xs) with (filter f xs )
    | (_ ** xs') = if (f x) then (_ ** x :: xs') else (_ ** xs')
  </code></pre>
  
  <p>But why is it necessary to put this in terms of a dependent pair instead of something more direct such as?</p>
  
  <pre><code>filter' : (a -&gt; Bool) -&gt; Vect n a -&gt; Vect p a
  </code></pre>
  
  <p>In both cases the type of <code>p</code> must be determined, but in my supposed alternative the redundancy of listing <code>p</code> twice is eliminated.</p>
  
  <p>My naive attempts at implementing <code>filter'</code> failed, so I was wondering is there a fundamental reason that it can't be implemented? Or can <code>filter'</code> be implemented, and perhaps <code>filter</code> 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?</p>
  
  <p>Thanks!</p>