[ek]

Great list!

A lot of the stuff there is to know about functional programming is still only contained in academic papers, and indeed many of these listed books are texts in programming languages that cite a great deal of the important literature. There is much about programming languages and functional programming that one might read interspersed with these books. Other than following references in the backs of many of these books, the Haskell wiki is a good place for starting to dig into literature on functional programming, as many articles link to important and interesting papers.

On that note it's a bit strange not to see a few books on semantics, such as Transitions and Trees or Semantics Engineering with PLT Redex, listed among books like TAPL and Barendregt's Lambda Calculus. Especially now that DSL design is something many programmers are dabbling in, it makes sense to gain some background on operational semantics. I'd recommend either of these books to anyone working on DSLs, especially in a functional language.

Finally, it might be worth adding Homotopy Type Theory to your list, especially since the list already contains several good books about Coq as well as works about type theory and type systems.

[platz]

I'll second Haskell wiki. It has some of the most detailed explanations of functional concepts I've come across.

http://www.haskell.org/haskellwiki/Fold

http://www.haskell.org/haskellwiki/Monad

http://www.haskell.org/haskellwiki/All_About_Monads

http://www.haskell.org/haskellwiki/Learn_Haskell_in_10_minut...

http://www.haskell.org/haskellwiki/Typeclassopedia

Also check out http://adit.io/ for some great tutorials with pictures

[codygman]

The functors, applicatives, and monads in pictures tutorial[1] just made so many things click for me. Those are all very very good resources indeed!

1. http://adit.io/posts/2013-04-17-functors,_applicatives,_and_...

[mej10]

Why Homotopy Type Theory? It is cutting edge research and it doesn't seem clear to me that it is going to have an impact on functional programming (of the non-mathematical research type) any time soon. Am I mistaken?

[tel]

It seems to have quickly "infected" literature on dependent types at large---not to the point of having replaced the normal terminology, but instead as forming a sort of common framework for examining those fields.

Which is definitely a point on the side of "has no impact".

But on the other hand, I think studying dependent types is a fantastic way to get some perspective as an intermediate to advanced Haskell or OCaml programmer. Software Foundations and Certified Programming with Dependent Types are both great books to read.

HoTT won't be on that list for some time if ever, but once you've got a good mental model for dependent types it's illuminating to see them worked out "from scratch" as HoTT does.

So, the best I can say is that it can be influential in the way that you view types if you're someone who frequently programs and thinks in a nicely typed language like Haskell/OCaml and maybe Scala.

[ek]

The book on Homotopy Type Theory is quite readable even though the developments are quite new. The purpose of the book is to get the material into the hands of as many as it may be useful to as soon as possible.

I would argue that the book is at least as useful as Categories for the Working Mathematician or Barendregt's Lambda Calculus are likely to be for your typical software engineer interested in functional programming. To be clear, someone interested only in learning how to program in functional languages is probably not going to get very much from either of those books, which are respectively an extremely technical mathematical text on topics in category theory, and a heavily logic-oriented, mathematical presentation of the lambda calculus and derivatives thereof. Not much of the material in either book would be directly applicable to the practice of software engineering using functional languages, but someone with a deeper interest would find them useful and interesting, and I think the same holds for the HoTT book. At the very least, as the other commenter alluded to, a novice reader would probably be able to glean a nice understanding of Martin-Löf dependent type theory from the first chapter.

[alexott]

thanks - I'm usually updating this list every 2-3 months, when I have long weekend or something like...