Difference between revisions of "Category theory/Monads"
(→Axioms: supplement missing F in the Axioms) |
|||
(One intermediate revision by one other user not shown) | |||
Line 5: | Line 5: | ||
=== Axioms === |
=== Axioms === |
||
− | #<math>\mu\circ F(\mu)=\mu\circ\ |
+ | #<math>\mu\circ F(\mu)=\mu\circ\mu_F</math> |
− | #<math>\mu\circ\ |
+ | #<math>\mu\circ\eta_F=id=\mu\circ F(\eta)</math> |
=== Examples === |
=== Examples === |
||
Line 127: | Line 127: | ||
= a |
= a |
||
</haskell> |
</haskell> |
||
+ | |||
+ | [[Category:Theoretical foundations]] |
Latest revision as of 17:49, 4 July 2024
Definition
A monad in a category is a triple .
Axioms
Examples
- In any category with arbitrary products, for any object of there is a monad with the object mapping taking the object of to corresponding to the CPS monad in Haskell.
Monads in Haskell
Translating the definition of a monad into Haskell using this terminology would give us
class Functor m => Monad m where
return :: alpha -> m alpha
join :: m (m alpha) -> m alpha
(join, by the way, is one of the most under-appreciated of Haskell library functions; learning it is necessary both for true mastery of Haskell monads. See Monad/join for further explication). The complete collection of class laws (including the natural transformation laws) in Haskell would be
fmap g . return = return . g
fmap g . join = join . fmap (fmap g)
join . fmap join = join . join
join . return = id = join . fmap return
Haskell, of course, actually gives us
class Monad m where
return :: alpha -> m alpha
(>>=) :: m alpha -> (alpha -> m beta) -> m beta
The relationship between these two signatures is given by the set of equations
fmap f a = a >>= return . f
join a = a >>= id
a >>= f = join (fmap f a)
and the monad laws in Haskell are
return x >>= f = f x
a >>= return = a
(a >>= f) >>= g = a >>= \ x -> f x >>= g
We can take the relationship given above as definitional, in either direction, and derive the appropriate set of laws. Taking fmap and join as primitive, we get
return x >>= f
= join (fmap f (return x))
= join (return (f x))
= f x
a >>= return
= join (fmap return a)
= a
(a >>= f) >>= g
= join (fmap g (join (fmap f a)))
= join (join (fmap (fmap g) (fmap f a)))
= join (fmap join (fmap (fmap g) (fmap f a)))
= join (fmap (join . fmap g . f) a)
= a >>= join . fmap g . f
= a >>= \ x -> join (fmap g (f x))
= a >>= \ x -> f x >>= g
Taking (>>=) as primitive, we get
fmap f (return x)
= return x >>= return . f
= return (f x)
fmap f (join a)
= (a >>= id) >>= return . f
= a >>= \ x -> id x >>= return . f
= a >>= \ x -> x >>= return . f
= a >>= fmap f
= a >>= \ x -> id (fmap f x)
= a >>= \ x -> return (fmap f x) >>= id
= (a >>= return . fmap f) >>= id
= join (fmap (fmap f) a)
join (join a)
= (a >>= id) >>= id
= a >>= \ x -> x >>= id
= a >>= \ x -> join x
= a >>= \ x -> return (join x) >>= id
= (a >>= return . join) >>= id
= join (fmap join a)
join (return a)
= return a >>= id
= id a
= a
join (fmap return a)
= (a >>= return . return) >>= id
= a >>= \ x -> return (return x) >>= id
= a >>= \ x -> return x
= a >>= return
= a