全函数式编程（Total Functional Programming）

导读

这篇论文讨论总函数式编程（total functional programming）：如何通过类型系统与终止性/生产性检查，避免函数对某些输入无输出或陷入无限循环。评论将其核心手段概括为区分有限数据 data 与无限 codata，对有限数据上的递归要求终止，对可能无限的过程要求每次递归都产生有用输出。它也涉及用受限递归换取更强的程序性质证明能力。

HN 关注点：总函数式编程与终止检查如何在实用性、图灵完备性和可证明性之间取舍。

关键词　total functional programmingdata/codatatermination checkingHaskell

HN 评论精选

这几条评论里：补充 4

补充梳理 Haskell 的失败模式，并解释 data/codata 如何在终止检查与图灵完备之间折中。

快速梳理一下问题：在理想机器（不崩溃、内存无限）上，Haskell 程序只有一种崩溃方式——函数对某个输入没有输出；可用 GHC 的 totality checker（如“GADTs meet their match”）防止。但程序仍可能死循环。解决方式包括要求递归函数参数单调递减（Idris、Agda 支持），代价是失去图灵完备；论文提出 data/codata 区分，对有限数据保留终止检查，对可能无限的函数则证明每次递归都“产出有用东西”，从而保留图灵完备。

wyager查看英文原文

I'll give a quick TL;DR of the issues at play; A program in Haskell can only crash in one way (on a hypothetical computer that doesn't break or run out of RAM): if you write a function that doesn't have an output for every input. You can prevent this through totality checkers such as the one presented in "GADTs meet their match", which you can enable in GHC, the most popular Haskell compiler. However, programs can still loop forever. There are several approaches to fix this. One approach is to require recursive functions to monotonically decrease on their arguments. Languages like Idris and Agda support this. The downside is you are no longer Turing complete. The approach mentioned in the paper is to make a formal distinction between finite and infinite data (data and codata), and in this way you can keep termination checking for functions on finite data, but you also get to keep Turing completeness. What you do instead of proving completeness for functions that might run forever is you prove that the function "does something useful" every time it recurses.

补充补充相关阅读与工业编码标准作为参照。

这是对该话题很好的解释：如何做出非图灵完备但仍然有用的语言。也推荐 Harper 的《Old Neglected Theorems Are Still Theorems》，并让人想到 NASA 编码标准第 4 条：所有循环必须有固定上界。

vog查看英文原文

This is a very good explaination of that topic, creating languages which are not turing complete but still useful. Also, I recommend reading Harper's throughts about it: "Old Neglected Theorems Are Still Theorems" https://existentialtype.wordpress.com/2014/03/20/old-neglected-theorems-are-still-theorems/ It also reminds me of the NASA coding standards, rule 4: "All loops must have a fixed upper-bound", see http://pixelscommander.com/en/javascript/nasa-coding-standarts-for-javascript-performance/ (Related HN discussion: https://news.ycombinator.com/item?id=8856226)

补充指出 Idris 提供可选的终止性检查。

相关地，Idris 有 totality checker，但并不强制要求 totality。

thecity2查看英文原文

Related to this, Idris has a totality checker. It does not require totality, however. http://docs.idris-lang.org/en/latest/tutorial/theorems.html#directives-and-compiler-flags-for-totality

补充真正优势是程序性质易证，终止只是附带；并澄清 Rice 定理常被误用。

只强调“总终止”会低估这些限制的一个关键优势：你能更容易证明程序的通用性质。这不是总终止的必然结果——有些总语言仍允许性质不可判定的程序；这个语言真正是让性质容易证明，终止只是其中之一。这个话题常出现在公链智能合约讨论中，人们也常误解 Rice 定理。

murbard2查看英文原文

The focus on "totality" undersells one key advantage of the restrictions in this language. You gain the ability to easily prove general properties about your program. This is not a consequence of totality. There are total programming languages which allow you to write programs with undecidable properties. This is really a language where properties are easy to prove, and termination happens to be one of them. The topic often comes up in the discussion of smart contracts on public blockchains, and people often get confused about what Rice's theorem says. I recently did a small write up on the topic (plug, plug) https://hackernoon.com/smart-contracts-turing-completeness-reality-3eb897996621#.heipbfzgf

历次讨论

2016Hacker News 讨论帖207 分 · 79 评

HN 二十年，最值得读的论文。

朋友分享的书单

专题阅读路线

本周最多人读

我的书单

必读 30 篇

论文库

这些论文是怎么挑出来的

全量扫一遍

只留论文本身

写导读、译评论

全函数式编程（Total Functional Programming）

导读

HN 评论精选

相关资源

历次讨论

同领域还值得读

Google 的软件工程（2017）

Peter Naur：编程作为理论构建 (1985)

SciPy 1.0：Python 科学计算的基础算法

Lisp 的历史（1979）

使用 NumPy 进行数组编程

打赏支持

关注向阳乔木