Can a total programming language be Turing-complete?

Question

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.

Answer 1

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.