New blog post: Substitution and Equational Reasoning

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

3 Likes

Extremely clear, excellent!

1 Like

Thank you! I really appreciate the feedback :slight_smile:

1 Like

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 :slight_smile:

1 Like