By hallucinate you mean, not knowing what/where you are or doing, in that particular moment? Then yes, one can use that word. The simplest analogy of here-now is when you are watching an exceptional movie (as per your taste) and you get lost in those moments of watching. The same phenomenon is apparent in observing other forms of arts (songs, paintings etc).
So, are such states hallucination? Every person (human being) knows for sure that they are real.
Do humans "hallucinate" what is in front of them? It's fairly well understood that our visual cortex is the product of evolution. So we will see things as they are meant to be seen, by our visual cortex. This is completely different from what is really there.
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.
> The only Thunderbolt port on my 2011 iMac is occupied.
An unfortunate design flaw specifically on LaCie's part. As with FireWire before it, and SCSI before that, Thunderbolt is a daisy-chain interface. Single-port devices in such ecosystems are best considered defective.
This looks awesome! I will be interested to see how well you can make the features fit together. I have been really interested in languages that give you tools for reasoning at multiple levels of abstraction.
Have you tried seeing how a full dependent type system could be used in your design?
I plan to sneak in something similar with a capable type system and contracts for stuff that you can't express in the types. That way you could "one day" use a solver like Z3 and start proving or disproving some of the tractable contracts, without having to even change the programs. A bit like LiquidHaskell.
Not exactly dependent types, but practical, I think.