Rate a Functional Programming paper, put commentary on one other.
Chris Pressey
1 year, 7 days ago
| 28 | 28 | |
| 29 | 29 | Total Functional Programming (online @ [www.jucs.org](https://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf)) |
| 30 | 30 | |
| 31 | [Turner, Bird, Eratosthenes: An Eternal Burning Thread](https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/erato.pdf) | |
| 31 | Turner, Bird, Eratosthenes: An Eternal Burning Thread (online @ [www.cs.ox.ac.uk](https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/erato.pdf)) | |
| 32 | 32 | |
| 33 | 33 | ### Books |
| 34 | 34 |
| 27 | 27 | |
| 28 | 28 | * authors: Jeremy Gibbons |
| 29 | 29 | * date: 2021 |
| 30 | * url: https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/erato.pdf | |
| 30 | * online @ [www.cs.ox.ac.uk](https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/erato.pdf) | |
| 31 | 31 | |
| 32 | , | |
| 33 | ||
| 32 | . |
| 37 | 37 | |
| 38 | 38 | * rating: 2 |
| 39 | 39 | |
| 40 | . | |
| 40 | It's a very interesting paper and you should read it. I should maybe | |
| 41 | write a more cogent summary of it here at some point. I would take | |
| 42 | some issue with the conclusion about a "dichotomy of language design" | |
| 43 | near the very end of the paper. Due to the Halting problem, there are | |
| 44 | indeed programs that are in R (they always halt) but we cannot | |
| 45 | prove they are in R; but I don't see this affecting a "dichotomy in | |
| 46 | language design" very materially, for several reasons: | |
| 47 | ||
| 48 | * a program that is guaranteed to terminate might still take an | |
| 49 | obscenely long time to terminate | |
| 50 | * very few problems of practical interest require algorithms | |
| 51 | in "large" complexity classes like TOWER; yet even these are | |
| 52 | guaranteed to terminate | |
| 53 | * systems with the full power of Turing machines are (ironically) the | |
| 54 | _easiest_ systems to define; everything "safer" requires more effort | |
| 55 | * you do need the full power of a Turing machine to implement a TM | |
| 56 | interpreter, but TMs are not the only "universal" computational class; | |
| 57 | there are "universal" CFLs and "universal" System F intepreters too | |
| 58 | * there are algorithms that are useful enough that we | |
| 59 | use them even absent of a proof that they are terminating: | |
| 60 | for example, higher-order unification. | |
| 41 | 61 | |
| 42 | 62 | ### Turner, Bird, Eratosthenes: An Eternal Burning Thread |
| 43 | 63 | |
| 44 | * rating: TODO | |
| 64 | * rating: 1 | |
| 45 | 65 | |
| 46 | . | |
| 66 | *Often* it's straightforward but *sometimes* it's tricky | |
| 67 | to prove that recursive functions terminate or | |
| 68 | that corecursive functions are productive. I agree. | |
| 47 | 69 | |
| 48 | 70 | ### Functors, Applicatives, And Monads In Pictures - adit.io |
| 49 | 71 |
| 15 | 15 | Of these, [**102** have the highest rating](by-rating/Top-rated.md), |
| 16 | 16 | [**27** are considered classics](by-rating/Classic.md), |
| 17 | 17 | [**47** are considered very interesting](by-rating/Very%20Interesting.md), |
| 18 | while [**77** are yet to be rated](by-rating/Unrated.md). | |
| 18 | while [**76** are yet to be rated](by-rating/Unrated.md). | |
| 19 | 19 | |
| 20 | 20 | <!-- /TOTALS --> |
| 21 | 21 |
| 128 | 128 | * [Introduction to the Calculus of Inductive Constructions](https://inria.hal.science/hal-01094195/document) |
| 129 | 129 | * [The Calculus of Inductive Constructions](https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf) |
| 130 | 130 | |
| 131 | ### Functional Programming | |
| 132 | ||
| 133 | * [Turner, Bird, Eratosthenes: An Eternal Burning Thread](https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/erato.pdf) | |
| 134 | ||
| 135 | 131 | ### Incompleteness |
| 136 | 132 | |
| 137 | 133 | * A Simple Character String Proof of the \"True but Unprovable\" Version of Goedel\'s First Incompleteness Theorem ([arxiv.org](https://arxiv.org/abs/1402.7253)) |