Idris determining result vector length

Question

In Idris, if I want to remove an element based on predicate, there is filter, dropWhile, takeWhile. However, all these functions return a dependent pair (n : Nat ** Vect n elem).

Is there any function that return back as a Vect type?

For what I could think of:

1. Convert a dependent pair to Vect

2. Implement a type that indicate the length vector after transformation (thought I have no idea how), like Here, There

For above ideas, it seems quite cumbersome for 1 (convert every result) or 2 (design each of the type to indicate the result vector length).

Are there any better ways to achieve such behaviour?

dropElem : String -> Vect n String -> Vect ?resultLen String

Answer 1

Maybe this is what you are searching for?

import Data.Vect

count: (ty -> Bool) -> Vect n ty -> Nat
count f [] = 0
count f (x::xs) with (f x)
    | False = count f xs
    | True = 1 + count f xs

%hint
countLemma: {v: Vect n ty} -> count f v `LTE` n
countLemma {v=[]} = LTEZero
countLemma {v=x::xs} {f} with (f x)
    | False = lteSuccRight countLemma
    | True = LTESucc countLemma

filter: (f: ty -> Bool) -> (v: Vect n ty) -> Vect (count f v) ty
filter f [] = []
filter f (x::xs) with (f x)
    | False = filter f xs
    | True = x::filter f xs

Then you con do this:

dropElem: (s: String) -> (v: Vect n String) -> Vect (count ((/=) s) v) String
dropElem s = filter ((/=) s)

You can even reuse the existing filter implementation:

count: (ty -> Bool) -> Vect n ty -> Nat
count f v = fst $ filter f v

filter: (f: ty -> Bool) -> (v: Vect n ty) -> Vect (count f v) ty
filter f v = snd $ filter f v