an epic journey through monoids
mono+oid means one … oid. or maybe “one noid”?TODO:
- compile this
- show large graph of algebraic structures, then zoom in to monoid
- monoid is kind of the powerhouse – massive strength to weight ratio, very common, not too complex, but has enough laws to be interesting.
Greg Pfeil
(right here)
Hiring Scala & Haskell devs (and many other roles) – if you find anything in this talk intriguing, you should talk to me about applying. Don’t let this talk dissuade you at all, though – understanding this is by no means a prerequisite for any position we have. (But my co-workers have certainly helped me work through some of these ideas).- this talk – https://github.com/sellout/category-parametric-talk/monoiad/
- Caterwaul – https://github.com/sellout/caterwaul
- Cheshire – https://github.com/sellout/cheshire
name: monoiad
version: 0.1.0.0
build-type: Simple
cabal-version: >=1.10
library
exposed-modules: Monoiad
, Monoiad.Isomorphic
, Monoiad.Category
, Monoiad.Instances.Add, Monoiad.Instances.Cartesian, Monoiad.Instances.CatCartesian, Monoiad.Instances.CatCocartesian, Monoiad.Instances.Cocartesian, Monoiad.Instances.Conjunction, Monoiad.Instances.Disjunction, Monoiad.Instances.First, Monoiad.Instances.Last, Monoiad.Instances.Max, Monoiad.Instances.Min, Monoiad.Instances.Multiply
default-extensions: AllowAmbiguousTypes, ConstraintKinds
, ExistentialQuantification, FlexibleContexts
, FlexibleInstances, InstanceSigs
, LambdaCase, MultiParamTypeClasses
, PolyKinds, RankNTypes
, TypeFamilies, TypeOperators
, UndecidableInstances
build-depends: base >=4.10 && <4.11, text
default-language: Haskell2010
module Monoiad where
import Prelude hiding (Category(..), Monoid(..), product)
monoid: a category with a single object
-ad: an epic poem, usually with a cyclical journey of discovery
monad: a monoid in the category of endofunctors
let nums = [8, 2, 4, 5, -2, 8, 3]
in fold nums
⇒ -2
⇒ 8
⇒ 28
⇒ -15360
foldr min maxBound nums
foldr max minBound nums
foldr (+) 0 nums
foldr (*) 1 nums
class Monoid a where
product :: a -> a -> a
unit :: a
class Monoid a where
product :: a -> a -> a
unit :: a
associativity :: (Eq a, Monoid a) => a -> a -> a -> Bool
associativity x y z =
product (product x y) z == product x (product y z)
leftIdentity :: (Eq a, Monoid a) => a -> Bool
leftIdentity x = product unit x == x
rightIdentity :: (Eq a, Monoid a) => a -> Bool
rightIdentity x = product x unit == x
fold :: Monoid a => [a] -> a
fold = foldr product unit
Ok, that’s everything. You totally get monoids now. Thanks for coming.
module Monoiad.Instances.Conjunction where
import Monoiad
import Prelude hiding (Monoid(..), product)
instance Monoid Bool where
product = (&&)
unit = True
-- True && (False && True) == False == (True && False) && True
-- False && True == False == True && False
module Monoiad.Instances.Disjunction where
import Monoiad
import Prelude hiding (Monoid(..), product)
instance Monoid Bool where
product = (||)
unit = False
-- True || (False || True) == True == (True || False) || True
-- True || False == True == False || True
module Monoiad.Instances.Add where
import Monoiad
import Prelude hiding (Monoid(..), product)
instance Monoid Int where
product = (+)
unit = 0
-- 4 + (2 + 3) == 9 == (4 + 2) + 3
-- 7 + 0 == 7 == 0 + 7
module Monoiad.Instances.Multiply where
import Monoiad
import Prelude hiding (Monoid(..), product)
instance Monoid Int where
product = (*)
unit = 1
-- 4 * (2 * 3) == 24 == (4 * 2) * 3
-- 7 * 1 == 7 == 1 * 7
module Monoiad.Instances.Max where
import Monoiad
import Prelude hiding (Monoid(..), product)
instance Monoid Int where
product = max
unit = minBound
-- max 12 (max 7 32) == 32 == max (max 12 7) 32
-- max 26 minBound == 26 == max minBound 26
module Monoiad.Instances.Min where
import Monoiad
import Prelude hiding (Monoid(..), product)
instance Monoid Int where
product = min
unit = maxBound
-- min 12 (min 7 32) == 7 == min (min 12 7) 32
-- min 26 maxBound == 26 == min maxBound 26
instance Monoid [Char] where
product = (++)
unit = ""
-- "mon" ++ ("oi" ++ "ad") == "monoiad" == ("mon" ++ "oi") ++ "ad"
-- "foo" ++ "" == "foo" == "" ++ "foo"
- concepts that transcend languages
- monoids are at a “sweet spot”
- concurrency
trait
I put up before, but let’s take a step back.
A ⊗ A → A η → A
∀x, y, z ∈ A (x ⊗ y) ⊗ z ≅ x ⊗ (y ⊗ z) η ⊗ x ≅ x ≅ x ⊗ η
(a, ⊗, μ)
This definition is a bit more abstract, and so maybe it can help us think of cases that aren’t quite instances of that type class.
And we weaken the equality of our laws to isomorphism. And what is isomorphism?
module Monoiad.Isomorphic where
import Data.Text
import Data.Void
import Prelude hiding (Monoid(..), product)
data Iso arr a b =
Isomorphism { apply :: arr a b, unapply :: arr b a }
textToString :: Iso (->) Text String
textToString = Isomorphism unpack pack
"monoiad" /= ['m', 'o', 'n', 'o', 'i', 'a', 'd']
class Monoid a where
product :: a -> a -> a
unit :: a
associativity :: (Eq a, Monoid a) => a -> a -> a -> Bool
associativity x y z =
product (product x y) z == product x (product y z)
leftIdentity :: (Eq a, Monoid a) => a -> Bool
leftIdentity x = product unit x == x
leftIdentity :: (Eq a, Monoid a) => a -> Bool
leftIdentity x = product x unit == x
class TMonoid (arr :: k -> k -> *) where
type Product arr :: k -> k -> k
type Unit arr :: k
class TMonoid (arr :: k -> k -> *) where
type Product arr :: k -> k -> k
type Unit arr :: k
associativity :: Iso arr (Product arr (Product arr a b) c)
(Product arr a (Product arr b c))
leftIdentity :: Iso arr (Product arr (Unit arr) x) x
rightIdentity :: Iso arr (Product arr x (Unit arr)) x
module Monoiad.Instances.Cartesian where
import Monoiad.Isomorphic
import Prelude hiding (Monoid(..), product)
instance TMonoid (->) where
type Product (->) = (,)
type Unit (->) = ()
associativity :: Iso (->) ((a, b), c) (a, (b, c))
associativity = Isomorphism undefined undefined
leftIdentity :: Iso (->) ((), a) a
leftIdentity = Isomorphism snd ((,) ())
rightIdentity :: Iso (->) (a, ()) a
rightIdentity = Isomorphism fst (flip (,) ())
module Monoiad.Instances.Cocartesian where
import Data.Void
import Monoiad.Isomorphic
import Prelude hiding (Monoid(..), product)
instance TMonoid (->) where
type Product (->) = Either
type Unit (->) = Void
associativity :: Iso (->) (Either (Either a b) c)
(Either a (Either b c))
associativity = Isomorphism undefined undefined
leftIdentity :: Iso (->) (Either Void a) a
leftIdentity = Isomorphism (either absurd id) Right
rightIdentity :: Iso (->) (Either a Void) a
rightIdentity = Isomorphism (either id absurd) Left
module Monoiad.Category where
import Data.Functor.Compose
import Data.Functor.Identity
import Data.Void
import Monoiad.Isomorphic hiding (Monoid(..))
import Prelude hiding (Monad(..), Monoid(..), product)
class Category arr where
compose :: arr b c -> arr a b -> arr a c
identity :: arr a a
instance Category (->) where
compose :: (b -> c) -> (a -> b) -> (a -> c)
compose f g = \x -> f (g x)
identity :: a -> a
identity = \x -> x
(stolen from Emily Riehl’s Category Theory in Context)
Let’s take a step back to (*, Tuple2, Unit) and our original type class definition:class Monoid a where
product :: a -> a -> a
unit :: a
class Monoid a where
product :: a -> a -> a
unit :: () -> a
class Monoid a where
product :: (a, a) -> a
unit :: () -> a
class Monoid a where
product :: (a, a) -> a
unit :: () -> a
instance TMonoid (->) where
type Product (->) = (,)
type Unit (->) = ()
The argument to each function is respectively the Product
and Unit
of our type-level Cartesian
instance.
So, we can make that explicit …
class TMonoid arr => Monoid arr a where
product :: arr (Product arr a a) a
unit :: arr (Unit arr) a
instance Monoid (->) Bool where
product p = fst p && snd p
unit _ = True
instance Monoid (->) a where
product :: Either a a -> a
product = either id id
unit :: Void -> a
unit = absurd
class Category arr where
compose :: arr b c -> arr a b -> arr a c
identity :: arr a a
type MonoidalCategory arr = (TMonoid arr, Category arr)
class MonoidalCategory arr => Monoid arr a where
product :: arr (Product arr a a) a
unit :: arr (Unit arr) a
module Monoiad.Instances.CatCartesian where
import Monoiad.Category
import Monoiad.Instances.Cartesian
import Prelude hiding (Monoid(..), product)
instance Monoid (->) Bool where
product p = fst p && snd p
unit _ = True
module Monoiad.Instances.CatCocartesian where
import Data.Void
import Monoiad.Category
import Monoiad.Instances.Cocartesian
import Prelude hiding (Monoid(..), product)
instance Monoid (->) a where
product = either id id
unit :: Void -> a
unit = absurd
newtype Op arr a b = Op { unOp :: arr b a }
instance Category arr => Category (Op arr) where
compose f g = Op (compose (unOp g) (unOp f))
identity = Op identity
instance TMonoid arr => TMonoid (Op arr) where
type Product (Op arr) = Product arr
type Unit (Op arr) = Unit arr
associativity = Isomorphism (Op (unapply associativity))
(Op (apply associativity))
leftIdentity = Isomorphism (Op (unapply leftIdentity))
(Op (apply leftIdentity))
rightIdentity = Isomorphism (Op (unapply rightIdentity))
(Op (apply rightIdentity))
instance Monoid (Op (->)) a where
-- :: a -> (a, a)
product = Op (\x -> (x, x))
-- :: a -> ()
unit = Op (const ())
- ([*] → *, cats.data.Compose, cats.Identity)
Compose[F[_], G[_], A] ≅ F[G[A]] Identity[A] ≅ A
Compose[Compose[List, Set, ?], Maybe, ?] ≅ Compose[List, Compose[Set, Maybe, ?], ?] // ≅ List[Set[Maybe[A]]] Compose[Identity, List, ?] ≅ List ≅ Compose[List, Identity, ?]
This has been happening behind the scenes mostly so far, but we’ll discuss it now as we start to use it in earnest.
{-# language PolyKinds #-}
TMonoid
a few times to understand the parallel.
data (f :: * -> *) ~> (g :: * -> *) =
NT { unNT :: forall a. f a -> g a }
instance TMonoid (~>) where
type Product (~>) = Compose
type Unit (~>) = Identity
-- Compose (Compose f g) h ≅ Compose f (Compose g h)
associativity = Isomorphism undefined undefined
-- Compose Identity F ≅ F ≅ Compose F Identity
leftIdentity = Isomorphism (NT (runIdentity . getCompose))
(NT (Compose . Identity))
rightIdentity = Isomorphism undefined undefined
“a monad is a monoid in the category of endofunctors”
type Monad m = (Functor m, Monoid (~>) m)
-- product :: forall a. Compose m m a -> m a -- join
-- unit :: forall a. Identity a -> m a -- return
mjoin :: Monad m => m (m a) -> m a
mjoin = unNT product . Compose
return :: Monad m => a -> m a
return = unNT unit . Identity
(>>=) :: Monad m => m a -> (a -> m b) -> m b
ma >>= f = mjoin (fmap f ma)
MonoidF
to Monad
, and then show how flatMap
can be implemented … and explain why we get map
“for free”.
They’re easy to create out of thin air.
module Monoiad.Instances.First where
import Monoiad.Category
import Monoiad.Instances.Cartesian
import Prelude hiding (Monoid(..), product)
instance Eq a => Monoid (->) a where
product (x, y) = if x == unit () then y else x
unit = undefined -- any value of type `a`
module Monoiad.Instances.Last where
import Monoiad.Category
import Monoiad.Instances.Cartesian
import Prelude hiding (Monoid(..), product)
instance Eq a => Monoid (->) a where
product (x, y) = if y == unit () then x else y
unit = undefined -- any value of type `a`
foldRight
.
digraph "" {
rankdir=BT
bgcolor=transparent
Monoid [style=bold]
Semigroup -> magma
quasigroup -> magma [color=orange]
loop -> quasigroup [color=red]
CommutativeSemigroup -> Semigroup [color=blue]
Monoid -> Semigroup [color=red]
Band -> Semigroup [color=purple]
CommutativeMonoid -> CommutativeSemigroup [color=red]
CommutativeMonoid -> Monoid [color=blue]
Semilattice -> CommutativeSemigroup [color=purple]
Semilattice -> Band [color=blue]
Group -> Monoid [color=orange]
Group -> loop
CommutativeGroup -> Group [color=blue]
CommutativeGroup -> CommutativeMonoid [color=orange]
BoundedSemilattice -> Semilattice [color=red]
BoundedSemilattice -> CommutativeMonoid [color=purple]
}
- associativity – black
- identity – red
- commutativity –
+
,*
,max
(but not String concatenation) – blue - idempotency –
max
,mix
(but not+
,*
) – purple - invertible –
+
for ℤ (but not for ℕ) – orange
- Monad (kind polymorphism)
- Alternative (quantified constraints)
- Comonoid
newtype Additive arr a b = Add { sum :: arr a b }
newtype Multiplicative arr a b = Multiply { prod :: arr a b }
class (TMonoid (Additive arr), TMonoid (Multiplicative arr)) => TRig arr where
type Add arr a b
type Add arr a b = Product (Additive arr) a b
type Zero arr
type Zero arr = Unit (Additive arr)
type Multiply arr a b
type Multiply arr a b = Product (Multiplicative arr) a b
type One arr
type One arr = Unit (Multiplicative arr)
distribute
:: Iso arr (Multiply arr a (Add arr b c))
(Add arr (Multiply arr a b) (Multiply arr a c))
leftAnnihilate :: Iso arr (Multiply arr (Zero arr) a) (Zero arr)
rightAnnihilate :: Iso arr (Multiply arr a (Zero arr)) (Zero arr)
type RigCategory arr = (TRig arr, Category arr)
instance TMonoid (Additive (->)) where
type Product (Additive (->)) = Either
type Unit (Additive (->)) = Void
associativity = Isomorphism undefined undefined
leftIdentity = Isomorphism (Add (either absurd id)) (Add Right)
rightIdentity = Isomorphism (Add (either id absurd)) (Add Left)
instance TMonoid (Multiplicative (->)) where
type Product (Multiplicative (->)) = (,)
type Unit (Multiplicative (->)) = ()
associativity = Isomorphism undefined undefined
leftIdentity = Isomorphism (Multiply snd) (Multiply ((,) ()))
rightIdentity =
Isomorphism (Multiply fst) (Multiply (flip (,) ()))
instance TRig (->) where
distribute :: Iso (->) (a, Either b c) (Either (a, b) (a, c))
distribute = Isomorphism
(\case
(a, Left b) -> Left (a, b)
(a, Right c) -> Right (a, c))
(\case
Left (a, b) -> (a, Left b)
Right (a, c) -> (a, Right c))
leftAnnihilate :: Iso (->) (Void, a) Void
leftAnnihilate = Isomorphism fst absurd
rightAnnihilate :: Iso (->) (a, Void) Void
rightAnnihilate = Isomorphism snd absurd
newtype Meet a = Meet { meet' :: a }
newtype Join a = Join { join' :: a }
class ( MonoidalCategory arr
, Monoid arr (Meet l), Monoid arr (Join l)
) => BoundedLattice arr l where
meet :: arr (Product k l l) l
minimum :: arr (Unit k) l
join :: arr (Product k l l) l
maximum :: arr (Unit k) l
newtype Diamond arr a b = Diamond { diamond :: arr a b }
newtype Star arr a b = Star { star :: arr a b }
class (TMonoid (Diamond arr), TMonoid (Star arr)) => TDuoid arr where
type ProductD arr :: k -> k -> k
type ProductD arr = Product (Diamond arr)
type UnitD arr :: k
type UnitD arr = Unit (Diamond arr)
type ProductS arr :: k -> k -> k
type ProductS arr = Product (Star arr)
type UnitS arr :: k
type UnitS arr = Unit (Star arr)
swap :: arr (ProductD arr (ProductS arr a b) (ProductS arr c d))
(ProductS arr (ProductD arr a c) (ProductD arr b d))
split :: arr (UnitD arr) (ProductS arr (UnitD arr) (UnitD arr))
merge :: arr (ProductD arr (UnitS arr) (UnitS arr)) (UnitS arr)
switch :: arr (UnitD arr) (UnitS arr)
data Day f g c = forall a b. Day (a -> b -> c) (f a) (g b)
-- liftA2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c
instance TMonoid (Diamond (~>)) where
type Product (Diamond (~>)) = Day
type Unit (Diamond (~>)) = (->) ()
associativity = Isomorphism undefined undefined
leftIdentity = Isomorphism undefined undefined
rightIdentity = Isomorphism undefined undefined
instance TMonoid (Star (~>)) where
type Product (Star (~>)) = Compose
type Unit (Star (~>)) = Identity
associativity = undefined undefined
leftIdentity = Isomorphism undefined undefined
rightIdentity = Isomorphism undefined undefined
instance TDuoid (~>) where
swap :: Day (Compose f g) (Compose h i)
~> Compose (Day f h) (Day g i)
swap = undefined
split :: (->) () ~> Compose ((->) ()) ((->) ())
split = undefined
merge :: Day Identity Identity ~> Identity
merge = undefined
switch :: (->) () ~> Identity
switch = NT (\f -> Identity (f ()))
- parallel & sequential applicative instances
overlay
&connect
algebraic graph operations
- bimonoids
- meadow
- tropical semiring
- boolean algebra(?)
class Category arr where
compose :: arr b c -> arr a b -> arr a c
identity :: arr a a
class Category arr where
compose :: arr b c -> arr a b -> arr a c
identity :: arr a a
class Monoid a where
product :: a -> a -> a
unit :: a
class Category arr where
compose :: forall a b. (forall z. (arr z b, arr a z)) -> arr a b
identity :: arr a a
class Monoid a where
product :: (a, a) -> a
unit :: a
- a monoid is some closed associative operation with an identity
- monoids show up everywhere (and way too often)
- we can best understand “important” monoids in terms of
- what additional properties they have
- how they relate to other monoids
- monoids are often hidden behind other interpretations
- Nathan Faubion for the typo that led to the name/structure of this talk.
- Andrey Mokhov – https://blogs.ncl.ac.uk/andreymokhov/united-monoids/
- many others for feedback on this talk, as well as helping me learn all this in the first place
- this talk – https://github.com/sellout/category-parametric-talk/monoiad/
- Caterwaul – https://github.com/sellout/caterwaul
- Cheshire – https://github.com/sellout/cheshire
- Seven Sketches in Compositionality
- Category Theory in Context – https://golem.ph.utexas.edu/category/2016/11/category_theory_in_context.html
- nLab – https://ncatlab.org/nlab