Total Functional Programming (2004) [pdf]

&gt; to make programming more closely related to mathematics<p>Why is this taken as a given to be a good thing? Our hardware has state. Any IO is a side effect, so what&#x27;s the non trivial use case for &quot;pure functions&quot; all the way down?<p>I think FP paradigms can be useful in specific problem domains, I&#x27;m skeptical of the general utility (vs resource spend) of strong FP languages.

I like how Lean4 handles totality. You can tell the compiler to trust you. Or you can provide a proof. The latter is more useful while the former is sometimes pragmatic.

I appreciate this article. It&#x27;s clear, easy to understand, and uses theory to propose practical improvements to FP.<p>Some minor nitpicks:<p>&gt; In total functional programming ⊥ does not exist.<p>That doesn&#x27;t seem right. In total FP, we can still define a ⊥ type that has no values. I think the problem here is that the author uses ⊥ to indicate both a type and a value of that type (e.g. f ⊥ = ⊥), which is confusing.<p>&gt; 0 &#x2F; 0 = 0<p>Surely it would be better to use a Maybe type for this instead?<p><pre><code> 0 &#x2F; 1 = Just 0 0 &#x2F; 0 = Nothing </code></pre> The same approach also addresses the difficulty of hd:<p><pre><code> hd :: List a -&gt; Maybe a hd (Cons a x) = Just a hd Nil = Nothing </code></pre> F# has this function, and calls it &quot;tryHead&quot;, rather than just &quot;head&quot;.

A few comments have cheerfully reproduced the stock objection that a program with no side effects does nothing and is thus useless. By extension functional programming is useless and it&#x27;s all pointless.<p>I&#x27;d like to counter that a function from vector of bytes to vector of bytes can be pure, terminating, implement some algorithm of great commercial interest and map exactly onto a program that reads said vector of bytes from stdin and sends them to stdout.<p>If you&#x27;re really generous, it can write two vectors of bytes, and tie the other one to stderr.<p>That covers such useless academic things as <i>your compiler</i>.

Did anyone notice the fib function on the first page? It doesn&#x27;t terminate:<p>fib :: Nat-&gt;Nat<p>fib 0 = 0<p>fib 1 = 1<p>fib (n+2) = fib (n+1) + fib (n+2)<p>The last line should be fib (n+2) = fib (n+1) + fib (n). The published version seems to have the same problem: <a href="https:&#x2F;&#x2F;pdfs.semanticscholar.org&#x2F;82b4&#x2F;ea72b89270c528006dd2532aef43eec463c3.pdf" rel="nofollow">https:&#x2F;&#x2F;pdfs.semanticscholar.org&#x2F;82b4&#x2F;ea72b89270c528006dd253...</a>

20 year old paper. People interested in total functions should probably have a good look at Idris.

In page 2, there is the theorem: Theorem ∀n in Nat.f n (fib p) (fib (p+1)) = fib (p+n), I think it should be for all p in Nat (fib p) + (fib (p+1)) = fib(p+2), otherwise there is something mysterious here.

See also discussion (2007) at <a href="http:&#x2F;&#x2F;lambda-the-ultimate.org&#x2F;node&#x2F;2003" rel="nofollow">http:&#x2F;&#x2F;lambda-the-ultimate.org&#x2F;node&#x2F;2003</a><p>(which mentions <a href="http:&#x2F;&#x2F;pll.cpsc.ucalgary.ca&#x2F;charity1&#x2F;www&#x2F;home.html" rel="nofollow">http:&#x2F;&#x2F;pll.cpsc.ucalgary.ca&#x2F;charity1&#x2F;www&#x2F;home.html</a> )

Isn&#x27;t this handled by &#x27;purity&#x27; of functions?<p>It seems like the big idea here is that Int-&gt;Int always, no errors, faults, &#x27;impact by extra data&#x27;.<p>Isn&#x27;t that all also solved by pure functions? And is incorporated into functional languages at this point?