What are the limitations of total functional programming? It is not Turing-complete, but still supports a large subset of the possible programs. Are there important constructs that you could write in a Turing-complete language, but not in a total functional language?And is it correct to say that programs written in total functional languages can be completely statically analysed, while static analysis in Turing-complete languages is limited by things like the halting problem? With that I do not mean that in total functional languages everything can be staticaly determined, because some things are only known at runtime, but I mean that in theory, programs written in an ideal total functional programming language, can be analysed so that everything that could in theory be determined statically can be determined statically. Or are there still undecidable problems inherit in total functional languages that make static analysis incomplete? Some problems will always be undecidable, no matter in which language they are written, but I am interested in such problems that are inherit to the language, like the halting problem in Turing-complete languages.
What are the limits of total functional programming?
computability;pl.programming languages;functional programming
It depends on the total functional language.This answer sounds like a cop-out, but nothing more specific can be said. After all, consider whatever important decidable program that you're interested in. Write a program in your favorite Turing-complete language to solve it. Since the problem is decidable, your program will halt on all inputs.(Arguably, a non-decidable problem could have interesting programs, but not such that people can use, because they'll never be able to wait long enough to know the answer.)Now, define a new language such that it has only one valid input program: the program that you just wrote, with the same semantics as it had before. It's certainly total, since all inputs to all programs written in it (of which there's only one) always terminate.This cheap trick is actually useful: the language Coq, for example, is a total functional language in that no program typechecks unless there is a proof that it terminates. (If you were to waive that requirement, it would be Turing-complete, so the only obstacle is finding a proof of termination.)I'm not sure what you mean by everything that could in theory be determined statically can be determined statically; it sounds tautologically true. Nonetheless, total languages aren't inherently easy to analyze; you know that nothing diverges, which is a useful fact, but the relationship between input and output is still complex. (In particular, there are still infinitely many possible inputs, so you can't exhaustively try them all, even in theory.)