There's a common belief floating around that total functions are an essential component of functional programming. I suppose there's growing demand for developing in Turing-incomplete languages.
Of course, there'll always be things you can't decide. The challenge is to learn how to spot more of them. But even within current constraints, you can still have Turing completeness.
-
-
But presumably TC is only attainable once you invoke the general recursion effect, where reasoning about termination is forsaken, as far as the type checker is concerned.
-
The idea is that you can describe general recursion, or partiality, in much the same way as you can describe interactive programs.
- 3 more replies
New conversation -
-
-
Buchberger’s algorithm jumps to mind. We know that it terminates, however this assumes a weak version of AC. Is there a way in Idris to declare a function to be total even if the type checker cannot prove this, an unsafePerformIO for total functions?
-
You can assert totality, at least.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.