सूची के लिए filter : (a -> Bool) -> List a -> List a है, लेकिन स्ट्रीम के लिए filter : (a -> Bool) -> Stream a -> Stream a नहीं है, क्यों?idris में स्ट्रीम का कोई फ़िल्टर फ़ंक्शन क्यों नहीं है?
क्या समान नौकरियां करने के कुछ विकल्प हैं? इदरिस में
कार्य डिफ़ॉल्ट रूप से कुल रहे हैं, और समग्रता चेकर ठीक ही धाराओं पर फिल्टर है, जो एक coinductive प्रकार पर एक गैर उत्पादक परिभाषा के कुछ विहित उदाहरण है स्वीकार करने के लिए मना कर देगा: क्या filter isEvenवापसी होगा जब लागू किया अजीब जाल की धारा के लिए?
चेक Productive Coprogramming with Guarded Recursion, जहाँ आप यह बहुत ही उदाहरण और coinductive प्रकार के संदर्भ में समग्रता के लिए एक अच्छा परिचय मिल जाएगा।
और सीएफ। [इस पेपर] (https://link.springer.com/chapter/10.1007%2F11417170_9) बर्टोट द्वारा स्ट्रीम पर फ़िल्टर-जैसे फ़ंक्शन की उत्पादक परिभाषा के लिए। – gallais