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?
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?
Copyright © 2021 Jogjafile Inc.
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 isEvenreturn 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.