Lawvere theories

[olf]

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)
import Data.Function (on)

-- * 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)

-- | forgets the statically known length 
argList :: F a n -> [a]
argList Zero_ = []
argList (One_ a) = [a]
argList (a1 :*: a2) = argList a1 ++ argList a2

-- Eq instance needed for property testing
instance Eq a => Eq (F a n) where
    (==) = (==) `on` argList

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. The functor must be product-preserving, whence we take the object mapping of the functor to be F. The function model defined below is the morphism part of the functor.

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. 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 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.

[mixphix]

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
  type Requirements Ord x = ()
  data Signature Ord x
  operations :: (Ord x) => Signature Ord x -> x
  operations = \case {}
  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 =
    oneof
      [ MonoidSemigroupLaws <$> arbitrary
      , MonoidMemptyLeft <$> arbitrary
      , MonoidMemptyRight <$> arbitrary
      ]

[L0neGamer]

I’m only barely grasping everything you’ve got here, but it seems really cool. Encoding in data types the laws something must follow is really neat, especially when the types become so “tight” the answer must pop right out (as I think is done with the arities and signatures for FreeCartesian.

@olf

F (a :: Type) (n :: Arity)

With the above, it is described as a functor; could we make it into a proper haskell function by just swapping n and a?

I’d personally appreciate further elaboration here if that’s possible.

Thought that just popped into my head; how possible would it be to TH’ify the laws and proof for this sort of thing and then have compile time verification that the laws are followed? Or is this construction not powerful enough for that kind of “proof”, and it’s merely just setting up for quickchecking (which we certainly shouldn’t do at compile time).

[olf]

@L0neGamer

With the above, it is described as a functor; could we make it into a proper haskell function by just swapping n and a?

Notice that F a has kind Arity -> Type so it definitely can not be a Functor in the strict Haskell Prelude sense. When swapping the arguments, it is nothing but a vector functor of statically known dimension, e.g.

newtype V2 a = V2 (F a Two)

For the functoriality of F a, I did write that objects of Arity are to be thought of as natural numbers, but did not say what the morphisms are. The n-Category Cafe describes it as “the opposite of a skeleton of the category of finite sets”. Hence my use of Pair for what at first glance appears to be a coproduct. (2 is not equal to 1 * 1 but to 1 + 1)

@L0neGamer

Or is this construction not powerful enough for that kind of “proof”, and it’s merely just setting up for quickchecking

I did not intend this to be accessible to proof-checking, just wanted to convey the original idea of Lawvere theory as direct as possible. In any case, what would a “proof” of the laws be? It would, for any particular model of the theory, require knowledge of the particular implementation of model, which would have to be encoded somehow in a form so that a proof checker can analyze it.

There is another technique for algebraic categories, called “generators and relations”. It says that every object of the category is a quotient of a free object over some generators, by relations that honour the algebraic structure, so-called congruence relations. I can imagine that is is easy to prove that a free construction is lawful, thereby shifting the proof burden towards proving that the relations form a congruence. Sadly, relations are hard to work with in computing, due to the existential quantification in the relational composition.

[olf]

Yes, having a Signature x -> x as operations is definitely easier to work with, and extending signatures and laws in a tower of varieties evidently works, too.

In your Variety class, I can see why Requirements var x is a useful context for lawful. But I fail to see why the same constraint should be needed for the operations. Why would a Semigroup need to have an Eq instance?

The Variety class has a less tight coupling between the signature and the laws; they could be entirely unrelated types. In contrast, Lawvere takes the signature as part of the skeleton of the category the laws are written in.

[olf]

By the way, does the GHC type checker know the principle of induction? Say we have

data Peano = Zero | Succ Peano
class Prop (n :: Peano)

Now suppose I have implemented

instance Prop Zero
instance (Prop n) => Prop (Succ n)

Can I then use the universally quantified constraint

forall n. Prop n

in my contexts?

EDIT: With the help of the added argList function that is polymorphic in the Arity, we can define the desired universally quantified constraint, even if GHC does not know the principle of induction.

[ashokkimmel]

No, especially because

type Stuck :: Peano
type family Stuck where

This is an irreducible type family, but it’s still technically valid. It also is not an instance of Prop.

[mixphix]

I didn’t use type-level naturals, but I did use type-level lists with a FilterableWithIndex constraint in my deep-map library. A DeepMap is a recursive Map indexed by a list of types, with an agglomerating Semigroup instead of an overwriting one. In order to

filterWithKeys ::
  (FilterableWithIndex (Deep (k ': ks)) (DeepMap (k ': ks))) =>
  (Deep (k ': ks) -> v -> Bool) ->
  DeepMap (k ': ks) v ->
  DeepMap (k ': ks) v
filterWithKeys = Witherable.ifilter

for all maps with at least one key type (but possibly still empty as maps), I need the induction principle:

-- base case
instance FilterableWithIndex (Deep '[k]) (DeepMap '[k]) where
  imapMaybe f (Wrap m) = Wrap $ Map.mapMaybeWithKey (\k (Core v) -> Core <$> f (D1 k D0) v) m

-- recursive case
instance
  (Ord j, FilterableWithIndex (Deep (k ': ks)) (DeepMap (k ': ks))) =>
  FilterableWithIndex (Deep (j ': k ': ks)) (DeepMap (j ': k ': ks))
  where
  imapMaybe f (Wrap m) = Wrap $ Map.mapWithKey (\k -> Witherable.imapMaybe (f . D1 k)) m

It doesn’t avoid the need to add the constraint to the definition of filterWithKeys, but in practice it is trivially satisfied except for DeepMap '[] v, which was what we wanted.

Maybe a similar thing with unary representations could work?

[mixphix]

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!

[olf]

@ashokkimmel

type Stuck :: Peano
type family Stuck where

This is an irreducible type family, but it’s still technically valid. It also is not an instance of Prop.

Interesting. Is that the type-level equivalent to a function declaration without a function body? Does the kind Peano also contain an infinity type like infinity = Succ infinity? Apparently under UndecidableInstances one can write such a type family. Your Stuck example is more unnerving, though, because it does not require an obviously dangerous language extension. Thanks for showing it!

[olf]

@mixphix

The laws aren’t always so tightly coupled to the signature

What I meant by coupled is: Just by looking at the constructors of EqLaw alone one can not learn how many operations there are in Eq and what their aritites are. You need to look at how the constructors are used in lawful.
Yet I agree that Lawvere’s way is far too complicated to be practically useful for Haskell type class hierarchies. I actually do not know whether Lawvere came up with this just for descriptive purposes or whether something genuinely new arose out of it.

[ashokkimmel]

While you can write the Infinity with undecidable instances, I’m pretty sure that using it anywhere in your code will throw the type checker into an infinite loop. One comment I recall, which showed how data families can be used to the same effect as my Stuck said

That’s a good reminder that pattern matching on types is never total.

Sorry, I’m on my phone so this comment might be a bit unreadable.