维基百科有这样的说法：
全函数式编程（也称为强函数式编程，与普通或弱函数式编程相比）是一种编程范式，它将程序的范围限制在可证明终止的程序范围内。
和
这些限制意味着整个函数式编程不是图灵完备的。然而，可以使用的算法集仍然是巨大的。例如，任何已经为其计算了渐近上界的算法都可以通过使用上限作为额外参数来简单地转换为可证明终止的函数，该额外参数在每次迭代或递归时递减。
还有一篇关于Total Functional Programming的论文的 Lambda The Ultimate Post 。
直到上周我在邮件列表中才发现这一点。
是否有更多您知道的资源、参考资料或任何示例实现？
如果我理解正确的话，Total Functional Programming 的意思就是：使用 Total Functions 进行编程。如果我没记错我的数学课程，总函数是在其整个域中定义的函数，部分函数是在其定义中有“漏洞”的函数。
现在，如果您有一个函数，该函数对于某些输入值v进入无限递归或无限循环，或者通常不会以其他方式终止，那么您的函数不是为 定义的v，因此不是部分的，即不是全部的。
Total Functional Programming 不允许您编写这样的函数。所有函数总是为所有可能的输入返回一个结果；并且类型检查器确保是这种情况。
我的猜测是，这极大地简化了错误处理：没有。
您的报价中已经提到了缺点：它不是图灵完备的。例如，操作系统本质上是一个巨大的无限循环。事实上，我们不希望操作系统终止，我们称这种行为为“崩溃”，并为此对我们的计算机大喊大叫！
虽然这是一个老问题，但我认为到目前为止没有一个答案提到完全函数式编程的真正动机，那就是：
如果程序是证明，而证明是程序，那么带有“漏洞”的程序作为证明没有任何意义，并且会引入逻辑不一致。
Basically, if a proof is a program, an infinite loop can be used to prove anything. This is really bad, and provides much of the motivation for why we might want to program totally. Other answers tend to not account for the flip side of the paper. While the languages are techincally not turing complete, you can recover a lot of interesting programs by using co-inductive definitions and functions. We're very prone to think of inductive data, but codata serves an important purpose in these languages, where you can totally define a definition which is infinite (and when doing real computation which terminates, you will potentially use only a finite piece of this, or maybe not if you're writing an operating system!).
It is also of note that most proof assistants work based on this principle, Coq, for example.
Charity 是另一种保证终止的语言：http:
//pll.cpsc.ucalgary.ca/charity1/www/home.html
休谟是一种有 4 个等级的语言。外层是图灵完备的，最内层保证终止：
http ://www-fp.cs.st-andrews.ac.uk/hume/report/