From Category Theory for Programmers - Series 1

Category Theory 10.1 - Monads

• What is a function, or why use functions at all in programming?
• Allows decomposition and recomposition of a program
• Monad is similar
• Used to provide composition of Kleisli arrows
• Kleisli category in Haskell
• "Fish operator" >=> is the function with embellishment

(>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c)
-- | m is the embellishment
-- | m is a functor
 
-- | function f is a -> mb (these are types)
-- | function g is b -> mc 
f >=> g = λ a -> let m_b = f a
                in ...
-- | looking for a function like the following
:: m b -> (b -> m c) -> m c
-- | call it "bind"
(>>=) :: m b -> (b -> m c) -> m c
-- | then
f >=> g = λ a -> let m_b = f a
                in m_b >>= g
-- | Monad definition is
class Monad m where
    (>>=) :: m a -> (a -> m b) -> m b
    return :: a -> m a
 
-- | what can be used from the fact m is a functor (in bind)?
-- | need another function
join :: m (m a) -> m a
-- | then, where f is (a -> m b) from (>>=)
m_a >>= f = join (fmap f m_a)
class Functor m => Monad m where
    join :: m(m a) -> m a
    return :: a -> m a
-- | join is actually provided by the Haskell library

• What use is all of this?
• It turns out, things useful in imperative programming that are used in non-pure functions can be converted to pure functions with embellishment
• Monad is useful to split these pure functions then recompose them
• Partial functions (in programming) are not pure, might throw an exception or similar
• Example

 
-- | partial function
a -> b
-- | rewritten
a -> Maybe b
join :: Maybe (Maybe a) -> Maybe a
join (Just (Just a)) = Just a
-- | anything else, return nothing
join _ = Nothing
 
-- | alternative using bind
-- | where f is a -> Maybe b
Nothing >>= f = Nothing
Just a >>= f = f a
return a = Just a
 
-- | another example
-- | a function that depends on external state s
a -> b
-- | change to pass state with function
(a, s) -> (b, s)
-- | change to use currying
a -> (s -> (b, s))
newtype State s a = State (s -> (a, s))

• Category theory uses different names than Haskell
• m -> T
• join -> μ
• For category C:
• return -> η
• For category C:
• Return is a polymorphic function, really a natural transformation
• A monad is an endofunctor T, plus two natural transformations
• Id → T
• T ∘ T → T
• Where arrow is natural transformation
• And, some additional requirements
• Associative (for identity I)
• μ ∙ (μ ∘ I) = μ ∙ (I ∘ μ)
• 
• 

(part 2: 10.2 - Monoid in the category of endofunctors)

• Monad is just a monoid in the category of endofunctors
• What does that
• Start with a definition with sets

μ :: (a, a) -> a
-- | set has element 'e' which is identity
η :: ( ) -> a

• Can replace (a,a) with product a ⨯ a
• η is morphism from terminal object
• Also need associativity and unit
• μ (μ (x, y), z) = μ(x, μ(y, z))
• μ( η ( ), x) = x
• μ( x, η ( )) = x
• Still using elements from a set though
• Monoid has product and terminal object; or coproduct and initial object
• Monoidal category has tensor product ⊗ and identity I
• So a monoid is an object in a monoidal category with two morphisms
• μ :: m ⊗ m → m
• η :: I → m
• Lax
• Up to isomorphism
• Pair (a,b) is not the same as (b,a)
• Strict has equality
• (a,b) = (b,a)
• (a ⊗ b) ⊗ c = a ⊗ (b ⊗ c)
• Composition of two functors can be treated as a tensor product