{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiciknf65pbrd3r5asdvgjfpwvr7sl2yyd2srjhmrvij6s3o4dfpwu",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mhl4auwjnpc2"
  },
  "path": "/t/sneak-peek-bolt-math/13766?page=2#post_24",
  "publishedAt": "2026-03-21T03:00:20.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "algebraic-graphs",
    "@Addition",
    "@Int",
    "@r",
    "@Multiplication",
    "@Division",
    "@Open",
    "@Lawful",
    "@Honk"
  ],
  "textContent": "# Math Update: Semigroup, and the Cooler Semigroup\n\nSo, 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…\n\n*SNAP*\n\n> _I dont know why I am using avengers infinity war memes, I haven’t even seen the movies._\n\nAnother 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?\n\nThings 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?\n\n# Algebra: It’s the law!\n\nThis 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.\n\nThat has changed.\n\n# Operations\n\nWe will start with a generalization of the heterogenous operators:\n\n\n    class Operation (r :: Type -> Type -> Constraint) a b where\n        type Result r a b :: Type\n        op :: a -> b -> Result r a b\n\n\nThe `r` constraint allows us to specify the typeclass that defines the operation, eg:\n\n\n    instance Operation Addition Int Int where\n        type Result Addition Int Int = Int\n        op = plus\n\n\nWe 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.\n\n# Actions\n\nOperations 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`:\n\n\n    class (Operation r a b, Result r a b ~ b) => LeftAction r a b where\n        lact :: a -> b -> b\n        lact = op @r\n\n    class (Operation r a b, Result r a b ~ a) => RightAction r a b where\n        actr :: a -> b -> a\n        actr = op @r\n\n\nThese 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)`.\n\n# Relations / Pairings\n\nAs 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.\n\n\n    type Codomain r a = Result r a a\n    class (Operation r a a) => Relation r a where\n        rel :: a -> a -> Codomain r a\n        rel = op @r\n\n\nWe also defined `Codomain` - neat!\n\n# Laws\n\nNow 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:\n\n\n    class Graph g => Undirected g\n        -- Empty class\n    class Graph g => Reflexive g\n        -- Empty class\n    class Graph g => Transitive g\n        -- Empty class\n    class (Reflexive g, Transitive g) => Preorder g\n        -- Empty class\n\n\nIt’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.\n\nInstead of defining a typeclass that says “this class _has legal behavior_ ”, we just define a typeclass that says it _can_ follow laws:\n\n\n    class (Operation r a b) => Lawful r a b where\n        lawful :: a -> b -> Bool\n\n\nSpecifically, 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.\n\nAs a result, this class sort of pre-generalizes several things:\n\n  * Throwing catchable exceptions\n  * Throwing fatal errors\n  * Returning exceptional values (Maybe, Either Error)\n  * Interrupt and recovery\n\n\n\nWe can use it via `lawful @Division @Int @Int 1 0` which yields `False`, allowing us to perform lawfulness checks before attempting the operation.\n\nAdding to this is a typeclass for specific laws:\n\n\n    class (Lawful r a b) => Law p r a b where\n        is :: a -> b -> Bool\n        isnt :: a -> b -> Bool\n\n\nWe 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:\n\n\n    instance (Lawful r a b) => Law Lawful r a b where\n        is = lawful @r\n        isnt a b = not (lawful @r a b)\n\n\nSo, how do we actually specify that an operation does in fact always follow all laws? Why, we use the mathematical definition:\n\n\n    class (Lawful r a b) => WellDefined r a b where\n        type Definition r a b :: Type\n        definition :: Definition r a b\n        -- lawful always returns true for well-defined relations\n        defined :: a -> b -> Bool\n        defined _ _ = True\n\n\nI decided to tack on the ability to retrieve a definition, too. Something tells me that will be handy in the future.\n\nIn 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:\n\n\n    class (Lawful r a b) => Indeterminate r a b where\n        type IndeterminateForm r a b :: Type -- 0, 1, or many possible results\n        indeterminate :: a -> b -> Bool\n        indeterminateForm :: a -> b -> IndeterminateForm r a b\n\n    data Undefined -- Eg, Void\n\n    class (Indeterminate r a b, IndeterminateForm r a b ~ Undefined) => Indefinite r a b where\n        indefinite :: a -> b -> Bool\n        indefinite = indeterminate @r\n\n\nNote 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.\n\n# Groupoids\n\nOkay, so let’s define some properties / laws:\n\n\n    class (Relation r a) => Open r a where\n        open :: a -> a -> Bool\n\n    class (Open r a, Codomain r a ~ a) => Closed r a where\n        closed :: a -> a -> Bool\n\n    class\n        ( Operation r a b -- Result r a b ~ d\n        , Operation r b c -- Result r b c ~ e\n        , Operation r a (Result r b c) -- Operation r a e\n        , Operation r (Result r a b) c -- Operation r d c\n        , Result r (Result r a b) c ~ Result r a (Result r b c) -- Result r d c ~ Result r a e\n        ) => Associative r a b c where\n        associative :: a -> b -> c -> Bool\n        default associative :: (Eq (Result r a (Result r b c))) => a -> b -> c -> Bool\n        associative a b c = op @r (op @r a b) c == op @r a (op @r b c)\n\n    class\n        ( Operation r a b\n        , Operation r b a\n        , Result r a b ~ Result r b a\n        ) => Commutative r a b where\n        commutative :: a -> b -> Bool\n        default commutative :: (Eq (Result r a b)) => a -> b -> Bool\n        commutative a b = op @r a b == op @r b a\n\n    class (Relation r a) => Unital r a where\n        identity :: a\n\n    class (Relation r a) => Invertible r a where\n        inverse :: a -> a\n\n\nOof! 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:\n\n\n    class (LeftAction r a a, RightAction r a a, Relation r a, Closed r a) => Magma r a where\n        act :: a -> a -> a\n        act = rel @r\n\n    class (Magma r a, Associative r a a a) => Semigroup r a where\n        append :: a -> a -> a\n        append = act @r\n\n    class (Semigroup r a, Unital r a) => Monoid r a where\n        empty :: a\n        empty = identity @r\n\n    class (Monoid r a, Invertible r a) => Group r a where\n\n\nBig 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!\n\nNow, 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`.\n\nBut I’ve got something else for closing:\n\n# Functions\n\nLets generalize `Operation` to support arbitrary arity.\n\nFirst, we need a function typeclass:\n\n\n    type family Call (args :: [Type]) out :: Type where\n        Call '[] out = out\n        Call (a ': args) out = a -> Call args out\n\n    class Function r (arity :: Nat) (args :: [Type]) | r -> arity args where\n        type Return r arity args :: Type\n        call :: Call args (Return r arity args)\n\n\nFundeps AND type families, oh my - the type families avoid parameter explosions while fundeps enforce injectivity without requiring intervening constructors like data families would have.\n\nAll 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.\n\nDefining unary and binary operations takes a little bit of thought, but is ultimately just forwarding arguments.\n\n\n    class (Function r 1 '[a], Return r 1 '[a] ~ Output r a) => UnaryOperation (r :: Type -> Constraint) a where\n        type Output r a :: Type\n        unop :: a -> Output r a\n        unop = call @r @1 @'[a]\n\n    class (Function r 2 '[a, b], Return r 2 '[a, b] ~ Result r a b) => Operation (r :: Type -> Type -> Constraint) a b where\n        type Result r a b :: Type\n        op :: a -> b -> Result r a b\n\n\nWhat’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?\n\nLets define a function:\n\n\n    data Honk\n    instance Function Honk 1 '[Int] where\n        type Return Honk 1 '[Int] = IO ()\n        -- NOTE: The awkward syntax / lack of inference can be elided with an\n        -- appropriate use of let- or where- clauses\n        call :: Call '[Int] (Return Honk 1 '[Int])\n        call = go where\n            go 0 = return ()\n            go n = print \"Honk!\" >> go (n - 1)\n\n\nNote that `Honk` has no values, so it disappears entirely during compilation and `call @Honk` just collapses directly to the `go` function.\n\nFinally, to test it out:\n\n\n    > honk = call @Honk\n    > honk 3\n    Honk!\n    Honk!\n    Honk!\n\n\nSilly goose, functions types are for people!\n\n# Conclusion\n\nI 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_.\n\nWe 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`.\n\n* * *\n\nChallenges for the studious reader\n\n  * Define the equivalent of `Reader` using `Function`\n  * Define the equivalent of `Lambda a b` using `Function`.\n  * How do these two differ? How are they related?\n  * Did you spot the Church encoding?\n\n",
  "title": "Sneak Peek: Bolt Math"
}