idrisにStreamのフィルタ機能がないのはなぜですか？

Question

Listにはfilter : (a -> Bool) -> List a -> List aがありますが、Streamにはfilter : (a -> Bool) -> Stream a -> Stream aがありません。なぜですか？

似たような仕事をするいくつかの選択肢がありますか？イドリスで

Answer 1

関数は、デフォルトでは、合計で、全体チェッカーが正しくcoinductiveタイプで非生産的な定義の幾分標準的な例であるストリームにフィルタを受け入れることを拒否します：filter isEvenリターン印加なるとき何奇妙なナットの流れに？

「Productive Coprogramming with Guarded Recursion」をチェックしてください。ここでは、この同じ例と、完全誘導性について、誘導性タイプのコンテキストで紹介しています。