All About Monads

A monad is more of a design pattern than a data structure. That is, there are many data structures that, if you look at them in the right way, turn out to be monads.

The name "monad" comes from the mathematical field of category theory, which studies abstractions of mathematical structures. If you ever take a PhD level class on programming language theory, you will likely encounter that idea in more detail. Here, though, we will omit most of the mathematical theory and concentrate on code.

Follow the tutorial aiming to explain the concept of a monad ant its application to functional programming in a way that is easy to understand and useful to beginning and intermediate Haskell programmers.

Well I need to be a little familiar with Haskell language.

The tutorial is arrange in three parts:

• Part 1: Understanding Monads

  This part provide a basic understanding of the role of monads in functional programming, how monads operate, and how they are declared and used in Haskell.

• Part 2: A Catalog of Sttandard Monads

  This part covers each standard monad in Haskell, giving the definition of the monad and discussing the use of the monad.

• Part 3: Monads in the Real World

  This part covers advanced material relating to monad transformers and real-world issues encountered when programming with monads.

THE BEST WAY TO REALLY UNDERSTAND MONADS IS TO EXPERIMENT WITH MONADIC CODE!

Part 1: Understanding Monads

What is a monad

In short: It is useful to think of a monad as a strategy for combining computations into more complex computations.

Consider a layer of indirection(abstract) at the computations domain and functional programming.

Why should I make the effort to understand monads

According to the author, it is a promising way to help improve code and extend capabilities.

Three useful properties

1. Modularity

   They allow computations to be composed from simpler computations and separate the combination strategy from the actualcomputations being performed.

2. Flexibility

   They allow functional programs to be much more adaptable than equivalent programs written without monads. This is becausethe monad distills the computational strategy into a single place instead of requiring it be distributed throughout the entire program.

3. Isolation

   They can be used to create imperative-style computational structures which remain safely isolated from the main body of thefunctional program. This is useful for incorporating side-effects (such as I/O) and state (which violates referential transparency) into a purefunctional language like Haskell.

Meet the Monads

Type constructors

Use Maybe type constructor throughout this chapter. Maybe in Haskell is similar to option in OCaml. Take the code in [Real World Ocaml] as an example:

let divide x y =
if y = 0 then None else Some (x / y)
;;

The toplevel will show

val divide : int -> int -> int option = <fun>

In Haskell, the definition of Maybe is:

data Maybe a = Nothing | Just a

Noticing the polymorphic a, Maybe Int can be thought of as a Maybe container holding an Int value (or Nothing) and Maybe String would be a container holding a String value (or Nothing same to above).

Maybe a monad

In Haskell a monad is represented as

• a type constructor (call it m)
• a function that builds value of that type (a -> m a)
• and a function that combines values of that type with computations that produce values of that type to produce a new computation for values of that type (m a -> (a -> m b) -> m b) (is know as "bind")

The signatures of the functions are (in Haskell and OCaml):

-- the type of monad m
data m a = ...

-- return is a type constructor that creates monad instances
return :: a -> m a

-- bind is a function that combines a monad instance m a with a computation
-- that produces another monad instance m b from a's to produce a new
-- monad instance m b
(>>=) :: m a -> (a -> m b) -> m b

module type Monad = sig
  type 'a t
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
end

As for the example of caculate the genetic history in sheep cloning experiments.

Bad programming style

maternalGrandfather :: Sheep -> Maybe Sheep
maternalGrandfather s = case (mother s) of
    Nothing -> Nothing
    Just m  -> father m

It get even worse if we want to find great grandparents:

mothersPaternalGrandfather :: Sheep -> Maybe Sheep
mothersPaternalGrandfather s = case (mother s) of
    Nothing -> Nothing
    Just m  -> case (father m) of
        Nothing -> Nothing
        Just gf -> father gf

Let Maybe a monad!

We consider Maybe as the type of monad m, and it's clear that the return function are Jusa a or Nothing. It is clear that a Nothing value at any point in the computation will cause Nothing to be final result. So good programming style would have us create a combinator that captures the behavior we want:

-- comb is a combinator for sequencing operations that return Maybe
comb :: Maybe a -> (a -> Maybe b) -> Maybe b
comb Nothing _ = Nothing
comb (Just x) f = f x

-- now we can use `comb` to build complicated sequences
mothersPaternalGrandfather :: Sheep -> Maybe Sheep
mothersPaternalGrandfather s = (Just s) `comb` mother `comb` father `comb` father

Though we give the comb signatures as Maybe a -> (a -> Maybe b) -> Maybe b which means a b could be different types, we applied comb with mother and father which implies a and b are actually the same(Sheep). Just as the tutorial says:

The combinator is a huge success! The code is much cleaner and easier to write, understand and modify. Notice also that the comb function isentirely polymorphic --- it is not specialized for Sheep in any way. In fact, the combinator captures a general strategy for combining computations that may fail to return a value. Thus, we can apply the same combinator to other computations that may fail to return a value, suchas database queries or dictionary lookups.

Return

In terms of computations, return is intended to have some kind of trivial effect. For example, if the monad represents computations whose side effect is printing to the screen, the trivial effect would be to not print anything.

Bind

• a boxed value, which has type 'a t(OCaml), and
• a function that itself takes un unboxed value of type 'a as input and returns a boxed value of type 'b t as output.

In terms of computations, bind is intended to sequence effects one after another. Continuing the running example of printing, sequencing would mean first printing one string, then another, and bind would be making sure that the printing happens in the correct order.

Doing it with class

Learning Haskell type classes

Not necessary but is recommended.

The standard Monad class definition isn Haskell looks something like this.

class Monad m where
    (>>=)  :: m a -> (a -> m b) -> m b
    return :: a -> m a

while in Coq

Class Monad (M: Type -> Type) : Type :=
    {
    ret : forall {T : Type}, T -> M T
    bind: forall {T U : Type}, M T -> (T -> M U) -> M U
    }

Example continued

instance Monad Maybe where
    Nothing  >>= f = Nothing
    (Just x) >>= f = f x
    return         = Just

Fit into Monad framework as an instance of Monad class.

The monad laws

Monadic operations must obey a set of laws, known as "the monad axioms".

The three fundamental laws

To be a proper monad, the return and >>= functions must work together according to three laws.

1. (return x) >>= f == f x
2. m >>= return == m
3. (m >>= f) >>= g == m >>= (\x -> f x >>= g)