How does one use mutually defined Streams in Idris?

Question

The issue I'm having may be more general than stated in the question. I'm trying to get the following program to work:

module Main
main: IO ()


process: Int -> Int
process req = req+1
server: Stream Int -> Stream Int
client: Int        -> Stream Int -> Stream Int
server (req :: reqs)           = process req :: server reqs
client initreq (resp :: resps) = initreq :: client resp resps
mutual
  reqsOut: Stream Int
  respsOut: Stream Int
  -- This fixes the segfault:
  -- reqsOut  = cycle [1, 2, 3, 4]
  reqsOut  = client 0 respsOut
  respsOut = server reqsOut

main = do
  printLn(take 5 reqsOut)

It will run if I swap out the definition of reqsOut with the commented version, but generates a segmentation fault as is. My guess is I'm using mutual incorrectly, but I'm not sure how.

Answer 1

Note that in function call the arguments gets evaluated beforehand, in particular case splits. Here in client the stream gets case splitted with client initreq (req :: reqs), so respsOut in client 0 respsOut gets evaluated before the delayed tail:

reqsOut =
client 0 respsOut =
client 0 (case respsOut of (req :: reqs) => ...) =
client 0 (case (server regsOut) of (req :: regs) => ...) =
...

You can delay the split with

client initreq stream = initreq :: client (head stream) (tail stream)

But then you'd still have the infinite loop through server:

reqsOut =
client 0 respsOut =
client 0 (server regsOut) =
client 0 (case regsOut of (req :: reqs) => ...) =
...

You can delay the computation of respsOut by making the argument Lazy:

client : Int -> Lazy (Stream Int) -> Stream Int
client initreq stream = initreq :: client (head stream) (tail stream)

And now client can finally construct a Stream Int without evaluating its arguments:

client 0 respsOut =
0 :: Delay (client (head (Force respsOut)) (tail (Force respsOut))) : Stream int