Sneak Peek: Bolt Math

Do you know about Lawvere theories? The unifying approach to laws there is to have a signature associated with a class of algebraic objects. In Haskell, we could hide the arity of the signature in a type family. Roughly speaking,

class Lawvere (theory :: Type -> Constraint) where
   type Signature theory :: Type -> Type
   operations :: theory a => Signature theory a -> a
   type Laws theory :: Type -> Type
   lawful :: (theory a, Eq a) => Laws theory a -> Bool

data MonoidLaws a where
   NeutralLeft :: a -> MonoidLaws a
   NeutralRight :: a -> MonoidLaws a
   Assoc :: a -> a -> a -> MonoidLaws a
lawfulMonoid :: (Monoid a, Eq a) => MonoidLaws a -> Bool
lawfulMonoid (NeutralLeft a) = a == mempty `mappend` a
lawfulMonoid (NeutralRight a) = a == a `mappend` mempty
lawfulMonoid (Assoc x y z) = mappend (mappend x y) z == mappend x (mappend y z)

instance Lawvere Monoid where
   type Signature Monoid a = Either () (a,a)
   operations (Left ()) = mempty
   operations (Right (x,y)) = mappend x y
   type Laws Monoid a = MonoidLaws a
   lawful = lawfulMonoid

ApothecaLabs:

Another problem that I’ve discovered in this design is an insufficient description / separation of properties vs the functions that define them

Lawvere combined the signature and laws in a single category L (objects = arities, morphisms = laws) and instances of the theory (models) are then functors from this category. Homomorphisms are natural transformations between such functors.

For the sake of efficiency, one could formulate the laws as Haskell rewrite rules.