为什么在idris中没有Stream的过滤功能？

Question

有filter : (a -> Bool) -> List a -> List aList,但是没有filter : (a -> Bool) -> Stream a -> Stream aStream,为什么？

是否有一些替代方案可以完成类似的工作？

Answer 1

默认情况下,Idris中的函数是完全的,并且整体检查器将正确地拒绝接受流上的过滤器,这是对于共同类型的非生产性定义的一个典型示例:当应用于奇数nat流时会filter isEven 返回什么？

使用Guarded Recursion检查Productive Coprogramming,在这里您可以找到相同的示例,并在coinductive类型的上下文中找到一个很好的介绍.