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 programme

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. [0] http://www.cis.upenn.edu/~byorgey/pub/monoid-pearl.pdf http://www.cis.upenn.edu/~byorgey/pub/monoid-pearl.pdf