{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiabq7wsp5h4dcvk4dnudw72x6eyykugltvzq2x5to7e3snpvblce4",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mhoozv3jkxv2"
  },
  "path": "/t/sneak-peek-bolt-math/13766?page=2#post_34",
  "publishedAt": "2026-03-22T22:02:40.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "ApothecaLabs:\n\n>\n>     class (Operation r a b) => Lawful r a b where\n>         lawful :: a -> b -> Bool\n>\n\nI 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.\nOf 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.\n\nWhy 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”.\n\n\n    associative :: Semigroup a => (a,a,a) -> (a,a)\n    associative (x,y,z) = (x <> (y <> z), (x <> y) <> z)\n\n\nWhenever `Eq a` is in scope, you can still post-compose with `uncurry (==)` and obtain the `lawful` test.\n\nApothecaLabs:\n\n> Specifically, this class doesn’t assert that it _is_ lawful in general, but rather, that we can check whether a particular operation is lawful.\n\nSo you have gained no static guarantees, only more convenient ways to write test suites.",
  "title": "Sneak Peek: Bolt Math"
}