28 ms·

> An introduction to dependent types, demonstrating the most beautiful aspects, one step at a time. Is there a companion book detailing the ugly downsides of d

> An introduction to dependent types, demonstrating the most beautiful aspects, one step at a time. Is there a companion book detailing the ugly downsides of dependent types and how to avoid them, one step at a time?

z5h 8y ago
Can you elaborate? Do you have war stories?
KirinDave 8y ago
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?
- bbeonx 8y ago
  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.
  - jackfraser 8y ago
    Unless said language is PHP, in which case there's no end of diatribes about it
  - owl57 8y ago
    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?
    - DonHopkins 8y ago
      Bertrand Meyer's book on Eiffel was all about the downsides of C++. And then there's the Unix-Hater's Handbook... https://en.wikipedia.org/wiki/The_Unix-Haters_Handbook https://en.wikipedia.org/wiki/The_Unix-Haters_Handbook I wrote a whole chapter about the downsides of X -- do you think there's a need for a broader book? ;) https://medium.com/@donhopkins/the-x-windows-disaster-128d398ebd47 https://medium.com/@donhopkins/the-x-windows-disaster-128d39...
      - mcguire 8y ago
        The one where you demonstrated that you don't know the difference between a client and a server? :-)
        DonHopkins 8y ago
        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. Right?
        AzzieElbab 8y ago
        Loled. I used to do phone support for x11 servers for pcs. This terminology confused people to no end
        mcguire 8y ago
        Exactly! I, too, used to live in an office next to a machine room full of "web clients"! :-D (Actually, I'm one of those deluded fools who claim a "server" provides a "service" to one or more "clients", who make "requests". Yeah, I know, but I figure somebody has to keep the joke funny.)
        8y ago
  - avip 8y ago
    Here's one for JS http://johnkpaul.github.io/presentations/empirejs/javascript-bad-parts http://johnkpaul.github.io/presentations/empirejs/javascript...
  - KirinDave 8y ago
    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.
    - ernst_klim 8y ago
      >only two implementations exist that are anywhere near "practical" Out of curiosity, why F* or Idris are not practical?
      - KirinDave 8y ago
        F* and Idris are precisely the ones I had in mind, although I guess you could make an argument for Agda. What did you think I was imagining? I can only name 5 DT languages off the top of my head.
        ernst_klim 8y ago
        So, why are they not practical in your opinion?
zem 8y ago
I feel like people are misreading this comment, which is asking how to avoid the pitfalls of dependent types, not how to avoid dependent types.
- lylecubed 8y ago
  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.
danidiaz 8y ago
> the ugly downsides of dependent types and how to avoid them There's this Reddit answer from two years ago, and the subsequent comments https://www.reddit.com/r/haskell/comments/3zc81v/tradeoffs_of_dependent_types_xpost_from_ridris/cyl0bm1 https://www.reddit.com/r/haskell/comments/3zc81v/tradeoffs_o...
- lylecubed 8y ago
  This is exactly what I'm looking for. Thanks!
  - bjz_ 8y ago
    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.

z5h 8y ago

Can you elaborate? Do you have war stories?

KirinDave 8y ago

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?

bbeonx 8y ago
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.
- jackfraser 8y ago
  Unless said language is PHP, in which case there's no end of diatribes about it
- owl57 8y ago
  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?
  - DonHopkins 8y ago
    Bertrand Meyer's book on Eiffel was all about the downsides of C++. And then there's the Unix-Hater's Handbook... https://en.wikipedia.org/wiki/The_Unix-Haters_Handbook https://en.wikipedia.org/wiki/The_Unix-Haters_Handbook I wrote a whole chapter about the downsides of X -- do you think there's a need for a broader book? ;) https://medium.com/@donhopkins/the-x-windows-disaster-128d398ebd47 https://medium.com/@donhopkins/the-x-windows-disaster-128d39...
    - mcguire 8y ago
      The one where you demonstrated that you don't know the difference between a client and a server? :-)
      - DonHopkins 8y ago
        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. Right?
        AzzieElbab 8y ago
        Loled. I used to do phone support for x11 servers for pcs. This terminology confused people to no end
        mcguire 8y ago
        Exactly! I, too, used to live in an office next to a machine room full of "web clients"! :-D (Actually, I'm one of those deluded fools who claim a "server" provides a "service" to one or more "clients", who make "requests". Yeah, I know, but I figure somebody has to keep the joke funny.)
        8y ago
- avip 8y ago
  Here's one for JS http://johnkpaul.github.io/presentations/empirejs/javascript-bad-parts http://johnkpaul.github.io/presentations/empirejs/javascript...
- KirinDave 8y ago
  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.
  - ernst_klim 8y ago
    >only two implementations exist that are anywhere near "practical" Out of curiosity, why F* or Idris are not practical?
    - KirinDave 8y ago
      F* and Idris are precisely the ones I had in mind, although I guess you could make an argument for Agda. What did you think I was imagining? I can only name 5 DT languages off the top of my head.
      - ernst_klim 8y ago
        So, why are they not practical in your opinion?

zem 8y ago

I feel like people are misreading this comment, which is asking how to avoid the pitfalls of dependent types, not how to avoid dependent types.

lylecubed 8y ago
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.

danidiaz 8y ago

> the ugly downsides of dependent types and how to avoid them There's this Reddit answer from two years ago, and the subsequent comments https://www.reddit.com/r/haskell/comments/3zc81v/tradeoffs_of_dependent_types_xpost_from_ridris/cyl0bm1 https://www.reddit.com/r/haskell/comments/3zc81v/tradeoffs_o...

lylecubed 8y ago
This is exactly what I'm looking for. Thanks!
- bjz_ 8y ago
  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.