13 ms·

Total Functional Programming [pdf]

207 points by adgasf 10y ago

almata 10y ago
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.
- dj-wonk 10y ago
  You might also want to check out "Functional Programming, Totally" by Keanu Reeves.
DenisM 10y ago
[...] We consider a simple discipline of total functional programming designed to exclude the possibility of non-termination. [...] 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". 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. It's a fascinating subject because sub-turing language programs are a lot easier to analyze.
- lomnakkus 10y ago
  > That is "useful despite being sub-turing". This has been called being "Pacman Complete" by Edwin Brady. I very nice catchy term, IMO.
  - skybrian 10y ago
    I like that. A search doesn't find anything relevant, though. Got a reference?
    - 14113 10y ago
      Edwin didn't coin it - but he did popularise it: https://twitter.com/edwinbrady/status/384671269490540544 https://twitter.com/edwinbrady/status/384671269490540544
      - lomnakkus 10y ago
        Ah, nice reference. The first time I heard it used was in one of his talks.
- barrkel 10y ago
  A compiler is, at a high level, just a function. And most architectural breakdowns of compilers turn them into sequences of functions, like: link(codegen(analyze(typecheck(parse(lex(source)))))) And compilers are one of the easiest kinds of programs to write naturally in a functional language.
swordbeta 10y ago
Any mirror? "You have exceeded your daily download allowance"
- bazzargh 10y ago
  The original journal the paper was published in has it: http://www.jucs.org/jucs_10_7/total_functional_programming http://www.jucs.org/jucs_10_7/total_functional_programming
  - agumonkey 10y ago
    Lots of cool issues http://www.jucs.org/jucs_2 http://www.jucs.org/jucs_2
- sndean 10y ago
  http://sblp2004.ic.uff.br/papers/turner.pdf http://sblp2004.ic.uff.br/papers/turner.pdf or http://www.mpi-sws.org/~skilpat/plerg/papers/turner-total-fp-2up.pdf http://www.mpi-sws.org/~skilpat/plerg/papers/turner-total-fp...
vog 10y ago
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/ https://existentialtype.wordpress.com/2014/03/20/old-neglect... 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/ http://pixelscommander.com/en/javascript/nasa-coding-standar... (Related HN discussion: https://news.ycombinator.com/item?id=8856226 https://news.ycombinator.com/item?id=8856226)
- wyager 10y ago
  The approach given in the paper explicitly allows for Turing completeness through the use of data/codata types. Instead of proving termination over codata you prove that a function "does something useful" every iteration.
  - willtim 10y ago
    You would of course need to factor out the outer-loop to do this. But it seems even this is not necessary. This paper discusses using total languages to build generally recursive (Turing complete) computations as an effect monad: https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree....
    - wyager 10y ago
      > You would of course need to factor out the outer-loop to do this What are you referring to? Data/codata checking works with local type inference.
      - mkehrt 10y ago
        Essentially, to get a nonterminating, program, your top level function needs to take a piece of codata to corecurse over to run indefinitely. Since you can't actually write a program that takes no arguments that produces an infinite piece of data, all programs must terminate.
