There is filter : (a -> Bool) -> List a -> List a for List, but there is no filter : (a -> Bool) -> Stream a -> Stream a for Stream, why?
Is there some alternatives to do the similar jobs?
Functions in Idris are total by default, and the totality checker will rightly refuse to accept filter on streams, which is a somewhat canonical example of a non-productive definition on a coinductive type: what would filter isEven return when applied to the stream of odd nats?
Check Productive Coprogramming with Guarded Recursion, where you will find this very same example and a nice intro to totality in the context of coinductive types.