如何在 Idris 中使用相互定义的流？答案

【问题标题】：How does one use mutually defined Streams in Idris?如何在 Idris 中使用相互定义的流？
【发布时间】：2018-11-19 23:48:55
【问题描述】：

我遇到的问题可能比问题中所述的更为笼统。我正在尝试让以下程序运行：

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)

如果我将reqsOut 的定义替换为注释版本，它将运行，但会按原样生成分段错误。我的猜测是我错误地使用了mutual，但我不确定如何使用。

【问题讨论】：

标签： idris

【解决方案1】：

请注意，在函数调用中，参数会被预先评估，特别是在拆分的情况下。在client 中，流与client initreq (req :: reqs) 分开大小写，因此client 0 respsOut 中的respsOut 在延迟尾部之前被评估：

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

您可以延迟拆分

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

但是你仍然有通过server的无限循环：

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

您可以通过设置参数Lazy 来延迟respsOut 的计算：

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

现在client 终于可以构造一个Stream Int 而无需评估它的参数：

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

【讨论】：