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*
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:
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:
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:
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.
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:
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:
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:
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:
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:
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:
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:
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:
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:
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.
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:
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:
> 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
ReaderusingFunction - Define the equivalent of
Lambda a busingFunction. - How do these two differ? How are they related?
- Did you spot the Church encoding?