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.
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.
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.
That shows a spreadsheet that you assemble using Applicative and Monoid operations that is built on top of several abstraction layers, and the correctness proof of each layer buulds on the previous proofs.
I personally feel that this post has missed a huge opportunity to show how to do much more complex things from smaller pieces with trivial proofs providing high assurance. I wish the example application had been something far more interesting and useful; at the moment it's a poor implementation of tee. Too much theory without any discussion of how it's actually useful (which it definitely is! it's just not articulated).
I do plan on writing up a longer example, but I wanted to get the basic idea out there first so that I could just link to it in the follow-up post. The example I'm building up to is quite long and would have easily tripled the size of the post if I had included the entire thing inline.
I've gotten through around half of it – the material itself is not extremely difficult, but it does take a long time to go line by line and see how exactly line `n` is equivalent to line `n-1` in the program transformations presented. Basic haskell knowledge is also a prerequisite, you will want to be following along and coding up the chapters as you read it.
For when you end up reading it so that you are not pulling your hair out as to why the code isn't working: there is a code error in chapter 4.
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.
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...
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?
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.
Ironically, perhaps some of the "web-scale" examples would be most complelling...
EDIT just saw some of your comments, and it looks like you're doing pretty much this already. :)
I think this blog post does a good job of showing how proofs of simple parts extend into proofs of increasingly complicated wholes, without additional programmer effort. Is there a reason you'd expect this to fall over on yet more complex types?
If you're looking for a 'real world' use of the monoid laws and the way the compiler can build them up for you, you might want to have a look at [0] Monoids: Themes and Variations, where the author shows how these ideas work themselves out in a quite nontrivial diagramming library.
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.
Gabriel, I've noticed your posts often attract this criticism - "you can do X in any language, it's not unique to Haskell". The funny thing is I don't think you ever claim that X is unique to Haskell. IMHO this (excellent) post advocates equational reasoning a lot more strongly than it advocates Haskell.
Assuming your aim is to spread awareness of the advantages of pure functional programming, rather than of Haskell specifically, I wonder if your Haskell-specific domain name is muddling your message?
Yeah, the domain name is misleading. It really should be called "Equational reasoning for all". I'm reluctant to change it at this point, but I think I should make more of an effort to clarify that the posts are advocacy for purely functional programming languages, including Idris in particular since it is maturing quite rapidly.
Tonight I will revise this post to be less Haskell-centric by mentioning that most of what it describes applies to other purely functional languages and also mention how dependently typed languages can improve and mechanically check the proof process.
I'm actually not aware of a proof in the wild equivalent to the one in Appendix B. If you know of a machine checked proof that Applicatives lift Monoids then I would be happy to link to it.
This is an excellent suggestion. I will take a stab at this, but probably in Idris first if you don't mind. If I succeed then I will write about what I learned.
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.)
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?
It's a continuum of how much checking/proving you want to do.
Assuming that all Monoid instances obey the monoid laws is a pretty reasonable thing to do even if you haven't proven every single instance yourself. It's the same as assuming that a Set<T> in e.g. Java actually obeys the set abstraction: has no duplicates, ordering is not guaranteed, etc. In practice the laws associated with type classes are a bit better specified in Haskell via either terse (algebraic) documentation or default implementations of associated functions. It would perhaps be nice if libraries which export type classes came with test functions that could be used to test your instances using some sort of QuickCheck-like approach.
Though I've personally found that Haskell is sufficient at least my purposes, Idris currently seems the most "practical" of the dependently typed languages, but it's quite young and doesn't really have any ecosystem to speak of AFAICT.
There's a good screencast of this being done with Idris, which has tools like you mentioned for interactively solving proofs. In it, the author proves that an instance of Monoid upholds its 'laws': properties like associativity that are only upheld by convention in Haskell.
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.
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.