Re:Total Functional Programming [pdf]
by ktRolster on Wednesday October 05, 2016 @05:34PM
(#12648106)
The main difficulty is that, very often, I do want my programs to loop forever/indefinitely. (Or at least until someone shuts them down).
Right! That's the point of codata. If you want your program to run forever, you could express e.g. I/O events as an infinite (codata) stream. Then, instead of trying to prove that your program terminates (which it might not), it proves that your program "does something useful" every time it gets an IO event, for a particular practical definition of "doing something useful".
Re:Total Functional Programming [pdf]
by skybrian on Wednesday October 05, 2016 @11:06PM
(#12649930)
Sure, for the main loop. But you probably don't want any function called from the main loop to run forever. (In JavaScript, any single event handler should terminate quickly or it becomes unresponsive.)
Re:Total Functional Programming [pdf]
by SomeStupidPoint on Wednesday October 05, 2016 @07:21PM
(#12648829)
Would it significantly harm your experience if all your programs turned off after 1000 years of execution without input?
If not, your program could be "total" in most of the useful senses, and subparts could have tighter bounds, without any harm.
A program in Haskell can only crash in one way (on a hypothetical computer that doesn't break or run out of RAM): if you write a function that doesn't have an output for every input. You can prevent this through totality checkers such as the one presented in "GADTs meet their match", which you can enable in GHC, the most popular Haskell compiler.
However, programs can still loop forever.
There are several approaches to fix this. One approach is to require recursive functions to monotonically decrease on their arguments. Languages like Idris and Agda support this. The downside is you are no longer Turing complete.
The approach mentioned in the paper is to make a formal distinction between finite and infinite data (data and codata), and in this way you can keep termination checking for functions on finite data, but you also get to keep Turing completeness. What you do instead of proving completeness for functions that might run forever is you prove that the function "does something useful" every time it recurses.