> If a piece of code uses Applicative or Monad you know it’s behaviour due to the Applicative/Monad mathematical laws.

Well, we actually only know what it is supposed to do. The laws are not enforced, so it is perfectly possible to implement a type class that violates the laws of the type class.

Several test frameworks implement Law Testing which will test your instances for lawfulness as long as you can generate instances of your data structures. E.g. https://hackage.haskell.org/package/hedgehog-classes . So you only need to be able to generate instances and you get comprehensive tests for free, so that's nice too.

It is also the case that implementations of these very abstract classes typically only also have very few implementations that make any kind of sense type-wise and that the 'obvious' one is correct.

(Just to preempt: Yes, tests aren't proof, but such is life without a full proof system in the language. In practice, I've found property-based testing sufficient.)

Oh, I know and I'm not arguing against anything you've said. I just wanted to express - for people who don't know Haskell - that while the laws exist, they are not (as of now ;) enforced or checked by the type checker.

No worries, I was also just trying to add info.

Your observation reminds me of Philip Wadler's Strange Loop talk [1], where he states that some languages are discovered, whereas most languages are merely constructed.

I think he would have agreed to Haskell (or at least, languages based around lambda calculus) is more in the first category, whereas Java, C++, Smalltalk, Javascrip (ie. OO languages) are in the second. Computational fundamentals versus engineering problems.

[1] https://thestrangeloop.com/2015/propositions-as-types.html

But Monads are like what you compose. The equivalent in OO would be the semicolon. You still need business logic that follows messy life / human rules no matter what paradigm you use.

I think these are two wildly opposed world. What the industry calls OO is just a way to try to avoid large business failure. Other paradigms were more about computation, the logical basis is way way deeper. These people like to own all computational layers very precisely from parsing, to compiling, to algorithmic analysis. Enterprise/Application coding is not about that, it's how to bridge the customer / IT gap with something not too horrendous and still adaptable enough to handle market chaos.

I am not seeing how these claims hold up in practice.

> law to say exactly what it is and its expected behaviour/output. What does Monad laws say about expected _behaviors_ of some Monad?

They specify part of the behavior. But at least it always tastes like a burrito!