Lawvere theories

I’ve also been thinking about this! In the end I settled on using the value level and concrete Bools for testing purposes. The Variety class actually closely resembles your original Lawvere but with some minor modifications to increase flexibility.

class Variety (var :: Type -> Constraint) where
  type Requirements var x :: Constraint
  data Signature var :: Type -> Type
  operations :: (var x, Requirements var x) => Signature var x -> x
  data Laws var :: Type -> Type
  lawful :: (var x, Requirements var x) => Laws var x -> Bool

For instance,

data EqLaw x
  = EqLawReflexive x
  | EqLawSymmetric x x
  | EqLawTransitive x x x
  deriving (Eq, Ord, Show)

instance Variety Eq where
  type Requirements Eq x = ()
  data Signature Eq x
  operations :: (Eq x) => Signature Eq x -> x
  operations = \case {}
  newtype Laws Eq x = EqLaw (EqLaw x)
    deriving (Show)
  lawful :: (Eq x) => Laws Eq x -> Bool
  lawful = \case
    EqLaw (EqLawReflexive x) -> x == x
    EqLaw (EqLawSymmetric x y) -> (x == y) --> (y == x)
    EqLaw (EqLawTransitive x y z) -> (x == y && y == z) --> (x == z)

data OrdLaw x
  = OrdLawReflexive x
  | OrdLawAntisymmetric x x
  | OrdLawTransitive x x x
  deriving (Eq, Ord, Show)

instance Variety Ord where
  data Signature Ord x
  operations :: (Ord x) => Signature Ord x -> x
  operations = \case {}
  type Requirements Ord x = ()
  newtype Laws Ord x = OrdLaw (OrdLaw x)
    deriving (Show)
  lawful :: (Ord x) => Laws Ord x -> Bool
  lawful = \case
    OrdLaw (OrdLawReflexive x) -> x <= x
    OrdLaw (OrdLawAntisymmetric x y) -> (x <= y && y <= x) --> (x == y)
    OrdLaw (OrdLawTransitive x y z) -> (x <= y && y <= z) --> (x <= z)

instance Variety Semigroup where
  type Requirements Semigroup x = Eq x
  data Signature Semigroup x
    = SemigroupAppend x x
    deriving (Show)
  operations ::
    (Semigroup x, Requirements Semigroup x) =>
    Signature Semigroup x -> x
  operations = \case
    SemigroupAppend x y -> x <> y
  data Laws Semigroup x
    = SemigroupAppendAssociative x x x
    deriving (Show)
  lawful ::
    (Semigroup x, Requirements Semigroup x) =>
    Laws Semigroup x -> Bool
  lawful = \case
    SemigroupAppendAssociative x y z -> x <> (y <> z) == (x <> y) <> z

instance Variety Monoid where
  type Requirements Monoid x = Eq x
  data Signature Monoid x
    = MonoidSemigroup (Signature Semigroup x)
    | MonoidMempty
    deriving (Show)
  operations ::
    (Monoid x, Requirements Monoid x) =>
    Signature Monoid x -> x
  operations = \case
    MonoidSemigroup sig -> operations sig
    MonoidMempty -> mempty
  data Laws Monoid x
    = MonoidSemigroupLaws (Laws Semigroup x)
    | MonoidMemptyLeft x
    | MonoidMemptyRight x
    deriving (Show)
  lawful ::
    (Monoid x, Requirements Monoid x) =>
    Laws Monoid x -> Bool
  lawful = \case
    MonoidSemigroupLaws laws -> lawful laws
    MonoidMemptyLeft x -> mempty <> x == x
    MonoidMemptyRight x -> x <> mempty == x

I’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 Varietys. 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:

instance (Eq x, Arbitrary x) => Arbitrary (EqLaw x) where
  arbitrary :: Gen (EqLaw x)
  arbitrary =
    oneof
      [ EqLawReflexive <$> arbitrary
      , EqLawSymmetric <$> arbitrary <*> arbitrary
      , EqLawTransitive <$> arbitrary <*> arbitrary <*> arbitrary
      ]

instance (Eq x, Arbitrary x) => Arbitrary (Laws Eq x) where
  arbitrary :: Gen (Laws Eq x)
  arbitrary = EqLaw <$> arbitrary

instance (Eq x, Arbitrary x) => Arbitrary (OrdLaw x) where
  arbitrary :: Gen (OrdLaw x)
  arbitrary =
    oneof
      [ OrdLawReflexive <$> arbitrary
      , OrdLawAntisymmetric <$> arbitrary <*> arbitrary
      , OrdLawTransitive <$> arbitrary <*> arbitrary <*> arbitrary
      ]

instance (Eq x, Arbitrary x) => Arbitrary (Laws Ord x) where
  arbitrary :: Gen (Laws Ord x)
  arbitrary = OrdLaw <$> arbitrary

instance (Eq x, Arbitrary x) => Arbitrary (Laws Semigroup x) where
  arbitrary :: Gen (Laws Semigroup x)
  arbitrary = SemigroupAppendAssociative <$> arbitrary <*> arbitrary <*> arbitrary

instance (Eq x, Arbitrary x) => Arbitrary (Laws Monoid x) where
  arbitrary :: Gen (Laws Monoid x)
  arbitrary = MonoidSemigroupLaws <$> arbitrary