Why is a lawful type class-based ecosystem so appealing to PureScript and Haskell community?

#1

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?

1 Like
#2

It’s not quite what you were asking about, but I really like this piece:

2 Likes
#3

I don’t think this is particularly unique to Purescript. For example, look at the documentation for the equals method in Java. It describes the laws that apply to this function, and the rest of the standard library (e.g. the HashMap class) assume that these laws will be followed.

I guess the part of your question I would agree with is that laws are not a priori useful because they are based in mathematics. The contract of the equals() method is important because it enables someone to write a useful data structure, not because it happens to be defined mathematically

3 Likes