13

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?

luochen1990
  • 3,689
  • 1
  • 22
  • 37

1 Answers1

13

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.

Eduardo Pareja Tobes
  • 3,060
  • 1
  • 18
  • 19
  • 3
    And cf. [this paper](https://link.springer.com/chapter/10.1007%2F11417170_9) by Bertot for a productive definition of a filter-like function on streams. – gallais Apr 24 '17 at 16:13