【发布时间】：2017-09-21 07:24:21
【问题描述】：
List有filter : (a -> Bool) -> List a -> List a，Stream没有filter : (a -> Bool) -> Stream a -> Stream a，为什么？
是否有一些替代品可以做类似的工作？
【问题讨论】：
标签： functional-programming idris codata
【发布时间】：2017-09-21 07:24:21
【问题描述】：
默认情况下，Idris 中的函数是总计的，并且总体检查器将正确地拒绝接受流上的过滤器，这是一个关于互感类型的非生产性定义的典型示例：filter isEven 会返回什么 当应用于奇数 nats 流时？
查看Productive Coprogramming with Guarded Recursion，您会在其中找到这个完全相同的示例，以及在协推类型上下文中对整体性的一个很好的介绍。
【讨论】：
-
然后参见。 this paper 由 Bertot 提供，用于在流上有效地定义类似过滤器的函数。