This. Thank you. I'm being rate limited, so this is the only post I'll be making on this thread. My question was genuine. I want to learn both the positives and the pitfalls of dependent types. I mimicked the book's description because it amused me from a linguistic perspective. Looking back, I probably should have phrased it differently.
Note that many of those problems are being actively worked on in research, and progress is being made, albeit slowly. That said, we can still get some of the benefits of dependent types, even without all the problems being solved right now! Just gotta be aware that it's not all roses yet.
Here is a quick guide to avoiding them: "Unless you are using Haskell at a very high level of abstraction, Coq, Agda, Pie or Idris: congratulations you have avoided them."
It's not really clear why you'd want a book about the downsides of a quite recent development in practically usable programming models. Is it just because you are a hater?
My guess is because OP has been burned by the "LEARN THIS NEW THING, IT'S REALLY COOL AND POWERFUL AND ALL OF THE COOL KIDS ARE DOING IT (and oh by the way many of the simple things you do all the time are incredibly inconvenient...)" narrative one too many times.
Adopting something purely on it's merits is a bad idea, but nobody ever writes the book about a language/paradigm's downsides. I'm pretty sure that was the joke, but I might be off.
nobody ever writes the book about a language/paradigm's downsides
Indeed. One can argue that books like "optimizing X" or "secure X" are about ways to easily write slow or insecure code in X, but this is somewhat narrow. Is there never enough demand for a broader book on downsides of X?
> I wrote a whole chapter about the downsides of X
I lol'ed 6-8 times... Still, I have to say that I'm loving my distros lately; distro maintainers, you rule!
Some typos in the article:
eents/events
client an/client can
because it the/because it solved? the
tires/tries
ore dump/core dump
trwe/tree
piel/pixel
resulution/resolution
ertain/certain
N ot/Not
screens een have/screens have
How's it "not knowing the difference" to explain that the usage of the terms client and server switched over time, in the sense of which is local and which is remote?
An xterm client running on a VAX mainframe connects to an X11 server running on a Sun workstation: the X11 client is remote, the X11 server is local.
A web browser client running on a phone connects to a web server running in the cloud: the web client is local, the web server is remote.
There are tons, but we really need to ask if any of this is a fair topic for Dependent Typing, which has only emerged from pi-calculus musings on paper to compilers that can do more than prove simple structural recursion.
It's like seeing a photo of a baby and asking why there isn't a service to provide police records for babies, because you "just want to be careful, you know?"
It's not even really possible to "adopt" dependent typing today. It's only emerged from the realm of academic curiosity and only two implementations exist that are anywhere near "practical" in the context you're describing.
Both of those implementations are very honest about their shortcomings, and nearly every talk and blogpost for them mentions you can't yet use this in many industrial contexts.
It's very difficult to see this as anything but the usual distate for PL theory that constantly swirls around this community. If the author didn't intend to associate a post with that, then they've done it by accident.