Return to Answer

in terms of Haskell-primitive function application f x (infixl 10). Composition . is defined in terms of $ as

In programming, a monad is functor type constructor with an instance of the monad type class. There are several equivalent variants of definition and implementation, each carrying slightly different intuitions about the monad abstraction.

 return <=< g = g :: b -> m c Left identity
 f <=< return = f :: c -> m d Right identity
(f <=< g) <=< h = f <=< (g <=< h) :: a -> m d Associativity

encodes computation Maybe t that may not yield a result t, computation that may "fail". The option monad is defined

a -> Maybe b is applied only if Maybe a yields a result.

instance Functor [] where
 map :: (a -> b) -> ([a] -> [b])
 map f (x : xs) = f x : map f xs
 map _ [] = []
instance Monad [] where
 return :: t -> [t]
 return = (: [])
 (=<<) :: (a -> [b]) -> [a] -> [b]
 f =<< (x : xs) = f x ++ f =<< xs
 _ =<< [] = []

Extension concatenates ++ all result lists [b] from applications f x of a Kleisli arrow a -> [b] to elements of [a] into a single result list [b].

forall n. let f = f <=< divisors in f n = []

class Applicative m => Monad m where
 (>>=) :: forall a b. m a -> (a -> m b) -> m b
 (>>) :: forall a b. m a -> m b -> m b
 m >> k = m >>= \ _ -> k
 {-# INLINE (>>) #-}
 return :: a -> m a
 return = pure
 fail :: String -> m a
 fail s = errorWithoutStackTrace s

For simplicitys sake, this explanation uses the type class hierarchy

because not only is every monad a functor, but every applicative is a functor and every monad an applicative, too.

roughly translates to the do block

the equivalent monad comprehension

[p | a <- [1 .. 10], b <- [1 .. 10], let p = a * b, even p]

[1 .. 10] >>= (\ a ->
 [1 .. 10] >>= (\ b ->
 let p = a * b in
 guard (even p) >>
 return p
 )
)

let x = v in e = (\ x -> e) $ v = v & (\ x -> e)
do r <- m; c = (\ r -> c) =<< m = m >>= (\ r -> c)

 fail <|> l = l
 k <|> fail = k
(k <|> l) <|> m = k <|> (l <|> m)

is applied to the result (). If false, then the guard produces the list monad’s fail [], which yields no result for a Kleisli arrow to be applied >> to.

in terms of Haskell-primitive function application f x (infixl 10).

Composition . is defined in terms of $ as

In programming, a monad is a functor type constructor with an instance of the monad type class. There are several equivalent variants of definition and implementation, each carrying slightly different intuitions about the monad abstraction.

 f <=< return = f :: c -> m d Right identity
 return <=< g = g :: b -> m c Left identity
(f <=< g) <=< h = f <=< (g <=< h) :: a -> m d Associativity

encodes computation Maybe t that not necessarily yields a result t, computation that may "fail". The option monad is defined

a -> Maybe b is applied to a result only if Maybe a yields a result.

instance Functor [] where
 map :: (a -> b) -> ([a] -> [b])
 map f (x : xs) = f x : map f xs
 map _ [] = []
instance Monad [] where
 return :: t -> [t]
 return = (: [])
 (=<<) :: (a -> [b]) -> [a] -> [b]
 f =<< (x : xs) = f x ++ (f =<< xs)
 _ =<< [] = []

Extension=<< concatenates ++ all lists [b] resulting from applications f x of a Kleisli arrow a -> [b] to elements of [a] into a single result list [b].

forall n. let { f = f <=< divisors } in f n = []

class Applicative m => Monad m where
 (>>=) :: forall a b. m a -> (a -> m b) -> m b
 (>>) :: forall a b. m a -> m b -> m b
 m >> k = m >>= \ _ -> k
 {-# INLINE (>>) #-}
 return :: a -> m a
 return = pure

For simplicity's sake, this explanation uses the type class hierarchy

because not only is every monad a functor, but every applicative is a functor and every monad is an applicative, too.

roughly translates to the do block,

the equivalent monad comprehension,

[ p | a <- [1 .. 10], b <- [1 .. 10], let p = a * b, even p ]

[1 .. 10] >>= (\ a ->
 [1 .. 10] >>= (\ b ->
 let p = a * b in
 guard (even p) >> -- [ () | even p ] >>
 return p
 )
)

let x = v in e = (\ x -> e) $ v = v & (\ x -> e)
do { r <- m; c }  = (\ r -> c) =<< m = m >>= (\ r -> c)

 k <|> fail = k
 fail <|> l = l
(k <|> l) <|> m = k <|> (l <|> m)

is applied to the result (). If false, then the guard produces the list monad’s fail ( [] ), which yields no result for a Kleisli arrow to be applied >> to, so this p is skipped over.

is defined

in terms of Haskell-primitive function application f x. Composition . is defined in terms of application as

where X, Y are objects in C. HomC(X, Y) is the Homomorphism class of all morphisms X -> Y in C. The functor must preserve morphism identity and composition, the "structure" of C, in D.

• Philip Wadler: The essence of functional programming

• Simon L Peyton Jones, Philip Wadler: Imperative functional programming

• Jonathan M. D. Hill, Keith Clarke: An introduction to category theory, category theory monads, and their relationship to functional programming ́

• Kleisli category

• Eugenio Moggi: Notions of computation and monads

• What a monad is not

is canonically defined

in terms of Haskell-primitive function application f x (infixl 10). Composition . is defined in terms of $ as

where X, Y are objects in C. HomC(X, Y) is the homomorphism class of all morphisms X -> Y in C. The functor must preserve morphism identity and composition, the "structure" of C, in D.

• Philip Wadler: Monads for functional programming

• Simon L Peyton Jones, Philip Wadler: Imperative functional programming

• Jonathan M. D. Hill, Keith Clarke: An introduction to category theory, category theory monads, and their relationship to functional programming ́

• Kleisli category

• Eugenio Moggi: Notions of computation and monads

• What a monad is not

class Functor (f :: * -> *) where
 map :: (a -> b) -> (f a -> f b)

Interpreted as a functor,forall x f g.

and its additive monoid operation

(++) :: [t] -> [t] -> [t]
[]  ++ ys = ys
(x : xs) ++ ys = x : xs ++ ys
infixr 5 ++

Let the proper divisors of a number n be

Do notation and monad comprehensions are syntactic sugar for nested bind expressions.

guard :: MonadPlus m => Bool -> m ()
guard True = return ()
guard False = mzero

Additive monads that support choice and failure, in the sense of Alternative, have an instance of the MonadPlus type class.

class Monad m => MonadPlus m where
 mzero :: m t
 mplus :: m t -> m t -> m t
instance MonadPlus Maybe where
 mzero = Nothing
 Nothing `mplus` m = m
 m `mplus` _ = m
instance MonadPlus [] where
 mzero = []
 mplus = (++)

even p is true, the guard produces [()], and, by the definition of >>, the local constant function

is applied to the result (), returning [p]. If false, the guard produces the list monad’s mzero [], which doesn’t yield a result for a Kleisli arrow to be applied to, and returned is [].

Infamously, monads are used to encode stateful computation. A state processor is a function

that transitions a state st and yields a result t. The state st can be anything. Nothing, flag, count, seed, board, handle, queue, machine, world. The type of state processors is usually called

newtype State st t = State { stateProc :: st -> (t, st) }
instance Functor (State st) where
 map :: (a -> b) -> ((State st) a -> (State st) b)
 map f (State p) = State $ \ s0 -> let (x, s1) = p s0
 in (f x, s1)
instance Monad (State st) where
 return :: t -> (State st) t
 return x = State $ \ s0 -> (x, s0)
 (=<<) :: (a -> (State st) b) -> (State st) a -> (State st) b
 f =<< (State p) = State $ \ s0 -> let (x, s1) = p s0
 in stateProc (f x) s1

A state processorState st t is run by supplying an initial statest:

State access is provided by the auxiliary type class

class Monad m => MonadState m st |m -> st where
 get :: m st
 put :: st -> m ()

m -> st declares a functional dependency of the state type st on the monad m; that a State t will determine the state type to be t uniquely. The unit type

data () = ()

is used analogously to void in C.

instance MonadState (State st) st where
 get = State $ \ s -> (s, s)
 put s = State $ \ _ -> ((), s)
modify :: MonadState m st => (st -> st) -> m ()
modify f = do
 s <- get
 put (f s)
gets :: MonadState m st => (st -> t) -> m t
gets f = do
 s <- get
 return (f s)

The state monad equivalent of the variable threadings0 :: Int

is the equally referentially transparent, but infinitely more elegant and practical

Like in expression-oriented imperative programming (e.g. Rust), the last statement of a block represents its yield. The bind operator is sometimes called a "programmable semicolon".

for :: Monad m => [a] -> (a -> m b) -> m ()
for f = foldr ((>>) . f) (return ())
while :: Monad m => m Bool -> m t -> m ()
while c m = do
 b <- c
 if b then m >> while c m
 else return ()
forever :: Monad m => m t
forever m = m >> forever m

Or should.

<T, eta, –*>

 (–)* : Hom(X, T(Y)) -> Hom(T(X), T(Y))
 (=<<) :: (a -> m b) -> (m a -> m b)

 eta .T g = g
 eta* . g = id . g forall f. id . f = f
 eta* = id forall f g h. f . h = g . h ==> f = g
(f .T g) .T h = f .T (g .T h)
(f* . g)* . h = f* . (g* . h) By definition
(f* . g)* . h = f* . g* . h . is associative
 (f* . g)* = f* . g* forall f g h. f . h = g . h ==> f = g

 mu . T(mu) = mu . mu : T(T(T(X))) -> T(X) Associativity
 join . map join = join . join :: f (f (f t)) -> f t
 mu . T(eta) = mu . eta = id : T(X) -> T(X) Identity
join . map return = join . return = id :: f t -> f t

Implementations of join can be translated from extension form using the equivalence

 mu = id* : T(T(X)) -> T(X)
 join = (id =<<) :: m (m t) -> m t

The reverse translation from mu to extension form is given by

 f* = mu . T(f) : T(X) -> T(Y)
(f =<<) = join . map f :: m a -> m b

instance Monad [] where
 return :: t -> [t]
 return = (: [])
 (=<<) :: (a -> [b]) -> ([a] -> [b])
 (f =<<) = concat . map f

tl;dr

{-# LANGUAGE InstanceSigs #-}
newtype Id t = Id t
instance Monad Id where
 return :: t -> Id t
 return = Id
 (=<<) :: (a -> Id b) -> Id a -> Id b
 f =<< (Id x) = f x

{-# LANGUAGE KindSignatures #-}
class Functor (f :: * -> *) where
 map :: (a -> b) -> (f a -> f b)

Interpreted as a functor,

and its additive monoid operation "append"

(++) :: [t] -> [t] -> [t]
(x : xs) ++ ys = x : xs ++ ys
[] ++ ys = ys
infixr 5 ++

Let the proper divisors of a positive integer n be

Do notation and monad comprehensions are syntactic sugar for nested bind expressions. The bind operator is used for local name binding of monadic results.

let x = v in e = (\ x -> e) $ v = v & (\ x -> e)
 do r <- m; c = (\ r -> c) =<< m = m >>= (\ r -> c)

where

(&) :: a -> (a -> b) -> b
(&) = flip ($)
infixl 0 &

guard :: Additive m => Bool -> m ()
guard True = return ()
guard False = fail

where the unit type or "empty tuple"

data () = ()

Additive monads that support choice and failure can be abstracted over using a type class

class Monad m => Additive m where
 fail  :: m t
 (<|>) :: m t -> m t -> m t
infixl 3 <|>
instance Additive Maybe where
 fail = Nothing
 Nothing <|> m = m
 m <|> _ = m
instance Additive [] where
 fail = []
 (<|>) = (++)

where fail and <|> form a monoid forall k l m.

 fail <|> l = l
 k <|> fail = k
(k <|> l) <|> m = k <|> (l <|> m)

and fail is the absorbing/annihilating zero element of additive monads

_ =<< fail = fail

even p is true, then the guard produces [()], and, by the definition of >>, the local constant function

is applied to the result (). If false, then the guard produces the list monad’s fail [], which yields no result for a Kleisli arrow to be applied >> to.

Infamously, monads are used to encode stateful computation.

A state processor is a function

that transitions a state st and yields a result t. The state st can be anything. Nothing, flag, count, array, handle, machine, world.

The type of state processors is usually called

newtype State st t = State { stateProc :: st -> (t, st) }
instance Functor (State st) where
 map :: (a -> b) -> ((State st) a -> (State st) b)
 map f (State p) = State $ \ s0 -> let (x, s1) = p s0
 in (f x, s1)
instance Monad (State st) where
 return :: t -> (State st) t
 return x = State $ \ s -> (x, s)
 (=<<) :: (a -> (State st) b) -> (State st) a -> (State st) b
 f =<< (State p) = State $ \ s0 -> let (x, s1) = p s0
 in stateProc (f x) s1

A state processor is run by supplying an initial state:

State access is provided by primitives get and put, methods of abstraction over stateful monads:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
class Monad m => Stateful m st |m -> st where
 get :: m st
 put :: st -> m ()

m -> st declares a functional dependency of the state type st on the monad m; that a State t, for example, will determine the state type to be t uniquely.

instance Stateful (State st) st where
 get :: State st st
 get = State $ \ s -> (s, s)
 put :: st -> State st ()
 put s = State $ \ _ -> ((), s)

with the unit type used analogously to void in C.

modify :: Stateful m st => (st -> st) -> m ()
modify f = do
 s <- get
 put (f s)
gets :: Stateful m st => (st -> t) -> m t
gets f = do
 s <- get
 return (f s)

The state monad equivalent of the variable threading

where s0 :: Int, is the equally referentially transparent, but infinitely more elegant and practical

Like in expression-oriented programming (e.g. Rust), the last statement of a block represents its yield. The bind operator is sometimes called a "programmable semicolon".

for :: Monad m => (a -> m b) -> [a] -> m ()
for f = foldr ((>>) . f) (return ())
while :: Monad m => m Bool -> m t -> m ()
while c m = do
 b <- c
 if b then m >> while c m
 else return ()
forever :: Monad m => m t
forever m = m >> forever m

Or, at least, should.

<T, eta, _*>

 (_)* : Hom(X, T(Y)) -> Hom(T(X), T(Y))
 (=<<) :: (a -> m b) -> (m a -> m b)

 eta .T g = g
 eta* . g = g By definition of .T
 eta* . g = id . g forall f. id . f = f
 eta* = id forall f g h. f . h = g . h ==> f = g
(f .T g) .T h = f .T (g .T h)
(f* . g)* . h = f* . (g* . h) By definition of .T
(f* . g)* . h = f* . g* . h . is associative
 (f* . g)* = f* . g* forall f g h. f . h = g . h ==> f = g

 mu . T(mu) = mu . mu : T . T . T -> T . T  Associativity
 join . map join = join . join :: f (f (f t)) -> f t
 mu . T(eta) = mu . eta = id : T -> T Identity
join . map return = join . return = id :: f t -> f t

instance Monad [] where
 return :: t -> [t]
 return = (: [])
 (=<<) :: (a -> [b]) -> ([a] -> [b])
 (f =<<) = concat . map f

Implementations of join can be translated from extension form using the equivalence

 mu = id* : T . T -> T
 join = (id =<<) :: m (m t) -> m t

The reverse translation from mu to extension form is given by

 f* = mu . T(f) : T(X) -> T(Y)
(f =<<) = join . map f :: m a -> m b