# Sneak Peek: Bolt Math

**URL:** <https://discourse.haskell.org/t/sneak-peek-bolt-math/13766>\
**Category:** Announcements\
**Created:** [March 6, 2026, 7:29pm UTC](https://discourse.haskell.org/t/sneak-peek-bolt-math/13766 "2026-03-06T19:29:05Z")\
**Posts on this page:** 1\
**Showing post:** 24

<div class="post-metadata">

**Author:** ![ApothecaLabs](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/apothecalabs/32/3215_2.png) [@ApothecaLabs](https://discourse.haskell.org/u/ApothecaLabs)\
**Post date:** [March 21, 2026, 3:00am UTC](https://discourse.haskell.org/t/sneak-peek-bolt-math/13766/24 "2026-03-21T03:00:20Z")

</div>

# Math Update: Semigroup, and the Cooler Semigroup

So, I have been paying close attention to feedback, and I thought I would address one of the concerns that is on many people’s minds - lawfulness. I have a ton more coming down the pipeline (topological spaces, manifolds, discrete spaces, projective and conformal geometry - fun stuff) but they need a solid foundation, and I’m still nailing down some design points, so today…

\*SNAP\*

 ![mr-curry-i-dont-feel-so-goodan6gae](https://us1.discourse-cdn.com/flex002/uploads/haskell/original/2X/1/1c569cf6ceb16d8fa759ee1f1de396ac8b98fe07.jpeg)

> _I dont know why I am using avengers infinity war memes, I haven’t even seen the movies._

Another thing that bothers me about Haskell, supposedly one of the best languages, is that we cannot define laws for typeclasses, and as a result, comments and documentation are littered with `-- INVARIANT: blah blah blah`, meaning you have to scan the documentation to even know about this invisible constraint that the compiler can’t warn you against. I hate that - don’t you?

Things like LiquidHaskell exist, but they tend to be plugins that define a new layer eg centered over parsing comments, and while that’s pretty darn cool, I just really like sticking with Haskell. Can’t we do better?

# Algebra: It’s the law!

This isn’t my first attempt at codifying algebraic laws into Haskell, but it is so far, my most successful. I have made previous attempts some years back, only those were simple, and limited to demonstrating magmas associativity and semigroups - I never really got any further with it, not because it didn’t work (it did), but because it didn’t really do or add anything, since it was too limited to even describe equality.

That has changed.

# Operations

We will start with a generalization of the heterogenous operators:

```haskell
class Operation (r :: Type -> Type -> Constraint) a b where
    type Result r a b :: Type
    op :: a -> b -> Result r a b

```

The `r` constraint allows us to specify the typeclass that defines the operation, eg:

```haskell
instance Operation Addition Int Int where
    type Result Addition Int Int = Int
    op = plus

```

We use this via `op @Addition @Int @Int 1 2`, and by doing so, we have promoted our typeclass to a first-class type. A little verbose, but we’ll deal with that by sealing it up later as a magma.

# Actions

Operations are really generic, actions are more restricted - one of the arguments is the same type as the result, so either `a -> b -> b`, or `a -> b -> a`:

```haskell
class (Operation r a b, Result r a b ~ b) => LeftAction r a b where
    lact :: a -> b -> b
    lact = op @r

class (Operation r a b, Result r a b ~ a) => RightAction r a b where
    actr :: a -> b -> a
    actr = op @r

```

These functions cover operations that perform some action over an object without changing its type. Using it is as simple as `lact @Multiplication @Float @(Vector Float)`.

# Relations / Pairings

As mentioned by in a few comments, operations of the form `a -> a -> b` are a ‘pairing’ but I think the most accurate term here is ‘relation’ as in, an open homogenous relationship.

```haskell
type Codomain r a = Result r a a
class (Operation r a a) => Relation r a where
    rel :: a -> a -> Codomain r a
    rel = op @r

```

We also defined `Codomain` - neat!

# Laws

Now comes the part where things start getting… legal. See, the standard way to go about enforcing constraints on classes is to add functions that add new capabilities or requirements. This has caused me some consternation, because it doesn’t scale well (typeclass explosions) and it can be hard to enforce the non-existence of a thing, and you end up with a bunch of empty typeclasses like [algebraic-graphs](https://hackage-content.haskell.org/package/algebraic-graphs-0.8/docs/Algebra-Graph-Class.html):

```haskell
class Graph g => Undirected g
    -- Empty class
class Graph g => Reflexive g
    -- Empty class
class Graph g => Transitive g
    -- Empty class
class (Reflexive g, Transitive g) => Preorder g
    -- Empty class

```

It’s great that you can express that a constraint follows a law - its not so great that these classes are all useless outside of the algebraic-graphs typeclass hierarchy. They’re also completely empty, and amount to nothing more than swearsy-realsy promises - and ultimately, I don’t think it’s quite the right approach - and I hope you’ll follow along, and come to see the same.

Instead of defining a typeclass that says “this class _has legal behavior_”, we just define a typeclass that says it _can_ follow laws:

```haskell
class (Operation r a b) => Lawful r a b where
    lawful :: a -> b -> Bool

```

Specifically, this class doesn’t assert that it _is_ lawful in general, but rather, that we can check whether a particular operation is lawful. This is meaningful, because there can be valid inputs that break the law, which is not exactly the same thing as an invalid input that throws an error and breaks the computer - though that certainly is one possible outcome of failing to adhere to a law.

As a result, this class sort of pre-generalizes several things:

- Throwing catchable exceptions
- Throwing fatal errors
- Returning exceptional values (Maybe, Either Error)
- Interrupt and recovery

We can use it via `lawful @Division @Int @Int 1 0` which yields `False`, allowing us to perform lawfulness checks before attempting the operation.

Adding to this is a typeclass for specific laws:

```haskell
class (Lawful r a b) => Law p r a b where
    is :: a -> b -> Bool
    isnt :: a -> b -> Bool

```

We can use this via `is @Open @Division` or even `is @Lawful @Division` - that second one is actually ratherm important, because `Lawful` itself _is a law_ that checks whether an operation follows _all_ laws:

```haskell
instance (Lawful r a b) => Law Lawful r a b where
    is = lawful @r
    isnt a b = not (lawful @r a b)

```

So, how do we actually specify that an operation does in fact always follow all laws? Why, we use the mathematical definition:

```haskell
class (Lawful r a b) => WellDefined r a b where
    type Definition r a b :: Type
    definition :: Definition r a b
    -- lawful always returns true for well-defined relations
    defined :: a -> b -> Bool
    defined _ _ = True

```

I decided to tack on the ability to retrieve a definition, too. Something tells me that will be handy in the future.

In a neat bit of symmetry, we can also define indeterminate forms, and distinguish between functions that have undefined results, and functions that have more than one result:

```haskell
class (Lawful r a b) => Indeterminate r a b where
    type IndeterminateForm r a b :: Type -- 0, 1, or many possible results
    indeterminate :: a -> b -> Bool
    indeterminateForm :: a -> b -> IndeterminateForm r a b

data Undefined -- Eg, Void

class (Indeterminate r a b, IndeterminateForm r a b ~ Undefined) => Indefinite r a b where
    indefinite :: a -> b -> Bool
    indefinite = indeterminate @r

```

Note that we don’t give instances to _specific types_, we give instances to constraints - so that means we can’t really define laws without defining properties to apply them, AND defining the data type they operate over. That’s a bit tedious, and its mostly just a bit of repetative boilerplate like when I defined `instance Addition Int Int`, so you’ll have to use your imagination.

# Groupoids

Okay, so let’s define some properties / laws:

```haskell
class (Relation r a) => Open r a where
    open :: a -> a -> Bool

class (Open r a, Codomain r a ~ a) => Closed r a where
    closed :: a -> a -> Bool

class
    ( Operation r a b -- Result r a b ~ d
    , Operation r b c -- Result r b c ~ e
    , Operation r a (Result r b c) -- Operation r a e
    , Operation r (Result r a b) c -- Operation r d c
    , Result r (Result r a b) c ~ Result r a (Result r b c) -- Result r d c ~ Result r a e
    ) => Associative r a b c where
    associative :: a -> b -> c -> Bool
    default associative :: (Eq (Result r a (Result r b c))) => a -> b -> c -> Bool
    associative a b c = op @r (op @r a b) c == op @r a (op @r b c)

class
    ( Operation r a b
    , Operation r b a
    , Result r a b ~ Result r b a
    ) => Commutative r a b where
    commutative :: a -> b -> Bool
    default commutative :: (Eq (Result r a b)) => a -> b -> Bool
    commutative a b = op @r a b == op @r b a

class (Relation r a) => Unital r a where
    identity :: a

class (Relation r a) => Invertible r a where
    inverse :: a -> a

```

Oof! Defining heterogenous associativity and commutativity was a pain in the arse - but well worth it, because now these get used to define our magma typeclasses:

```haskell
class (LeftAction r a a, RightAction r a a, Relation r a, Closed r a) => Magma r a where
    act :: a -> a -> a
    act = rel @r

class (Magma r a, Associative r a a a) => Semigroup r a where
    append :: a -> a -> a
    append = act @r

class (Semigroup r a, Unital r a) => Monoid r a where
    empty :: a
    empty = identity @r

class (Monoid r a, Invertible r a) => Group r a where

```

Big group hug, everyone! No longer do we have to hem and haw about which instance of `Monoid` is the most important and which get relegated to newtype wrappers - now multiple instances (eg, of Semigroup, Monoid, etc) can coexist simultaneously, and can be easily selected between!

Now, we could make also law instances, given an actual operation data type - `instance Law Closed Addition Int Int`, `instance Law Associative Addition Int Int` etc so long as we also have `instance Closed Addition Int Int` and `instance Associative Int Int`.

But I’ve got something else for closing:

# Functions

Lets generalize `Operation` to support arbitrary arity.

First, we need a function typeclass:

```haskell
type family Call (args :: [Type]) out :: Type where
    Call '[] out = out
    Call (a ': args) out = a -> Call args out

class Function r (arity :: Nat) (args :: [Type]) | r -> arity args where
    type Return r arity args :: Type
    call :: Call args (Return r arity args)

```

Fundeps AND type families, oh my - the type families avoid parameter explosions while fundeps enforce injectivity without requiring intervening constructors like data families would have.

All this does though is curry a type-level list of arguments into a proper lambda, though - but now we can describe imperative functions more correctly.

Defining unary and binary operations takes a little bit of thought, but is ultimately just forwarding arguments.

```haskell
class (Function r 1 '[a], Return r 1 '[a] ~ Output r a) => UnaryOperation (r :: Type -> Constraint) a where
    type Output r a :: Type
    unop :: a -> Output r a
    unop = call @r @1 @'[a]

class (Function r 2 '[a, b], Return r 2 '[a, b] ~ Result r a b) => Operation (r :: Type -> Type -> Constraint) a b where
    type Result r a b :: Type
    op :: a -> b -> Result r a b

```

What’s neat is that since this is all occurring at the type level, so all of this gets elided by the compiler, hopefully giving it zero runtime cost - but how can we know this?

Lets define a function:

```haskell
data Honk
instance Function Honk 1 '[Int] where
    type Return Honk 1 '[Int] = IO ()
    -- NOTE: The awkward syntax / lack of inference can be elided with an
    -- appropriate use of let- or where- clauses
    call :: Call '[Int] (Return Honk 1 '[Int])
    call = go where
        go 0 = return ()
        go n = print "Honk!" >> go (n - 1)

```

Note that `Honk` has no values, so it disappears entirely during compilation and `call @Honk` just collapses directly to the `go` function.

Finally, to test it out:

```ghci
> honk = call @Honk
> honk 3
Honk!
Honk!
Honk!

```

Silly goose, functions types are for people!

# Conclusion

I know that the plethora of type annotations are going to some worries, so I will head those off with a reminder - you are looking at the exposed seedy underbelly of the machine, we will cover it with elegance and ergonomics when we are satisfied that _it is correct_.

We are giving up a lot of type inference, but what we get in return is an effortless scaling of typeclasses, so this is best understood as targeting the machinery that powers the guts and runtime. Imagine how this integrates with the `memalloc` library that is being developed, or with writing interpreters with first-class access to Haskell functions, because after `Function` comes `Method` and `Object`, by opening a way to allow for function definitions to become first-class ‘Typed functions’ (Data functions?), like how data types can be first class via `Generic`.

* * *

Challenges for the studious reader

- Define the equivalent of `Reader` using `Function`
- Define the equivalent of `Lambda a b` using `Function`.
- How do these two differ? How are they related?
- Did you spot the Church encoding?

---

_[View the full topic](https://discourse.haskell.org/t/sneak-peek-bolt-math/13766)._