Как использовать взаимно определенные потоки в Idris? - PullRequest
Новая
       15

Как использовать взаимно определенные потоки в Idris?

0 голосов
/ 10 июня 2018

У меня проблема может быть более общей, чем указано в вопросе.Я пытаюсь заставить работать следующую программу: 

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, но я не знаю, как.

1 Ответ

0 голосов
/ 11 июня 2018

Обратите внимание, что при вызове функции аргументы вычисляются заранее, в частности, в случае разбиения.Здесь в client поток разделяется на регистр с помощью client initreq (req :: reqs), поэтому respsOut в client 0 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) => ...) =
...

Вы можете отложить вычисление respsOut, указав аргумент Lazy: 

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
...