I'll give a quick TL;DR of the issues at play;<p>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.<p>However, programs can still loop forever.<p>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.<p>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.
This is a very good explaination of that topic, creating languages which are not turing complete but still useful.<p>Also, I recommend reading Harper's throughts about it:<p><i>"Old Neglected Theorems Are Still Theorems"</i> <a href="https://existentialtype.wordpress.com/2014/03/20/old-neglected-theorems-are-still-theorems/" rel="nofollow">https://existentialtype.wordpress.com/2014/03/20/old-neglect...</a><p>It also reminds me of the NASA coding standards, rule 4:<p><i>"All loops must have a fixed upper-bound"</i>, see <a href="http://pixelscommander.com/en/javascript/nasa-coding-standarts-for-javascript-performance/" rel="nofollow">http://pixelscommander.com/en/javascript/nasa-coding-standar...</a><p>(Related HN discussion: <a href="https://news.ycombinator.com/item?id=8856226" rel="nofollow">https://news.ycombinator.com/item?id=8856226</a>)
Related to this, Idris has a totality checker. It does not require totality, however.<p><a href="http://docs.idris-lang.org/en/latest/tutorial/theorems.html#directives-and-compiler-flags-for-totality" rel="nofollow">http://docs.idris-lang.org/en/latest/tutorial/theorems.html#...</a>
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 <i>not</i> 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.<p>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)<p><a href="https://hackernoon.com/smart-contracts-turing-completeness-reality-3eb897996621#.heipbfzgf" rel="nofollow">https://hackernoon.com/smart-contracts-turing-completeness-r...</a>
[...] We consider a simple discipline of total functional programming designed to exclude the possibility of non-termination. [...]<p>So the idea seems to be a programming framework that on one hand guarantees termination, while on the other hand is sufficiently powerful to be useful. That is "useful despite being sub-turing".<p>I spent some time causally studying the subject of sub-turing languages, and found something notable. If a language guarantees that all its programs consume input as they go, that program is guaranteed to terminate, and so the language itself is sub-turing. One example of such program could be a compiler, which makes for a great example of a useful application of a sub-turing language.<p>It's a fascinating subject because sub-turing language programs are a lot easier to analyze.
I'm still a little unclear on what we would achieve by making the language 'complete.' I get that being able to check for non-termination would be useful—but is there more?<p>The paper opens with:<p><i>The driving idea of functional programming is to make programming more closely related to mathematics.</i><p>From a paper by John Backus:<p><i>Associated with the functional style of programming is an algebra of programs whose variables range over programs and whose operations are combining forms. This algebra can be used to transform programs and to solve equations whose “unknowns” are programs in much the same way one transforms equations in high school algebra.</i><p>Are they talking about the same thing here?<p>Also, are there advantages to having such an algebra of programs outside of correctness verification?
Super interesting reading, thank you. Does anyone know similar papers on functional programming? I've sometimes found some that were much more difficult to read if you're not a mathematician.
I love this paper. The idea of non-Turing-complete languages that are quite useful for real work (whatever that means) is such a fascinating concept. Knowing at compile time that my program won't run off in unending or unproductive code seems like such a useful bit of static checking.<p>There are also essentially no total languages today. Idris, Coq, etc. have support for totality, but there's nothing widespread or simple that does. I expect a total language would be quite useful in certain contexts (real-time, scripting, running user code, compilers), but the drive for - I can do whatever I want in this language - is so strong that a total language would need to provide significant, useful advantages to see adoption.
I was recently introduced to functional programming when I started learning Elixir. There seems to be so much potential with Elixir and I am not kidding when I say that learning the concepts of functional programming was one of the more "mind bending" ventures I have taken. I don't mean this in a negative way. If anything, it opened my mind to think about problem solving/programming in a completely different way.<p>For example, something as simple as <i>assigning</i> a variable has so much more meaning and functionality than I am used to, thanks to pattern matching.<p>I look forward to diving deeper into functional programming. Thanks for posting.
The Charity language appears to fit into this mold:<p><a href="https://en.wikipedia.org/wiki/Charity_(programming_language)" rel="nofollow">https://en.wikipedia.org/wiki/Charity_(programming_language)</a><p>Very interesting stuff.
The second paragraph of the text refers to "the functional subset of Standard ML"; does that mean Standard ML less reassignment of references?