5 ms·
I'll give a quick TL;DR of the issues at play; A program in Haskell can only crash in one way (on a hypothetical computer that doesn't break or run out of RAM)
by wyager 10y ago
I'll give a quick TL;DR of the issues at play;
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.
- icen 10y agoBrief nitpick: Idris and Agda both have codata constructions, and in Idris (at least, I'm not familiar with Agda) it is supported by the totality checker.
- ktRolster 10y agoThe main difficulty is that, very often, I do want my programs to loop forever/indefinitely. (Or at least until someone shuts them down).
- wyager 10y agoRight! 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".
- SomeStupidPoint 10y agoWould 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.
- skybrian 10y agoSure, 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.)