{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreid55tf67a2c4ratrdl6lqewulipxa6kn66zgih2lh7zthkkuqbkvi",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mjpi3esvzgt2"
  },
  "path": "/t/lawvere-theories/13944#post_2",
  "publishedAt": "2026-04-17T16:33:36.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "I’ve also been thinking about this! In the end I settled on using the value level and concrete `Bool`s for testing purposes. The `Variety` class actually closely resembles your original `Lawvere` but with some minor modifications to increase flexibility.\n\n\n    class Variety (var :: Type -> Constraint) where\n      type Requirements var x :: Constraint\n      data Signature var :: Type -> Type\n      operations :: (var x, Requirements var x) => Signature var x -> x\n      data Laws var :: Type -> Type\n      lawful :: (var x, Requirements var x) => Laws var x -> Bool\n\n\nFor instance,\n\n\n    data EqLaw x\n      = EqLawReflexive x\n      | EqLawSymmetric x x\n      | EqLawTransitive x x x\n      deriving (Eq, Ord, Show)\n\n    instance Variety Eq where\n      type Requirements Eq x = ()\n      data Signature Eq x\n      operations :: (Eq x) => Signature Eq x -> x\n      operations = \\case {}\n      newtype Laws Eq x = EqLaw (EqLaw x)\n        deriving (Show)\n      lawful :: (Eq x) => Laws Eq x -> Bool\n      lawful = \\case\n        EqLaw (EqLawReflexive x) -> x == x\n        EqLaw (EqLawSymmetric x y) -> (x == y) --> (y == x)\n        EqLaw (EqLawTransitive x y z) -> (x == y && y == z) --> (x == z)\n\n    data OrdLaw x\n      = OrdLawReflexive x\n      | OrdLawAntisymmetric x x\n      | OrdLawTransitive x x x\n      deriving (Eq, Ord, Show)\n\n    instance Variety Ord where\n      data Signature Ord x\n      operations :: (Ord x) => Signature Ord x -> x\n      operations = \\case {}\n      type Requirements Ord x = ()\n      newtype Laws Ord x = OrdLaw (OrdLaw x)\n        deriving (Show)\n      lawful :: (Ord x) => Laws Ord x -> Bool\n      lawful = \\case\n        OrdLaw (OrdLawReflexive x) -> x <= x\n        OrdLaw (OrdLawAntisymmetric x y) -> (x <= y && y <= x) --> (x == y)\n        OrdLaw (OrdLawTransitive x y z) -> (x <= y && y <= z) --> (x <= z)\n\n    instance Variety Semigroup where\n      type Requirements Semigroup x = Eq x\n      data Signature Semigroup x\n        = SemigroupAppend x x\n        deriving (Show)\n      operations ::\n        (Semigroup x, Requirements Semigroup x) =>\n        Signature Semigroup x -> x\n      operations = \\case\n        SemigroupAppend x y -> x <> y\n      data Laws Semigroup x\n        = SemigroupAppendAssociative x x x\n        deriving (Show)\n      lawful ::\n        (Semigroup x, Requirements Semigroup x) =>\n        Laws Semigroup x -> Bool\n      lawful = \\case\n        SemigroupAppendAssociative x y z -> x <> (y <> z) == (x <> y) <> z\n\n    instance Variety Monoid where\n      type Requirements Monoid x = Eq x\n      data Signature Monoid x\n        = MonoidSemigroup (Signature Semigroup x)\n        | MonoidMempty\n        deriving (Show)\n      operations ::\n        (Monoid x, Requirements Monoid x) =>\n        Signature Monoid x -> x\n      operations = \\case\n        MonoidSemigroup sig -> operations sig\n        MonoidMempty -> mempty\n      data Laws Monoid x\n        = MonoidSemigroupLaws (Laws Semigroup x)\n        | MonoidMemptyLeft x\n        | MonoidMemptyRight x\n        deriving (Show)\n      lawful ::\n        (Monoid x, Requirements Monoid x) =>\n        Laws Monoid x -> Bool\n      lawful = \\case\n        MonoidSemigroupLaws laws -> lawful laws\n        MonoidMemptyLeft x -> mempty <> x == x\n        MonoidMemptyRight x -> x <> mempty == x\n\n\nI’ve also been working with an extended algebraic hierarchy with `Variety` instances for them. Additive groups, semirings, rings, fields, modules and vector spaces, all expressible as `Variety`s. It also lets one model the type of “arity” directly as a Haskell datatype instead of having to (or getting to, depending on your perspective  ) define the arities explicitly. This makes it easy to derive `Generic` for `Laws var x`, giving light work to the deriving strategies for test generators. Generatable boilerplate below:\n\n\n    instance (Eq x, Arbitrary x) => Arbitrary (EqLaw x) where\n      arbitrary :: Gen (EqLaw x)\n      arbitrary =\n        oneof\n          [ EqLawReflexive <$> arbitrary\n          , EqLawSymmetric <$> arbitrary <*> arbitrary\n          , EqLawTransitive <$> arbitrary <*> arbitrary <*> arbitrary\n          ]\n\n    instance (Eq x, Arbitrary x) => Arbitrary (Laws Eq x) where\n      arbitrary :: Gen (Laws Eq x)\n      arbitrary = EqLaw <$> arbitrary\n\n    instance (Eq x, Arbitrary x) => Arbitrary (OrdLaw x) where\n      arbitrary :: Gen (OrdLaw x)\n      arbitrary =\n        oneof\n          [ OrdLawReflexive <$> arbitrary\n          , OrdLawAntisymmetric <$> arbitrary <*> arbitrary\n          , OrdLawTransitive <$> arbitrary <*> arbitrary <*> arbitrary\n          ]\n\n    instance (Eq x, Arbitrary x) => Arbitrary (Laws Ord x) where\n      arbitrary :: Gen (Laws Ord x)\n      arbitrary = OrdLaw <$> arbitrary\n\n    instance (Eq x, Arbitrary x) => Arbitrary (Laws Semigroup x) where\n      arbitrary :: Gen (Laws Semigroup x)\n      arbitrary = SemigroupAppendAssociative <$> arbitrary <*> arbitrary <*> arbitrary\n\n    instance (Eq x, Arbitrary x) => Arbitrary (Laws Monoid x) where\n      arbitrary :: Gen (Laws Monoid x)\n      arbitrary = MonoidSemigroupLaws <$> arbitrary\n",
  "title": "Lawvere theories"
}