{
"$type": "site.standard.document",
"bskyPostRef": {
"cid": "bafyreicupccg6svfljmbckhjaw3j5sfanelck2sy3fkgy6jcb7mylbmpme",
"uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mhb73ideggg2"
},
"path": "/t/sneak-peek-bolt-math/13766?page=2#post_21",
"publishedAt": "2026-03-16T21:49:45.000Z",
"site": "https://discourse.haskell.org",
"tags": [
"residuated"
],
"textContent": "Adjoints, anyone?\nLast time I was building something using units, I needed the arithmetic equivalent to symmetric set difference. Take the monoid operation • to be addition in a lattice of non-negative quantities (e.g. energy). This makes this `Semiring`residuated.\n\nTry to take amount `y` from amount `x` where both are non-negative. Conceptually, `x-y` is the unique number such that `y+(x-y) = x`, or, in the language of residuals, subtraction is right adjoint to addition in the lattice of numbers. If all quantities are non-negative (e.g. energy), the proper difference `y-x` must remain a pair and uniqueness is lost. We can, however, choose a canonical representative:\n\n * If `y > x`, then the result is the pair `(0, y-x)` signifying that there was more to take away than what was there.\n * If `x > y` then the result is the pair `(x-y, 0)` signifying what is left over after taking away some.\n\n\n\nI have the impression that primary school kids use a related concept when doing arithmetic involving numbers larger than 10. The fundamental operation being _to split a quantity (number) using a smaller one_.",
"title": "Sneak Peek: Bolt Math"
}