If you're going to call your article "at scale", the least you can do is give examples that can't already be found everywhere on the Internet explaining monoids, monads, applicatives and functors. Reading from the terminal doesn't qualify as an "at scale" example of Haskell.<p>Explain how to make HTTP requests, query databases, load balance web servers or write GUI's. And then explain how equational reasoning can be useful there.<p>My personal experience is that equational reasoning quickly falls apart as soon as you go beyond toy examples such as the ones shown in this article, but I'm dying to be proven wrong.
"Pearls of functional algorithm design" [0] is a fantastic book if you are interested in some more equational reasoning, I highly recommend it.<p>[0] <a href="http://www.amazon.co.uk/Pearls-Functional-Algorithm-Design-Richard/dp/0521513383" rel="nofollow">http://www.amazon.co.uk/Pearls-Functional-Algorithm-Design-R...</a>
He means scaling over the dimension of complexity - not web-scale, over performance/efficiency/throughput etc. Perhaps it would be clearer to include "complexity" in the title, but to be fair, complexity always has been and always will be the problematic scaling dimension of programming.<p>There's a pedagogical difficulty in showing a very complex problem: the article is already quite long, and just the showing of a complex problem is, well, complex. It reminds me of the difficulty of teaching a one-semester course in Software Engineering: you need a large project before software engineering principles start to be needed; but developing a large project is more than semester's work in itself...<p>I'm not sure there is an answer to this, for equational reasoning. It seems some tradeoff/sacrifice is needed; something must be given up. Maybe: only summarise the project and sketch out the proof (like those of professional mathematicians) - the tradeoff is that this is no longer elementary from first principles, and would be inaccessible to newcomers. Maybe a "201" blog post, that has as prerequisites some of your "101" blog posts?<p>There's certainly a need to have an actual complex project to prove. Could be one of your own; building one specifically for this (so the complexity is not overwhelming; and minimize interactions); or choose some existing complex project off the shelf. Probably needs to be an objectively convincingly complex one (so not one that is intrinsically tied to addressing problems within Haskell itself). For example, not an IO monad, but some application that is complex no matter what language it's written in.<p>Ironically, perhaps some of the "web-scale" examples would be most complelling...<p><i>EDIT</i> just saw some of your comments, and it looks like you're doing pretty much this already. :)
Not the best explanation for "at scale". A toy implementation of map-reduce would have gone a bit farther in showing that yes, monoids are fundamental to a lot of scalable things.
This is really toy example, and there's nothing special about it. Languages like Agda, Coq, Idris support this for quite a long time. And unlike what the author wrote, all the reasoning is checked formally.<p>In Agda it looks like this: <a href="https://github.com/solomatov/AgdaSandbox/blob/master/Monoid.agda" rel="nofollow">https://github.com/solomatov/AgdaSandbox/blob/master/Monoid....</a> Here we prove that in a monoid if a inverse element exists, then it's unique.
What I find weird about Haskell and its touted equational reasoning and all, is that there doesn't seem to be any program for aiding in and/or checking these proofs. (All examples of it I've seen are 'with pen and paper'. And while that might be a great/good enough way for beginners, I would expect that bigger/more serious applications of it would welcome the chance of having a program verify the proof steps for them.)<p>It doesn't seem that hard, at least when it comes to these algebraic proofs; let the programmer build up proofs and lemmas by applying legal equational substitutions. Then let him reuse them in new proofs. The only responsibility of the program might be that it checks that all transitions are legal. Then you just have a verifier/checker, not even an automatic prover or anything. Does anything like this exist?