Lawvere theories

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 Bools 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!