什么是"全功能编程"？

维基百科有这样的说法:

总函数编程(也称为强函数编程,与普通或弱函数编程形成对比)是一种编程范例,它将程序范围限制为可证明终止的程序范围.

和

这些限制意味着整个函数式编程不是图灵完备的.但是,可以使用的算法集仍然很大.例如,通过使用上限作为额外参数(其在每次迭代或递归时递减),可以将具有为其计算的渐近上界的任何算法简单地转换为可证明终止的函数.

还有一篇关于全功能编程的论文的Lambda The Ultimate Post .

直到上周我才在邮件列表上看到过这个问题.

您知道更多的资源,参考或任何示例实现吗？

1> Jörg W Mitta..：

---

如果我理解正确,那么全功能编程就意味着:用全部函数编程.如果我正确记住我的数学课程,则总函数是在整个域中定义的函数,部分函数是在其定义中具有"洞"的函数.

现在,如果你有一个函数,对于某些输入值v进入无限递归或无限循环或一般不以其他方式终止,那么你的函数没有被定义v,因此是部分的,即不是总的.

Total Functional Programming不允许您编写这样的函数.所有功能始终返回所有可能输入的结果; 并且类型检查器确保这种情况.

我的猜测是,这极大地简化了错误处理:没有任何错误处理.

您的报价中已经提到了缺点:它不是图灵完备的.例如,操作系统本质上是一个巨大的无限循环.实际上,我们不希望操作系统终止,我们将此行为称为"崩溃",并对我们的计算机大喊大叫!

---

我不同意,如果您阅读论文和帖子,您可以拥有"永远运行"的总功能,它只是一个共同定义的功能,而不是归纳定义的功能,这正是_how_您使用此方法编写操作系统编程.

2> Kristopher M..：

---

虽然这是一个老问题,但我认为迄今为止没有一个答案提到了全功能编程的真正动机,这就是:

如果程序是证明,并且证明是程序,则具有"漏洞"的程序作为证据没有任何意义,并且引入逻辑不一致.

基本上,如果证明是程序,则可以使用无限循环来证明任何事物.这真的很糟糕,并提供了我们为什么要完全编程的动机.其他答案往往不考虑论文的另一面.虽然这些语言在技术上并不完整,但您可以通过使用共感应定义和函数来恢复许多有趣的程序.我们很容易想到归纳数据,但是在这些语言中,codata是一个重要的目的,在这些语言中你可以完全定义一个无限的定义(当进行真正的计算终止时,你可能只使用一个有限的部分,或者如果您正在编写操作系统,可能不会!).

值得注意的是,大多数证据助理都是基于这个原则工作的,例如Coq.

3> ja...：

---

慈善机构是另一种保证终止的语言:http:
//pll.cpsc.ucalgary.ca/charity1/www/home.html

休谟是一种4级语言.外层是图灵完成,最内层保证终止:http:
//www-fp.cs.st-andrews.ac.uk/hume/report/