New answers tagged

4

In these sorts of cases, one idiomatic way is to run it with gas, and to create one non-total gas value to let you finish the program. Yes, perhaps Idris should offer a combinator for IO that allows full streams to be run, but this is sufficient, and doesn't affect the validity of anything else. Seeing this, I'd agree that the IO monad should be coinductive,...


2

As an example where unbounded loops are needed: I can write an emulator for any machine, running in a loop. With unbounded loops, that emulator can run forever. With bounded loops, I must calculate beforehand how long that emulator runs. That calculation might return "the simulator will run for one trillion trillion trillion years", which in theory makes a ...


2

Real world computers are not Turing complete (they have a finite amount of memory) and are equiparable to Linear Bounded Automata. So the easiest way to design a non-Turing-complete language is to design a language that has only a limited amount of memory (the memory can also be a function of the input length) and don't worry about other restrictions. But ...


Top 50 recent answers are included