{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreicnkd57nwntvjcnvee5b4ionwoiicfdb6fcbq34yijixwcufwbo2m",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mhpyk6vl2ae2"
  },
  "path": "/t/sneak-peek-bolt-math/13766?page=2#post_35",
  "publishedAt": "2026-03-22T22:55:40.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "olf:\n\n> I feel (but can not prove) that this will not get you very far. […]\n\nYes, this approach worked for simple laws, but I’ve already found it does not scale well, especially for laws that invoke other laws. Take for example the `trimedial` relation, which states that any 3 elements generate a subset that has the `medial` property, which is `wx * yz = wy * xz`, so it has 3^4 = 81 combinations to test _just in the first generation_ , and it continues going, so yeah. Some laws just cannot be proven by exhaustive iteration.\n\nI’m not surprised, I hadn’t really even planned on doing any heavy algebraic laws in this library, it was more for vector and geometric spaces and I had to deal with the `Num` hierarchy because it was _in the way,_ but when people mentioned algebraic laws, it I wanted to see what I could do, so this was a bit spur of the moment, and I got a lot further than I expected.\n\nAnother problem that I’ve discovered in this design is an insufficient description / separation of properties vs the functions that define them - take for example ‘identity’, we have (using addition to illustrate):\n\n  * the identity element, 0\n  * the identity law, x + 0 = x\n  * the identity definition using inverse, 0 = x + (-x)\n\n\n\nYou might think that these belong in the same class, but no, they don’t because you can define identity elements without inverses (eg addition over natural numbers). And then there are things with left and right identities that unify, etc. All things that could and should be described better.\n\nolf:\n\n> Why don’t you do it the categorical way and describe diagrams that ought to commute?\n\nI’ll give this approach some thought, as it also might help with considering left and right laws, and how to handle them.\n\nolf:\n\n> So you have gained no static guarantees, only more convenient ways to write test suites.\n\nWe mustn’t let perfect be the enemy of good - I think that is still a worthwhile benefit, being able to generate tests and test suites automatically based on laws, it might help provide an alternative to people writing `-- INVARIANT: Foo` in the code and then writing tests in a separate place to back it up.\n\n* * *\n\nSo definitely more work to be done, but the best time to plant a tree for shade is 20 years ago, and the second best time is today. The improvements to the definition of `Semigroup` `Monoid` and `Group` alone have made this worth it for me.",
  "title": "Sneak Peek: Bolt Math"
}