wyager 10y ago
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.
- icen 10y ago
  Brief nitpick: Idris and Agda both have codata constructions, and in Idris (at least, I'm not familiar with Agda) it is supported by the totality checker.
- ktRolster 10y ago
  The main difficulty is that, very often, I do want my programs to loop forever/indefinitely. (Or at least until someone shuts them down).
  - wyager 10y ago
    Right! That's the point of codata. If you want your program to run forever, you could express e.g. I/O events as an infinite (codata) stream. Then, instead of trying to prove that your program terminates (which it might not), it proves that your program "does something useful" every time it gets an IO event, for a particular practical definition of "doing something useful".
  - SomeStupidPoint 10y ago
    Would it significantly harm your experience if all your programs turned off after 1000 years of execution without input? If not, your program could be "total" in most of the useful senses, and subparts could have tighter bounds, without any harm.
snake117 10y ago
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. For example, something as simple as assigning a variable has so much more meaning and functionality than I am used to, thanks to pattern matching. I look forward to diving deeper into functional programming. Thanks for posting.
- sotojuan 10y ago
  There's a lot to explore! Elixir is my favorite "new" language, and its style of functional programming is accessible and practical yet still very didactic. That said, there's always more mind bending things out there once you've digester Elixir. I'm experiencing a similar thing with Haskell at the moment.
- chriswarbo 10y ago
  > For example, something as simple as assigning a variable has so much more meaning and functionality than I am used to, thanks to pattern matching. Once I grokked FP, I started thinking about this the other way around. If I see code like this in FP: x = 5; foo I read this as "evaluate 'foo', substituting 'x' with '5'" (accounting for shadowing, etc.). In other words, it's sugar for "let x = 5 in foo", or "(lambda x. foo) 5". In contrast, I read the same 2 lines in an imperative program as "first update the contents of memory location 'x' to contain '5', then evaluate 'foo'". This is much more complicated (i.e. has more meaning/function) than the FP version: - We're specifying an evaluation order (do this, then do that), whilst the FP version works with any evaluation order. Among other things, this makes it difficult to evaluate in parallel (imagine if '5' were 'someExpensiveCalculation' and 'foo' were 'anotherExpensiveCalculationWhichMightNotUseTheFirst'). - We need a notion of "memory cells", which don't follow the lexical/syntactic nature of scoped variables; i.e. the first line may affect references in a seemingly separate piece of code. This makes reasoning much harder (although techniques like separation logic can make many common cases easier). - The 'foo' calculation may affect the contents of 'x', so we can't trust the "equation" 'x = 5' to hold after (or even part-way-through!) the evaluation of 'foo' One nice approach is "static single assignment"; it looks imperative (e.g. "single assignment C" looks like C), but it follows the FP semantics. In other words, it's useful when you want to show that your code is "straightforward": if you write it in C, the maintainer/compiler might guess that it's straightforward (e.g. that you don't invalidate the "x = 5") but doesn't know; in single assignment C, they know because the compiler enforces it.
oconnor0 10y ago
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. 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.
- JadeNB 10y ago
  > There are also essentially no total languages today. As you obviously meant, no total general-purpose languages. I'm sure that HTML is total, for example. You also later qualified that "no total languages" meant "no widespread, simple, total languages", which I think is a very different statement!
  - oconnor0 10y ago
    Yes, there's also the subset of SQL that is total - or, at least, not-Turing-complete. Edit: As far as HTML goes, I was attempting to describe "programming languages" - or perhaps algorithmic languages - which I don't consider HTML falling under.
    - lgas 10y ago
      Is that not true of every not-total/turing-complete language?
  - gue5t 10y ago
    HTML has no reduction/evaluation rules and so it can't have a semantics in the same way as real programming languages. You could think of a "layout semantics" relating HTML and a given environment (screen size, fonts, etc.) to the resulting box model or rendered page, but that's not very interesting from the standpoint of totality: we already know that Web browsers are supposed to show something no matter how mangled their input is.
pklausler 10y ago
The second paragraph of the text refers to "the functional subset of Standard ML"; does that mean Standard ML less reassignment of references?
westoncb 10y ago
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? The paper opens with: The driving idea of functional programming is to make programming more closely related to mathematics. From a paper by John Backus: 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. Are they talking about the same thing here? Also, are there advantages to having such an algebra of programs outside of correctness verification?
- pash 10y ago
  > Are they talking about the same thing here? Yes, they're talking about roughly the same thing. The kernel of the idea is called "equational reasoning", which exploits the key mathematical characteristic of functional programs, that they are referentially transparent [0]. > Also, are there advantages to having such an algebra of programs outside of correctness verification? Proving correctness is a big one, but you can also use these techniques to derive more sophisticated algorithms from a naive (but correct) first implementation. For an example, see section 4 on the implementation of an efficient minimax algorithm in a short paper by Richard Bird [1]. (You will have to read some of the previous sections to understand the example.) If that piques your interest, Bird's introductory book on functional programming written with Philip Wadler [2] introduces the technique, which is usually called "program calculation". (Though published in 1988, their book remains a great introduction to functional programming.) If you really want to go off the deep end, Jeremy Gibbons's extensive lectures notes, published as a book chapter [3], are the best source I know. (Beware: here be category theory.) 0. https://en.m.wikipedia.org/wiki/Referential_transparency https://en.m.wikipedia.org/wiki/Referential_transparency 1. R. Bird (1988), "Algebraic identities for program calculation", http://comjnl.oxfordjournals.org/content/32/2/122.full.pdf http://comjnl.oxfordjournals.org/content/32/2/122.full.pdf [PDF] 2. R. Bird and P. Wadler (1988), Introduction to Functional Programming. It's out of print and hard copies are scarce, but a scan is available at https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Introduction%20to%20Functional%20Programming.1ed.pdf https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Intro... [PDF] 3. J. Gibbons (2002), "Calculating Functional Programs, http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-calcfp.pdf http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-ca... [PDF]
nickpsecurity 10y ago
The Charity language appears to fit into this mold: https://en.wikipedia.org/wiki/Charity_(programming_language) https://en.wikipedia.org/wiki/Charity_(programming_language) Very interesting stuff.
ht85 10y ago
fib (n+2) = fib (n+1) + fib (n+2) Something's wrong there...
- zild3d 10y ago
  Yeah that stuck out like a sore thumb to me. Maybe it was because I just finished reading the "bot crawled thousands of studies looking for simple math errors" article https://news.ycombinator.com/item?id=12643978 https://news.ycombinator.com/item?id=12643978
thecity2 10y ago
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 http://docs.idris-lang.org/en/latest/tutorial/theorems.html#...
murbard2 10y ago
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 https://hackernoon.com/smart-contracts-turing-completeness-r...
- pron 10y ago
  Even if you restrict yourself to the weakest programming model possible -- finite state machines -- proving program correctness is still infeasible in general (PSPACE-complete for very simple FSM languages; EXPTIME or even 2-EXP for richer FSM languages, I think). It is a mistake to ignore all the results about FSM verification. In your post, you write: > However, almost all correct programs of interest are going to be essentially provably correct. Moreover, the proof of their correctness will be relatively straightforward. This has been shown to be false in practice. The difficulty of proving real-world program correctness shows that real-world cases can get arbitrarily close to the worst-case predicted by the theory. Proving small programs like seL4 took required experts, and even then demanded an extreme simplification of all involved algorithms so that proof would be feasible. Even then, the cost was far beyond what any "ordinary" software could afford, and even after a great streamlining of the process and the use of "easily verifiable" languages, it is expected to be suitable only for resource-rich high-assurance software. Note that I'm not saying that formal methods are useless. I regularly use formal methods myself. But making them affordable is an art. I've written at length about the relevant theory here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
  - murbard2 10y ago
    Thanks, those are good comments and I largely agree. I'll reply on a couple points though: 1) Yes, even in weak models, proving correctness is still intractable in general. However, this does not mean that a general algorithm has to be slow when run on typical instances. Typical instances are designed with a proof of correctness in mind, which is a strong indication that such a proof should be accessible. Unless you're generating programs randomy, programming generally entails carrying at least an informal proof of correctness in mind. 2) As you point out it is currently very hard and tedious to formalize those proofs. However, I believe this isn't a fundamental barrier. We need better tooling, more clever proof-finding algorithm to bridge the gaps, clearer interfaces. Importantly, it is not a computational barrier. There is nothing about the formal verification of typical software that intrinsically requires expensive computations. Compare it to image recognition. It used to be very hard to do in software and it didn't work well. But when it finally started working, it didn't turn out to be particularly computer intensive. I think the same is true in formal verification. We don't know how to do it very well, but we're not up against theorems in complexity theory, we just lack the know-how.

207 points by adgasf 10y ago

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.

dj-wonk 10y ago
You might also want to check out "Functional Programming, Totally" by Keanu Reeves.

DenisM 10y ago

[...] We consider a simple discipline of total functional programming designed to exclude the possibility of non-termination. [...] 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". 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. It's a fascinating subject because sub-turing language programs are a lot easier to analyze.

lomnakkus 10y ago
> That is "useful despite being sub-turing". This has been called being "Pacman Complete" by Edwin Brady. I very nice catchy term, IMO.
- skybrian 10y ago
  I like that. A search doesn't find anything relevant, though. Got a reference?
  - 14113 10y ago
    Edwin didn't coin it - but he did popularise it: https://twitter.com/edwinbrady/status/384671269490540544 https://twitter.com/edwinbrady/status/384671269490540544
    - lomnakkus 10y ago
      Ah, nice reference. The first time I heard it used was in one of his talks.
barrkel 10y ago
A compiler is, at a high level, just a function. And most architectural breakdowns of compilers turn them into sequences of functions, like: link(codegen(analyze(typecheck(parse(lex(source)))))) And compilers are one of the easiest kinds of programs to write naturally in a functional language.

swordbeta 10y ago

Any mirror? "You have exceeded your daily download allowance"

bazzargh 10y ago
The original journal the paper was published in has it: http://www.jucs.org/jucs_10_7/total_functional_programming http://www.jucs.org/jucs_10_7/total_functional_programming
- agumonkey 10y ago
  Lots of cool issues http://www.jucs.org/jucs_2 http://www.jucs.org/jucs_2
sndean 10y ago
http://sblp2004.ic.uff.br/papers/turner.pdf http://sblp2004.ic.uff.br/papers/turner.pdf or http://www.mpi-sws.org/~skilpat/plerg/papers/turner-total-fp-2up.pdf http://www.mpi-sws.org/~skilpat/plerg/papers/turner-total-fp...

vog 10y ago

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/ https://existentialtype.wordpress.com/2014/03/20/old-neglect... 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/ http://pixelscommander.com/en/javascript/nasa-coding-standar... (Related HN discussion: https://news.ycombinator.com/item?id=8856226 https://news.ycombinator.com/item?id=8856226)

wyager 10y ago
The approach given in the paper explicitly allows for Turing completeness through the use of data/codata types. Instead of proving termination over codata you prove that a function "does something useful" every iteration.
- willtim 10y ago
  You would of course need to factor out the outer-loop to do this. But it seems even this is not necessary. This paper discusses using total languages to build generally recursive (Turing complete) computations as an effect monad: https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree....
  - wyager 10y ago
    > You would of course need to factor out the outer-loop to do this What are you referring to? Data/codata checking works with local type inference.
    - mkehrt 10y ago
      Essentially, to get a nonterminating, program, your top level function needs to take a piece of codata to corecurse over to run indefinitely. Since you can't actually write a program that takes no arguments that produces an infinite piece of data, all programs must terminate.

wyager 10y ago

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.

icen 10y ago
Brief nitpick: Idris and Agda both have codata constructions, and in Idris (at least, I'm not familiar with Agda) it is supported by the totality checker.
ktRolster 10y ago
The main difficulty is that, very often, I do want my programs to loop forever/indefinitely. (Or at least until someone shuts them down).
- wyager 10y ago
  Right! That's the point of codata. If you want your program to run forever, you could express e.g. I/O events as an infinite (codata) stream. Then, instead of trying to prove that your program terminates (which it might not), it proves that your program "does something useful" every time it gets an IO event, for a particular practical definition of "doing something useful".
- SomeStupidPoint 10y ago
  Would it significantly harm your experience if all your programs turned off after 1000 years of execution without input? If not, your program could be "total" in most of the useful senses, and subparts could have tighter bounds, without any harm.

snake117 10y ago

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. For example, something as simple as assigning a variable has so much more meaning and functionality than I am used to, thanks to pattern matching. I look forward to diving deeper into functional programming. Thanks for posting.

sotojuan 10y ago
There's a lot to explore! Elixir is my favorite "new" language, and its style of functional programming is accessible and practical yet still very didactic. That said, there's always more mind bending things out there once you've digester Elixir. I'm experiencing a similar thing with Haskell at the moment.
chriswarbo 10y ago
> For example, something as simple as assigning a variable has so much more meaning and functionality than I am used to, thanks to pattern matching. Once I grokked FP, I started thinking about this the other way around. If I see code like this in FP: x = 5; foo I read this as "evaluate 'foo', substituting 'x' with '5'" (accounting for shadowing, etc.). In other words, it's sugar for "let x = 5 in foo", or "(lambda x. foo) 5". In contrast, I read the same 2 lines in an imperative program as "first update the contents of memory location 'x' to contain '5', then evaluate 'foo'". This is much more complicated (i.e. has more meaning/function) than the FP version: - We're specifying an evaluation order (do this, then do that), whilst the FP version works with any evaluation order. Among other things, this makes it difficult to evaluate in parallel (imagine if '5' were 'someExpensiveCalculation' and 'foo' were 'anotherExpensiveCalculationWhichMightNotUseTheFirst'). - We need a notion of "memory cells", which don't follow the lexical/syntactic nature of scoped variables; i.e. the first line may affect references in a seemingly separate piece of code. This makes reasoning much harder (although techniques like separation logic can make many common cases easier). - The 'foo' calculation may affect the contents of 'x', so we can't trust the "equation" 'x = 5' to hold after (or even part-way-through!) the evaluation of 'foo' One nice approach is "static single assignment"; it looks imperative (e.g. "single assignment C" looks like C), but it follows the FP semantics. In other words, it's useful when you want to show that your code is "straightforward": if you write it in C, the maintainer/compiler might guess that it's straightforward (e.g. that you don't invalidate the "x = 5") but doesn't know; in single assignment C, they know because the compiler enforces it.

oconnor0 10y ago

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. 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.

JadeNB 10y ago
> There are also essentially no total languages today. As you obviously meant, no total general-purpose languages. I'm sure that HTML is total, for example. You also later qualified that "no total languages" meant "no widespread, simple, total languages", which I think is a very different statement!
- oconnor0 10y ago
  Yes, there's also the subset of SQL that is total - or, at least, not-Turing-complete. Edit: As far as HTML goes, I was attempting to describe "programming languages" - or perhaps algorithmic languages - which I don't consider HTML falling under.
  - lgas 10y ago
    Is that not true of every not-total/turing-complete language?
- gue5t 10y ago
  HTML has no reduction/evaluation rules and so it can't have a semantics in the same way as real programming languages. You could think of a "layout semantics" relating HTML and a given environment (screen size, fonts, etc.) to the resulting box model or rendered page, but that's not very interesting from the standpoint of totality: we already know that Web browsers are supposed to show something no matter how mangled their input is.

pklausler 10y ago

The second paragraph of the text refers to "the functional subset of Standard ML"; does that mean Standard ML less reassignment of references?

westoncb 10y ago

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? The paper opens with: The driving idea of functional programming is to make programming more closely related to mathematics. From a paper by John Backus: 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. Are they talking about the same thing here? Also, are there advantages to having such an algebra of programs outside of correctness verification?

pash 10y ago
> Are they talking about the same thing here? Yes, they're talking about roughly the same thing. The kernel of the idea is called "equational reasoning", which exploits the key mathematical characteristic of functional programs, that they are referentially transparent [0]. > Also, are there advantages to having such an algebra of programs outside of correctness verification? Proving correctness is a big one, but you can also use these techniques to derive more sophisticated algorithms from a naive (but correct) first implementation. For an example, see section 4 on the implementation of an efficient minimax algorithm in a short paper by Richard Bird [1]. (You will have to read some of the previous sections to understand the example.) If that piques your interest, Bird's introductory book on functional programming written with Philip Wadler [2] introduces the technique, which is usually called "program calculation". (Though published in 1988, their book remains a great introduction to functional programming.) If you really want to go off the deep end, Jeremy Gibbons's extensive lectures notes, published as a book chapter [3], are the best source I know. (Beware: here be category theory.) 0. https://en.m.wikipedia.org/wiki/Referential_transparency https://en.m.wikipedia.org/wiki/Referential_transparency 1. R. Bird (1988), "Algebraic identities for program calculation", http://comjnl.oxfordjournals.org/content/32/2/122.full.pdf http://comjnl.oxfordjournals.org/content/32/2/122.full.pdf [PDF] 2. R. Bird and P. Wadler (1988), Introduction to Functional Programming. It's out of print and hard copies are scarce, but a scan is available at https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Introduction%20to%20Functional%20Programming.1ed.pdf https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Intro... [PDF] 3. J. Gibbons (2002), "Calculating Functional Programs, http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-calcfp.pdf http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-ca... [PDF]

nickpsecurity 10y ago

The Charity language appears to fit into this mold: https://en.wikipedia.org/wiki/Charity_(programming_language) https://en.wikipedia.org/wiki/Charity_(programming_language) Very interesting stuff.

ht85 10y ago

fib (n+2) = fib (n+1) + fib (n+2) Something's wrong there...

zild3d 10y ago
Yeah that stuck out like a sore thumb to me. Maybe it was because I just finished reading the "bot crawled thousands of studies looking for simple math errors" article https://news.ycombinator.com/item?id=12643978 https://news.ycombinator.com/item?id=12643978

thecity2 10y ago

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 http://docs.idris-lang.org/en/latest/tutorial/theorems.html#...

murbard2 10y ago

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 https://hackernoon.com/smart-contracts-turing-completeness-r...

pron 10y ago
Even if you restrict yourself to the weakest programming model possible -- finite state machines -- proving program correctness is still infeasible in general (PSPACE-complete for very simple FSM languages; EXPTIME or even 2-EXP for richer FSM languages, I think). It is a mistake to ignore all the results about FSM verification. In your post, you write: > However, almost all correct programs of interest are going to be essentially provably correct. Moreover, the proof of their correctness will be relatively straightforward. This has been shown to be false in practice. The difficulty of proving real-world program correctness shows that real-world cases can get arbitrarily close to the worst-case predicted by the theory. Proving small programs like seL4 took required experts, and even then demanded an extreme simplification of all involved algorithms so that proof would be feasible. Even then, the cost was far beyond what any "ordinary" software could afford, and even after a great streamlining of the process and the use of "easily verifiable" languages, it is expected to be suitable only for resource-rich high-assurance software. Note that I'm not saying that formal methods are useless. I regularly use formal methods myself. But making them affordable is an art. I've written at length about the relevant theory here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
- murbard2 10y ago
  Thanks, those are good comments and I largely agree. I'll reply on a couple points though: 1) Yes, even in weak models, proving correctness is still intractable in general. However, this does not mean that a general algorithm has to be slow when run on typical instances. Typical instances are designed with a proof of correctness in mind, which is a strong indication that such a proof should be accessible. Unless you're generating programs randomy, programming generally entails carrying at least an informal proof of correctness in mind. 2) As you point out it is currently very hard and tedious to formalize those proofs. However, I believe this isn't a fundamental barrier. We need better tooling, more clever proof-finding algorithm to bridge the gaps, clearer interfaces. Importantly, it is not a computational barrier. There is nothing about the formal verification of typical software that intrinsically requires expensive computations. Compare it to image recognition. It used to be very hard to do in software and it didn't work well. But when it finally started working, it didn't turn out to be particularly computer intensive. I think the same is true in formal verification. We don't know how to do it very well, but we're not up against theorems in complexity theory, we just lack the know-how.