Conversation
QuickCheck/Hedgehog break laws!??
1
Because of the implementation using splittable RNGs (to enable generating infinite structures), reassociating your applicative/monadic computation can change which random number you get.
2
Although all our laws depend on a vague notion of equality. Which = do the monad laws use? It can't always be Haskell's Eq, because we would agree that ((->) r) is a monad but ((->) r a) is never Eq.
2
Isn’t this related to the problem of functional extensionality (ie. can be hard to agree on when functions are equal) and why its hard to do category theory in type theory? Still learning, so could be wrong about this 😅
it's related but more basically: laws are respect to "equality" - which we don't define. In practice, not much of a problem. Usually we can tell if we have the "same program"
1
for things like Agda, things like VerifiedMonoid have to abstract over the equality relation, because propositional equality is just one form and doesn't work on things like codata (where you want to use a specific relation for type, representing its bisimulation)
1