6
$\begingroup$

I've seen two answers to this:

Wikipedia says no:

These restrictions mean that total functional programming is not Turing-complete.

And the Wikipedia article cites D.A. Turner as the coiner of "total functional programming," and Turner says on page 755 of Total Functional Programming:

There are two obvious disadvantages of total functional programming

  1. Our programming language is no longer Turing complete
  2. If all programs terminate, how do we write an operating system?

But Conor McBride says total programming languages can be Turing-complete:

Now represent the semantics of Turing machines as coinductive processes and review your hasty and inaccurate repetition of the common falsehood that totality prevents Turing-completeness. You exactly get to say “we know how to run it for as long as we’re willing to wait, but we can’t promise you it will stop”, which is both the truth, and exactly the deal when you work in a partial language. The only difference is that when you promise something does work, you’re believable. The expressive weakness is on the partial side.

Turner had indeed thought about codata, and it plays a big role in their article re problem (2), but they don't seem to think codata helps with (1).

Would an answer to McBride's Retort be something like:

Re "Now represent the semantics of Turing machines as coinductive processes ..." A Universal Turing Machine won't halt (if executing a program with an infinite loop), but a copgram will always halt until someone asks it to compute some more: to actually do computation for infinite time rather than just representing an infinite computation requires non-termination.

Improve this question
$\endgroup$
7
$\begingroup$

I'm pretty sure McBride isn't claiming that a total programming language can be Turing complete, just that it's a useless distinction in practice. You can take any program in a partial language and replace all not-provably-terminating loops with loops that run at most $2^{128}$ times, and the result is theoretically different but not observably different.

You exactly get to say “we know how to run it for as long as we’re willing to wait, but we can’t promise you it will stop”, which is [...] exactly the deal when you work in a partial language.

I.e. maximum run times are bounded in the real world.

The only difference is that when you promise something does work, you’re believable. The expressive weakness is on the partial side.

I.e. there's an expressivity tradeoff in using total vs partial languages, but the expressive advantage of total languages is useful in practice, while the theoretical expressive advantage of partial languages has no practical consequence.

Edit: In response to OP's comment, I think ruakh's comment is correct. McBride is implicitly suggesting that a better notion of completeness ought to not only replace Turing completeness as the de facto standard for real-world languages, but also take the name of Turing completeness and the brand identity associated with it, because it's more deserving of it. Maybe it would be more accurate to say he thinks the better notion of completeness ought to have been called Turing completeness from the beginning. It matters because the perception that total languages are deficient in some practical way, due to their lack of Turing completeness, may have actually hindered their real-world adoption.

Improve this answer
$\endgroup$
3
  • 4
    $\begingroup$ +1, but given McBride's reference to "the common falsehood that totality prevents Turing-completeness", I think he is indeed arguing that a total language can be Turing-complete; in essence, he seems to be arguing against the standard definition of "Turing-completeness", insofar as that definition assumes a distinction between a program that completes after a gazillion years and a program that never completes (whereas in real life neither one would actually be allowed to run to completion). $\endgroup$ – ruakh Dec 12 '20 at 8:46
  • $\begingroup$ McBride is specifically pointing at conduction right? That means a process that generates structure and doesn't consume it. In this sense, it can generate structure forever without terminating, but we know that the step between coiterations is provably sound. $\endgroup$ – J_mie6 Dec 12 '20 at 9:12
  • $\begingroup$ Thanks for your answer. I'm sorry to vote down, but I can't find any correspondence between your explanation and what McBride wrote. As @ruakh pointed out, McBride is very clearly saying that the statement is false, not that, as you say, that the distinction is "a useless distinction in practice." And your point about "losing a degree of theoretical expressiveness" is the opposite of what McBride is saying. He says total languages are more expressive!! (right there in your second quote) $\endgroup$ – Max Heiber Dec 12 '20 at 14:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.