5
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ So, the way that we've mixed stream-like ideas with IO in idris has been through monadic stream functions, which separate the idea of two monadic computations that are related causally to one another, from the effects themselves. And, of course, idris gets a bit confused trying to prove termination, and also because the way that the monad wraps the continuation in MSFs could have adverse effects if it's not strictly positive. $\endgroup$ – Ivan Perez Oct 2 at 0:57
  • 1
    $\begingroup$ Now, with indexed monads or a similar idea, which I have used for fault tolerance annotations in MSFs, perhaps we could say that an MSF is terminating in a maximum number of steps, or not at all (unless it crashes). $\endgroup$ – Ivan Perez Oct 2 at 1:01
4
$\begingroup$

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
$\endgroup$
  • 1
    $\begingroup$ Thanks; good to see an example of how to do this. Strictly though it's still not a total solution. $\endgroup$ – Kazark Oct 2 at 13:53
  • 2
    $\begingroup$ Yes, in Idris the language, IO is inductive, not coinductive, so this is the only solution in this particular language today. It's not related to totality in general though, one should just have a top level that supports it. But ultimately that means that your stream is fine, there just needs to be an interface for it. $\endgroup$ – Jason Carr Oct 2 at 20:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.