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