This is a largely philosophical post. I leave an open question at the end. I thought it was an interesting thought process that I hadn’t heard before, so I hope it’s interesting to someone else here!
A relatively large portion of the Haskell and now PureScript communities seems to hold the opinion that lawful type classes are pretty great, and moreover that those lawful type classes which come from mathematics are pretty great.
I was reading some mathematics the other day when I realized, “Wait, this entire book makes sense only if laws of elementary algebra hold. And some of these theorems only hold in the situation of X and Y both being this certain type of structure. If any X or Y is found to not be that certain type of that structure, then all the theorems built on that idea fall apart! Well, in that case, we can just modify X and Y to give them that certain type of structure, then we are back on The Happy Path! Wait! We can do that in the software world!”.
So yeah, I think mathematics stands long through time and develops based around laws because logical deductions can only be defined in terms of laws (which I’d like to start calling invariants for my point of view here). Logic has roots in the nature of oratory arguments, and oratory arguments are reflections of human thought processes (roughly). So, if we want to have software which is easy to reason about, we need to have software which is built on invariants!
If so, which sorts of invariants are good invariants on which to build software? Is there something special about the invariants we imported into the PureScript ecosystem from mathematics? Or perhaps the specific invariants we choose doesn’t matter, so long as they are invariant through the life of the software?
I’ll end this thought here. What do you think?