Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Functional Programming

Structure and Interpretation of Computer Programs

• rating: TODO

There's a section on amb and parsing vs generation (section 4.3). Many, many other things.

Purely Functional Data Structures

• rating: TODO

.

ACM Symposium on LISP and Functional Programming, 1984

• rating: 1

Some decent papers in these conference proceedings.

A tutorial on the universality and expressiveness of fold

• rating: 3

Hutton talks about the universal property of fold, showing that it can be used in proofs to avoid the need for inductive proofs. If I was feeling bold, I might go one further and say: the universal property of fold is induction!

Total Functional Programming

• rating: 2

It's a very interesting paper and you should read it. I should maybe write a more cogent summary of it here at some point. I would take some issue with the conclusion about a "dichotomy of language design" near the very end of the paper. Due to the Halting problem, there are indeed programs that are in R (they always halt) but we cannot prove they are in R; but I don't see this affecting a "dichotomy in language design" very materially, for several reasons:

• a program that is guaranteed to terminate might still take an obscenely long time to terminate
• very few problems of practical interest require algorithms in "large" complexity classes like TOWER; yet even these are guaranteed to terminate
• systems with the full power of Turing machines are (ironically) the easiest systems to define; everything "safer" requires more effort
• you do need the full power of a Turing machine to implement a TM interpreter, but TMs are not the only "universal" computational class; there are "universal" CFLs and "universal" System F intepreters too
• there are algorithms that are useful enough that we use them even absent of a proof that they are terminating: for example, higher-order unification.

Turner, Bird, Eratosthenes: An Eternal Burning Thread

• rating: 1

Often it's straightforward but sometimes it's tricky to prove that recursive functions terminate or that corecursive functions are productive. I agree.

Fast and Loose Reasoning is Morally Correct

• rating: 1

Wow. Well, I think it's good to understand that "Fast and Loose" has a specific meaning here (it means, to treat functions as terminating (or total) even if you don't know for sure that they are), as does "morally" (it is meant in the sense of "virtually" or "essentially"), because otherwise you might find some strange senses in that title.

The idea has some merit. I don't know how well the relation they define between a partial language and a total language, justifies the idea. Clearly, the fact that they can even try to show that some results are preserved, gives it some weight.

let (rec) insertion without effects, lights or magic

• rating: TODO

I did actually read this once but I would need to re-read it. I rather got the impression the first time that it was rather specialized to a rather specific metalanguage approach. I wonder how much general wisdom could be extracted from it.

Functors, Applicatives, And Monads In Pictures - adit.io

• rating: 3

.

functional programming - What is the origin and meaning of the phrase "Lambda the ultimate?" - Software Engineering Stack Exchange

• rating: 1

.

compiler construction - Converting a function to use tail recursion -- a formal study - Stack Overflow

• rating: 1

.

Do Applicative Functors Generalize the S & K Combinators? - Brandon.Si(mmons)

• rating: 1

.

Railway Oriented Programming | F# for fun and profit

• rating: 2

.

interpreters - How to implement scheme\'s letrec in a lazy dialect? - Computer Science Stack Exchange

• rating: 1

The question has not been answered on the site.

Recitation 21: Let Expressions & The Environment Model

• rating: 1

.

PseudoPower/AFSM: Arrowized functional state machines

• rating: 3

.