[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?