How to write a coterminating, effectful program?

Question

^{[Using Idris for code examples and terminology, but the question is not about Idris per se]}

In a post titled A Neighborhood of Infinity, @sigfpe argues that "the kind of open-ended loop we see in operating systems and interactive applications" is to be modeled mathematically using codata, and that these sorts of programs can even written in a total functional programming language if they found to coterminate. Though I don't yet understand this to the depth in which he lays it out, the idea makes sense, and I'm familiar with the fact that Idris' totality checker (for example) considers cotermination. Thus, we might write the Unix yes program thus:

yes : Stream String
yes = "yes" :: yes

—except that this is not Unix yes, but intra-Idris yes. I cannot run this program and have it do what yes does: I need an effectful program. Stream is a Functor; it seems I want a main : Stream (IO ()). Let me make the example slightly more compelling by making this an interactive program, as @sigfpe speaks of:

stopOrPrint : String -> IO ()
stopOrPrint s = do
  maybeQ <- getChar
  if maybeQ == 'q'
  then pure ()
  else putStrLn s

main : Stream (IO ())
main = map stopOrPrint yes

But Idris does not accept programs whose main function has type Stream (IO ()). No problem, maybe if I used traverse_ : Foldable t => Applicative f => (a -> f b) -> t a -> f () instead of map, I could get a main with the right type, IO (). However Stream is not a Foldable, and I'm thinking it's not just because Brady forgot to implement it: how do you guarantee that you can fold a potentially infinite value into a finite value? Isn't that kind of crossing over from infinitude to finitude the opposite of totality?

So I'm stuck. I love the idea that with codata and cotermination, we could write a total operating system or even server. But when I actually go to write a socket server in Idris, I end up marking stuff partial; yet Idris' totality checker respects these ideas.

Am I running into a limitation of Idris (or any languages currently in existence), or a more fundamental limitation? If Idris just learned to take a Stream (IO ()) for its main, would that solve it? I have a feeling that still doesn't address the underlying issue, because now you have a bunch of disconnected IOs: don't you actually want an infinite IO monad (can there be such a thing?)?

Is it possible to mix cotermination and effects, in a pure, total functional language? Has it been done? If not, what would it have to look like?

Answer 1

In these sorts of cases, one idiomatic way is to run it with gas, and to create one non-total gas value to let you finish the program. Yes, perhaps Idris should offer a combinator for IO that allows full streams to be run, but this is sufficient, and doesn't affect the validity of anything else.

Seeing this, I'd agree that the IO monad should be coinductive, not inductive.

%default total

data Gas : Type where
  More : Lazy Gas -> Gas
  Done : Gas

runStream : Gas -> Stream (IO ()) -> IO ()
runStream (More g) (i :: is) = i >>= \_ => runStream g is
runStream Done _ = pure ()

partial
unbounded : Gas
unbounded = More unbounded