Why there is no filter function of Stream in idris?

Question

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?

Dallman

Answer 1

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.

Gronseth

And cf. this paper by Bertot for a productive definition of a filter-like function on streams. – Carlie