The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

Micah (1) [Avatar] Offline
#1
Hi,

In Section 11.2.2, Executing Infinite Processes, run is defined as follows:

data InfIO : Type where
  Do : IO a -> (a -> Inf InfIO) -> InfIO

run : InfIO -> IO ()
run (Do action cont) = do res <- action
                          run (cont res)


The book says that this function is not total, but when I check it in the repl it says that it is total.

Which is correct?

Thanks,
Micah