1. 10

  2. 8

    It is too bad that this chose to take the tone that it did. It doesn’t really benefit or convince anyone.

    1. 5

      Could you identify, specifically, how you think the information in the article could have been conveyed more effectively?

      As is, your comment just says that you didn’t like the tone and asserts that others won’t either, but doesn’t have any information about why you think these things, and doesn’t address any of the content of the article, either.

      Personally, I didn’t have a problem with the article, so I’d be interested to hear why you thought the tone made the article unconvincing, or what you thought of the article’s content.

      1. 9

        Sure, on Twitter, the author says (https://twitter.com/theerasmas/status/464539660791058432):

        @infosaurus I don't expect a fake whitepaper to convince people of anything!
        I want people to be excited about types. :)

        Going to the start of the article itself:

        Recent research-based advances in computering have shown that people want
        more TDD and expend most of their time coming up with components of code
        called “units” so that they can test them for quality assurance.
        But guess what?
        They’re doing it. Wrong.
        A crack team of compiler inventors has been in stealth mode for literally
        months preparing a new way to TDD without having to make up units all the time.
        The Idris compiler (industry buzzword for a linting tool) is so advanced you can:

        I have a hard time seeing how this isn’t at least somewhat snarky and it certainly reinforces the “fake whitepaper” feel.

        If the audience is meant to be people who are doing TDD in other languages, it probably would pay to take them seriously rather than appear to be laughing at them. (“Computering”, “most of their time” “They’re doing it. Wrong.”, “make up units all the time”.)

        Idris is a language, it isn’t an “industry buzzword for a linting tool”, and the analogy to a linting tool simply doesn’t stand up or offer anything, since it isn’t like you can use Idris to prove anything about your existing code in some other language.

        Going back to the article, the examples aren’t as detailed as they might be. In the first one, it fails to explain Fin. It also doesn’t make any attempt to introduce the language itself, point to any documentation or anything else until the last bit of the article.

        It gets to explaining a bit about mathematical proofs

        I am assuming that this bit was meant to be funny:

         In the early days of computing (circa 2009 when node.js was created) everyone tried to
         make up for this uncertainty by writing unit tests.

        Getting into one of the next examples, maybe I’m just tired, but it took me a bit to realize that LTE was ‘less than or equal’. (Someone else commented on the linked gist that they had the same problem, so maybe it isn’t just me being tired.)

        Much of the rest of the example contained there is fairly readable, although the jump to the content in the linked gist is pretty large. (Apart from having the offset in the original definitions even though it wasn’t needed until a subsequent step and wasn’t explained well.)

        But then we’re back to the “Not Convinced?” section which again doesn’t bother to take the readers that it is supposedly addressing seriously.

        If this was addressing people familiar with Haskell, then whatever. Many of them are already aware of this sort of thing. But if this is addressing the people who are still stuck doing TDD in other languages that aren’t so mathematically inclined, I don’t think they’ll find it all that useful or respectful.

        1. 3

          Interesting that someone flagged this comment as a troll with no explanation.

          1. 2

            Thanks, this is really informative (and an excellent, high-quality comment).

            Do you think it’s fair to say that your key complaint is that the article is pretending to be written for people doing TDD in dynamic languages, but based on the actual content and what it assumes of the reader, is really aimed at people who already know Idris and/or are convinced of the value of powerful static type systems?

            1. 3

              That’s surely part of it. But the tone and the way he treats the pretend-audience is another part of it. As SeanTAllen said, it is pretty off putting.

              I’ve found Idris interesting for a while (especially as a couple of fellow Dylan people have been involved with it) but don’t have as much time as I’d like to dive in. I’d also be highly interested in seeing how dependent types can be applied in other languages (in particular, I’d like to see http://www.itu.dk/~hame/ilc2010.pdf made production-ready / capable).

        2. 4

          I’m going to agree here. I’ve played with Idris a little, I really like it and I found this to be completely off putting. If this had been my first encounter with Idris, I’m not sure I would think highly of it afterwards. I think there is a lot of really good points that are sadly buried beneath what is a weak idea of “I’ll fake a whitepaper”.

          Dependent typing can solve a large number of TDD related problems simply and that important message gets lost.

          1. -1

            What tone did you project?

            See also: http://rationalwiki.org/wiki/Tone_troll

          2. 2

            Odd presentation aside, this definitely piqued my interest in Idris, in particular the ?wtf variable used to start interactively proving the theorem embedded in the types.

            I was curious enough to go look for official Idris docs (here’s the wiki on github) - I was hoping for just a slightly deeper explanation along the same lines, but mostly ended up in the deep end and gave up. It’d be great to see a similar “here’s how to use dependent types and interactive proving in a real program”, with a little more detail and a little less trollage :)

            1. 4

              Paul Callaghan wrote an amazing series of posts in the PragPub Magazine about functional programming. Later on in the series he dips into a few posts about dependent types in Idris:

              1. http://pragprog.com/magazines/2013-03/uncle-bob-and-functional-programming
              2. http://pragprog.com/magazines/2013-04/dependent-types
              3. http://pragprog.com/magazines/2013-05/dependent-types-part-ii
              4. http://pragprog.com/magazines/2013-06/unification
              5. http://pragprog.com/magazines/2013-07/dependent-types-iii

              I’m including the part of the series covering Idris and dependent types, but if you are interested, he has earlier articles which are very much worth reading.