[pittma]

Hm, that's not how I'm reading this. An infinite loop is, by definition, partial. What I'm gathering from this is that that stuckness that the typechecker can encounter in the face of partiality is okay in Idris, that its typechecker just says, "welp, this is as far as I go."

[jinwoo68]

I’m specifically talking about the “Produces a non-empty, finite, prefix of a possibly infinite result” part on that page. As long as your server generates finite responses in finite times, Idris recognizes your code as total.

[Shoue]

When dealing with corecursion (infinite streams) you don't care about whether you terminate, but rather, whether the infinite stream is _productive_ meaning it doesn't stop producing values. The prime example of a function that's impossible(?) to prove productive (for all cases) is filter – since it takes a predicate function that decides whether values are returned or not. If you give filter a predicate that always returns false you will never produce any values, hence that wouldn't be productive.

[kryptiskt]

If you have codata you can have infinite loops in total functional programming.

https://en.wikipedia.org/wiki/Corecursion