functional-programming - 为什么idris中没有Stream的过滤功能？

Question

filter : (a -> Bool) -> List a -> List aList 有，Stream 没有，filter : (a -> Bool) -> Stream a -> Stream a为什么？

有没有其他方法可以做类似的工作？

Answer 1

Idris 中的函数默认是总计的，并且总体检查器将正确地拒绝接受流上的过滤器，这是一个关于共归纳类型的非生产性定义的典型示例：应用于奇数 nat 流时会filter isEven 返回什么？

检查Productive Coprogramming with Guarded Recursion，您会在其中找到这个完全相同的示例，以及在协推类型的上下文中对整体性的一个很好的介绍。