I am learning dependent pairs in idris and couldn't understand how one can use it. For example, if I filter a Data.List, I get back a Data.List, which you I do sum or other computations on.
sum $ filter (< 3) [1,2,3,4]
3
But if I filter a Data.Vect, I get a dependent pair:
:t filter (< 3) (fromList [1,2,3,4])
filter (\arg => arg < 3) (fromList [1, 2, 3, 4]) : (p : Nat ** Vect p Integer)
Obviously, the result of filter is no longer a normal Vect. Instead, it's (p : Nat ** Vect p Integer). I read that this can be interpreted as Vect p Integer for some p. But I am not sure how to do computation with it. A naive attempt the List way is a type error:
sum $ filter (< 3) (fromList [1,2,3,4])
Error: Sorry, I can't find any elaboration which works. All errors:
...
Hence the question,
How can I compute sum, map (or even filter itself) on the items in the dependent pair that's returned from Vect.filter?
(This is with idris2 0.6.0)
Dependent pair has fields fst and snd to extract values:
Main> sum $ snd $ filter (< 3) (fromList [1,2,3,4])
3
Main> fst $ filter (< 3) (fromList [1,2,3,4])
2