Hi, I wrote a new blog post about substitution and equational reasoning, a topic I feel is really important to practice when learning Haskell. Hope it helps anyone:
https://gilmi.me/blog/post/2020/10/01/substitution-and-equational-reasoning
Extremely clear, excellent!
Thank you! I really appreciate the feedback 
I will ask a question then: since with impl the substitution result is — or should be:
(1 * (2 * (3*1)))
have we gained anything by using a counter instead of the naive version?
That’s a good question. If we were in a strict language like Purescript where all arguments to a function are evaluated before applying them to the function, then the answer was yes.
But in Haskell, even though you see such program change presented as a solution in places like cs240h, naively, this wouldn’t change anything for us.
It is possible that GHC would figure out that acc should be evaluated strictly, but this is not a topic I’m too knowledgeable in and I’m not 100% confident that it would.
For that, a good solution to this problem, as is hinted in the article, is to add a ! before acc in the function arguments definition (\ !acc n ->) to force the evaluation of acc before entering the function, using the BangPatterns extension.
And then, the rewritten implementation will definitely be better then the original