{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreidmq37n4oif7pwx5anawxbgojotmgz6xjxelaxmdi6a3n3yx4cbf4",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mjpb3ssmezp2"
  },
  "path": "/t/lawvere-theories/13944#post_1",
  "publishedAt": "2026-04-17T14:43:19.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "reply",
    "@apothecalabs",
    "free-category"
  ],
  "textContent": "Expanding on my reply to @apothecalabs, here is how Lawvere theories could be encoded in Haskell.\n\n# Arities\n\nA 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.\n\n\n    {-# LANGUAGE GADTs,\n        KindSignatures,\n        PolyKinds,\n        DataKinds,\n        FlexibleInstances,\n        MultiParamTypeClasses,\n        FlexibleContexts,\n        QuantifiedConstraints #-}\n    module Lawvere where\n    import Prelude hiding (id,(.),fst,snd)\n    import Control.Category\n    import Data.Kind (Type)\n\n    -- * Arities\n\n    -- | Operator arities.\n    -- We would like to use 'GHC.TypeNats.Nat' here as kind,\n    -- but the product of that kind is a type family,\n    -- which can not be partially applied.\n    data Arity = Zero\n        | One\n        | Pair Arity Arity\n\n    type Two = Pair One One\n\n\nAn 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.\n\n\n    -- |  Lawvere's product-preserving functor\n    data F (a :: Type) (n :: Arity) where\n        Zero_ :: F a Zero\n        One_  :: a -> F a One\n        (:*:) :: F a n -> F a m -> F a (Pair n m)\n\n    -- Eq instance needed for property testing\n    instance Eq (F a Zero) where\n        Zero_ == Zero_ = True\n    instance Eq a => Eq (F a One) where\n        (One_ x) == (One_ y) = x == y\n    instance (Eq (F a n), Eq (F a m)) => Eq (F a (Pair n m)) where\n        (x :*: y) == (a :*: b) = x == a && y == b\n\n\n\nFor 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.\n\n# Signatures\n\nFor any particular theory, we therefore only define the **signature** , like so.\n\n\n    data MonoidSignature (x :: Arity) (y :: Arity) where\n        Mempty  :: MonoidSignature Zero One\n        Mappend :: MonoidSignature Two  One\n\n\n\n# Diagrams\n\nNext 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.\n\n\n    -- | Category for diagrams\n    data FreeCartesian (c :: k -> k -> Type) (product :: k -> k -> k) (x :: k) (y :: k) where\n        Id    :: FreeCartesian c p x x\n        Arr   :: c x y -> FreeCartesian c p x y\n        Comp  :: FreeCartesian c p y z -> FreeCartesian c p x y -> FreeCartesian c p x z\n        Prod  :: FreeCartesian c product x y -> FreeCartesian c product x z -> FreeCartesian c product x (product y z)\n        Fst   :: FreeCartesian c product (product x y) x\n        Snd   :: FreeCartesian c product (product x y) y\n        Assoc :: FreeCartesian c product (product (product x y) z) (product x (product y z))\n\n    instance Category (FreeCartesian c product) where\n        id = Id\n        (.) = Comp\n\n    first :: FreeCartesian c product x y -> FreeCartesian c product (product x z) (product y z)\n    first f = Prod (f . Fst) Snd\n\n    second :: FreeCartesian c product x y -> FreeCartesian c product (product z x) (product z y)\n    second f = Prod Fst (f . Snd)\n\n    infixr 3 ***\n\n    (***) :: FreeCartesian c product x y ->\n        FreeCartesian c product a b ->\n        FreeCartesian c product (product x a) (product y b)\n    f *** g = Prod (f . Fst) (g . Snd)\n\n\n\n# Models\n\nNow 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.\n\n\n    class Models (sig :: Arity -> Arity -> Type) (a :: Type) where\n        model :: FreeCartesian sig Pair x y -> F a x -> F a y\n\n\nObserve that, given a product type constructor `product` in some category `c`, the existence of a function\n\n\n    runFree :: FreeCartesian c product x y -> c x y\n\n\nexpresses that the category `c` is Cartesian. **Excercise** : Implement\n\n\n    runFree :: FreeCartesian (->) (,) x y -> x -> y\n\n\nAs an example, we note than any `Monoid` models the `MonoidSignature`.\n\n\n    instance Monoid a => Models MonoidSignature a where\n        model (Arr Mempty) = \\Zero_ -> One_ mempty\n        model (Arr Mappend) = \\((One_ x) :*: (One_ y)) -> One_ (mappend x y)\n        --everything below: mandated by functoriality\n        model Id = id\n        model (Comp f g) = model f . model g\n        model (Prod f g) = \\x -> (model f x) :*: (model g x)\n        model Fst = \\(x :*: _) -> x\n        model Snd = \\(_ :*: y) -> y\n        model Assoc = \\((x :*: y) :*: z) -> x :*: (y :*: z)\n\n\n## Homomorphisms\n\nIn 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.\n\n# Equations and Laws\n\nWe 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.\nWe said that an equation is to be understood as equality between certain morphisms.\n\n\n    infix 0 :=:\n    data Diagram c product x y = FreeCartesian c product x y :=: FreeCartesian c product x y\n\n\nFor example, the universal property of the Cartesian product mandates the equation\n\n\n    Prod Fst Snd :=: Id\n\n\nThe equations of our Lawvere theories will have all different types of arities as input and output, whence we hide these in an existential quantification.\n\n\n    data Laws sig where\n        Law :: Diagram sig Pair x y -> Laws sig\n\n    instance Semigroup (Laws sig) where\n        (Law (lhs :=: rhs)) <> (Law (lhs' :=: rhs')) = Law ((lhs *** lhs') :=: (rhs *** rhs'))\n\n\nYou can think of the mathematical Lawvere theory as the free Cartesian category quotiented by\n\n  1. The laws that make `Pair` the categorical Cartesian product, `Comp` the categorical composition and `Id` the categorical identity,\n  2. The particular laws of the theory, as below.\n\n\n\nHere are the `Monoid` laws. Notice that these are entirely independent of any particular type that might be a monoid.\n\n\n    leftIdentity :: Diagram MonoidSignature Pair (Pair Zero One) One\n    leftIdentity = (Arr Mappend . (Arr Mempty *** Id)) :=: Snd\n\n    rightIdentity :: Diagram MonoidSignature Pair (Pair One Zero) One\n    rightIdentity = (Arr Mappend . (Id *** Arr Mempty)) :=: Fst\n\n    associativity :: Diagram MonoidSignature Pair (Pair Two One) One\n    associativity = (Arr Mappend . first (Arr Mappend)) :=: (Arr Mappend . second (Arr Mappend) . Assoc)\n\n    monoidLaws :: Laws MonoidSignature\n    monoidLaws = Law leftIdentity <> Law rightIdentity <> Law associativity\n\n\nIf Haskell did not already have a `Monoid` type class, we could use\n\n\n    Models MonoidSignature :: Type -> Constraint\n\n\nas a substitute and provide `monoidLaws` as the contract.\n\n# Property Checks\n\nThe 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\n\n\n    forall a. Eq a => forall (n :: Arity). Eq (F a n)\n\n\nholds, 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.\n\n\n    propDiagram :: (Eq (F a n), Models sig a) =>\n        Diagram sig Pair m n ->\n        F a m -> Bool\n    propDiagram (lhs :=: rhs) = \\x -> model lhs x == model rhs x\n\n\nAny 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.\n\n\n    -- | Lifting test case generators to higher arities.\n    -- Likely would be derived generically in a particular testing framework.\n    class CheckableArity (n :: Arity) where\n        liftGen :: Applicative gen => gen a -> gen (F a n)\n    instance CheckableArity Zero where\n        liftGen _ = pure Zero_\n    instance CheckableArity One where\n        liftGen g = One_ <$> g\n    instance (CheckableArity n, CheckableArity m) => CheckableArity (Pair n m) where\n        liftGen g = (:*:) <$> liftGen g <*> liftGen g\n\n\nSince 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.\n\n\n    checkDiagram :: (Eq (F a n), Models sig a, CheckableArity m, Applicative gen) =>\n        Diagram sig Pair m n ->\n        gen a -> gen Bool\n    checkDiagram d g = propDiagram d <$> liftGen g\n\n    checkLaws :: (forall n. Eq (F a n), forall m. CheckableArity m, Applicative gen, Models sig a) =>\n        Laws sig ->\n        gen a -> gen Bool\n    checkLaws (Law eqn) g = checkDiagram eqn g\n\n\n# Conclusion\n\nWe have seen how to capture equational theories with finite arities in a Haskell type class,\n\n\n    class LawvereTheory (signature :: Arity -> Arity -> Type) where\n        laws :: Laws signature\n\n\nand what it means for a particular type to be a model of the theory.\n\n\n    instance LawvereTheory MonoidSignature where\n        laws = monoidLaws\n\n\nSince 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.\n\n\n    associativity :: c (product n n) n ->\n        Diagram c product (product (product n n) n) n\n    associativity op = (Arr op . first  (Arr op))\n                   :=: (Arr op . second (Arr op) . Assoc)\n\n\nFurther, we saw how a model gives rise to testable properties.",
  "title": "Lawvere theories"
}