{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreifvy5rwwqvdu4zum3fsyvmlny76yhui2gnlnh2n3vzbcxf4h63zyy",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mjpi3a3bu3e2"
  },
  "path": "/t/lawvere-theories/13944#post_3",
  "publishedAt": "2026-04-17T17:31:45.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "I’m only barely grasping everything you’ve got here, but it seems really cool. Encoding in data types the laws something must follow is really neat, especially when the types become so “tight” the answer must pop right out (as I think is done with the arities and signatures for `FreeCartesian`.\n\nolf:\n\n> `F (a :: Type) (n :: Arity)`\n\nWith the above, it is described as a functor; could we make it into a proper haskell function by just swapping `n` and `a`?\n\nI’d personally appreciate further elaboration here if that’s possible.\n\nThought that just popped into my head; how possible would it be to TH’ify the laws and proof for this sort of thing and then have compile time verification that the laws are followed? Or is this construction not powerful enough for that kind of “proof”, and it’s merely just setting up for quickchecking (which we certainly shouldn’t do at compile time).",
  "title": "Lawvere theories"
}