Sneak Peek: Bolt Math

ApothecaLabs:

class (Operation r a b) => Lawful r a b where
    lawful :: a -> b -> Bool

I feel (but can not prove) that this will not get you very far. One reason is that not all laws are decidable, because Result r a b might not even have a decent Eq instance that lawful can use. (E.g. point-wise operations on function spaces.) The other case where this fails is when the law involves universal quantification, possibly not only over the elements of a and b but also over type variables. Think about the Monad laws. Of course you can keep adding type parameters to Lawful to cater for all the universal quantification, but the discussion on arity shows that this will be very tricky at best.

Why don’t you do it the categorical way and describe diagrams that ought to commute? For example, the associative law diagram has as starting point a triple and two paths that should be equal. But since equality may not be decidable, we just yield a pair that we require to be “morally equal”.

associative :: Semigroup a => (a,a,a) -> (a,a)
associative (x,y,z) = (x <> (y <> z), (x <> y) <> z)

Whenever Eq a is in scope, you can still post-compose with uncurry (==) and obtain the lawful test.

ApothecaLabs:

Specifically, this class doesn’t assert that it is lawful in general, but rather, that we can check whether a particular operation is lawful.

So you have gained no static guarantees, only more convenient ways to write test suites.