Expanding on my reply to @apothecalabs, here is how Lawvere theories could be encoded in Haskell.

Arities

A Lawvere theory is a finitary equational theory. The first thing we therefore need is arities. We would like to use GHC.TypeNats but the fact that the product (*) of Nat is a type familiy and can therefore not be partially applied, hinders their use. We therefore conjure something equivalent.

{-# LANGUAGE GADTs,
    KindSignatures,
    PolyKinds,
    DataKinds,
    FlexibleInstances,
    MultiParamTypeClasses,
    FlexibleContexts,
    QuantifiedConstraints #-}
module Lawvere where
import Prelude hiding (id,(.),fst,snd)
import Control.Category
import Data.Kind (Type)

-- * Arities

-- | Operator arities.
-- We would like to use 'GHC.TypeNats.Nat' here as kind,
-- but the product of that kind is a type family,
-- which can not be partially applied.
data Arity = Zero
    | One
    | Pair Arity Arity

type Two = Pair One One

An algebra in a Lawvere theory is a product-preserving functor F from a category that has arities as objects to a target category, which will be (->) in our case.

-- |  Lawvere's product-preserving functor
data F (a :: Type) (n :: Arity) where
    Zero_ :: F a Zero
    One_  :: a -> F a One
    (:*:) :: F a n -> F a m -> F a (Pair n m)

-- Eq instance needed for property testing
instance Eq (F a Zero) where
    Zero_ == Zero_ = True
instance Eq a => Eq (F a One) where
    (One_ x) == (One_ y) = x == y
instance (Eq (F a n), Eq (F a m)) => Eq (F a (Pair n m)) where
    (x :*: y) == (a :*: b) = x == a && y == b

For every type a, the type constructor F a has kind Arity -> Type and essentially sends 0 to (), 1 to a, 2 to (a,a) and so forth. We are going to model the morphisms in Lawvere’s category using a free construction.

Signatures

For any particular theory, we therefore only define the signature , like so.

data MonoidSignature (x :: Arity) (y :: Arity) where
    Mempty  :: MonoidSignature Zero One
    Mappend :: MonoidSignature Two  One

Diagrams

Next we set up the category in which to express our equations as diagrams. These will be commutative squares, triangles etc. What we define below is very similar to the free Arrow from the free-category package, only that it is poly-kinded. The product parameter is the reason why we can not use GHC.TypeNats.Nat as k, as it’s product is a type family and newtype-wrapping it would destroy the k -> k -> k signature.

-- | Category for diagrams
data FreeCartesian (c :: k -> k -> Type) (product :: k -> k -> k) (x :: k) (y :: k) where
    Id    :: FreeCartesian c p x x
    Arr   :: c x y -> FreeCartesian c p x y
    Comp  :: FreeCartesian c p y z -> FreeCartesian c p x y -> FreeCartesian c p x z
    Prod  :: FreeCartesian c product x y -> FreeCartesian c product x z -> FreeCartesian c product x (product y z)
    Fst   :: FreeCartesian c product (product x y) x
    Snd   :: FreeCartesian c product (product x y) y
    Assoc :: FreeCartesian c product (product (product x y) z) (product x (product y z))

instance Category (FreeCartesian c product) where
    id = Id
    (.) = Comp

first :: FreeCartesian c product x y -> FreeCartesian c product (product x z) (product y z)
first f = Prod (f . Fst) Snd

second :: FreeCartesian c product x y -> FreeCartesian c product (product z x) (product z y)
second f = Prod Fst (f . Snd)

infixr 3 ***

(***) :: FreeCartesian c product x y ->
    FreeCartesian c product a b ->
    FreeCartesian c product (product x a) (product y b)
f *** g = Prod (f . Fst) (g . Snd)

Models

Now a model of a particular theory is a functor from the free cartesian category over the signature to the category of Haskell types and functions.

class Models (sig :: Arity -> Arity -> Type) (a :: Type) where
    model :: FreeCartesian sig Pair x y -> F a x -> F a y

Observe that, given a product type constructor product in some category c, the existence of a function

runFree :: FreeCartesian c product x y -> c x y

expresses that the category c is Cartesian. Excercise : Implement

runFree :: FreeCartesian (->) (,) x y -> x -> y

As an example, we note than any Monoid models the MonoidSignature.

instance Monoid a => Models MonoidSignature a where
    model (Arr Mempty) = \Zero_ -> One_ mempty
    model (Arr Mappend) = \((One_ x) :*: (One_ y)) -> One_ (mappend x y)
    --everything below: mandated by functoriality
    model Id = id
    model (Comp f g) = model f . model g
    model (Prod f g) = \x -> (model f x) :*: (model g x)
    model Fst = \(x :*: _) -> x
    model Snd = \(_ :*: y) -> y
    model Assoc = \((x :*: y) :*: z) -> x :*: (y :*: z)

Homomorphisms

In a Lawvere theory, a homomorphism between models a and b is a natural transformation between two functors F a and F b. We do not cover homomorphisms in this post.

Equations and Laws

We have not expressed a single equation yet. Of course being a Cartesian category already mandates certain equations to hold between the elements of our representation FreeCartesian, but we brush these under the carpet for now. We said that an equation is to be understood as equality between certain morphisms.

infix 0 :=:
data Diagram c product x y = FreeCartesian c product x y :=: FreeCartesian c product x y

For example, the universal property of the Cartesian product mandates the equation

Prod Fst Snd :=: Id

The equations of our Lawvere theories will have all different types of arities as input and output, whence we hide these in an existential quantification.

data Laws sig where
    Law :: Diagram sig Pair x y -> Laws sig

instance Semigroup (Laws sig) where
    (Law (lhs :=: rhs)) <> (Law (lhs' :=: rhs')) = Law ((lhs *** lhs') :=: (rhs *** rhs'))

You can think of the mathematical Lawvere theory as the free Cartesian category quotiented by

1. The laws that make Pair the categorical Cartesian product, Comp the categorical composition and Id the categorical identity,
2. The particular laws of the theory, as below.

Here are the Monoid laws. Notice that these are entirely independent of any particular type that might be a monoid.

leftIdentity :: Diagram MonoidSignature Pair (Pair Zero One) One
leftIdentity = (Arr Mappend . (Arr Mempty *** Id)) :=: Snd

rightIdentity :: Diagram MonoidSignature Pair (Pair One Zero) One
rightIdentity = (Arr Mappend . (Id *** Arr Mempty)) :=: Fst

associativity :: Diagram MonoidSignature Pair (Pair Two One) One
associativity = (Arr Mappend . first (Arr Mappend)) :=: (Arr Mappend . second (Arr Mappend) . Assoc)

monoidLaws :: Laws MonoidSignature
monoidLaws = Law leftIdentity <> Law rightIdentity <> Law associativity

If Haskell did not already have a Monoid type class, we could use

Models MonoidSignature :: Type -> Constraint

as a substitute and provide monoidLaws as the contract.

Property Checks

The type Laws is rather abstract, though. Let’s look at how the laws could be property-checked using a testing framework such as QuickCheck. Remember that we defined Eq instances for our F a functor. Unfortunately, I can’t seem to convice GHC that

forall a. Eq a => forall (n :: Arity). Eq (F a n)

holds, even though we covered all type constructors of Arity in our derivations. Nevertheless, we use the Eq instances to write a transformer from diagrams to properties.

propDiagram :: (Eq (F a n), Models sig a) =>
    Diagram sig Pair m n ->
    F a m -> Bool
propDiagram (lhs :=: rhs) = \x -> model lhs x == model rhs x

Any decent testing framework, like QuickCheck, would be able to infer test case generators for types like F a Two given a generator for a. For the sake of generality, we capture this in a custom type class.

-- | Lifting test case generators to higher arities.
-- Likely would be derived generically in a particular testing framework.
class CheckableArity (n :: Arity) where
    liftGen :: Applicative gen => gen a -> gen (F a n)
instance CheckableArity Zero where
    liftGen _ = pure Zero_
instance CheckableArity One where
    liftGen g = One_ <$> g
instance (CheckableArity n, CheckableArity m) => CheckableArity (Pair n m) where
    liftGen g = (:*:) <$> liftGen g <*> liftGen g

Since we hid the arities in an existential quantification in Laws, we must add universally quantified constraints (which we are unable to prove, needs the principle of induction) as a context for a general property checker.

checkDiagram :: (Eq (F a n), Models sig a, CheckableArity m, Applicative gen) =>
    Diagram sig Pair m n ->
    gen a -> gen Bool
checkDiagram d g = propDiagram d <$> liftGen g

checkLaws :: (forall n. Eq (F a n), forall m. CheckableArity m, Applicative gen, Models sig a) =>
    Laws sig ->
    gen a -> gen Bool
checkLaws (Law eqn) g = checkDiagram eqn g

Conclusion

We have seen how to capture equational theories with finite arities in a Haskell type class,

class LawvereTheory (signature :: Arity -> Arity -> Type) where
    laws :: Laws signature

and what it means for a particular type to be a model of the theory.

instance LawvereTheory MonoidSignature where
    laws = monoidLaws

Since the signature of any particular theory is a GADT, it is easy to re-use signatures in defining hierarchical theories. Likewise, our FreeCartesian has enough type parameters to express equations that can hold in many theories at once, e.g.

associativity :: c (product n n) n ->
    Diagram c product (product (product n n) n) n
associativity op = (Arr op . first  (Arr op))
               :=: (Arr op . second (Arr op) . Assoc)

Further, we saw how a model gives rise to testable properties.