{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiahkfpiotcaeghefzvkzbel4pfmt42fumadcb65kmm73mkdvkt3yi",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mjrrw23q7tx2"
  },
  "path": "/t/lawvere-theories/13944#post_9",
  "publishedAt": "2026-04-18T15:41:02.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "The signature is almost the less important part to represent though, right? I mean we’re in the class, we’ve got access to the methods of the class, their arities are the arities of the Haskell functions. Writing the laws as `Bool`s outright lets us use the algebra inside `Hask` to model them already. The arity of the constructor is the number of forall quantified variables, and we can use the methods in the RHS of `lawful` rather than encoding them in the type level. The laws aren’t always so tightly coupled to the signature: semirings and lattices have two binary operations (+, * and /\\, \\/), one unary operation (negative and complement), and two nilary operations (0, 1 and bottom, top), but the laws they follow are very different. IMO, it’s easier to encode them at the value level. `Hask` is already a Cartesian category!",
  "title": "Lawvere theories"
}