{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiajk2ii5bw4cachvthoyw3egcrtlzqm474opcazjqdwgytusfxdny",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mhq7agr7wwp2"
  },
  "path": "/t/sneak-peek-bolt-math/13766?page=2#post_36",
  "publishedAt": "2026-03-23T08:00:36.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "Lawvere theories"
  ],
  "textContent": "Do you know about Lawvere theories? The unifying approach to laws there is to have a signature associated with a class of algebraic objects. In Haskell, we could hide the arity of the signature in a type family. Roughly speaking,\n\n\n    class Lawvere (theory :: Type -> Constraint) where\n       type Signature theory :: Type -> Type\n       operations :: theory a => Signature theory a -> a\n       type Laws theory :: Type -> Type\n       lawful :: (theory a, Eq a) => Laws theory a -> Bool\n\n    data MonoidLaws a where\n       NeutralLeft :: a -> MonoidLaws a\n       NeutralRight :: a -> MonoidLaws a\n       Assoc :: a -> a -> a -> MonoidLaws a\n    lawfulMonoid :: (Monoid a, Eq a) => MonoidLaws a -> Bool\n    lawfulMonoid (NeutralLeft a) = a == mempty `mappend` a\n    lawfulMonoid (NeutralRight a) = a == a `mappend` mempty\n    lawfulMonoid (Assoc x y z) = mappend (mappend x y) z == mappend x (mappend y z)\n\n    instance Lawvere Monoid where\n       type Signature Monoid a = Either () (a,a)\n       operations (Left ()) = mempty\n       operations (Right (x,y)) = mappend x y\n       type Laws Monoid a = MonoidLaws a\n       lawful = lawfulMonoid\n\n\nApothecaLabs:\n\n> Another problem that I’ve discovered in this design is an insufficient description / separation of properties vs the functions that define them\n\nLawvere combined the signature and laws in a single category L (objects = arities, morphisms = laws) and instances of the theory (models) are then functors from this category. Homomorphisms are natural transformations between such functors.\n\nFor the sake of efficiency, one could formulate the laws as Haskell rewrite rules.",
  "title": "Sneak Peek: Bolt Math"
}