+A monad `M` will consist of a mapping from types `'t` to types `M('t)`, and a mapping from functions <code>f:C1→C2</code> to functions <code>M(f):M(C1)→M(C2)</code>. This is also known as <code>lift<sub>M</sub> f</code> for `M`, and is pronounced "function f lifted into the monad M." For example, where `M` is the list monad, `M` maps every type `'t` into the type `'t list`, and maps every function <code>f:x→y</code> into the function that maps `[x1,x2...]` to `[y1,y2,...]`.
+
+
+In functional programming, instead of working with natural transformations we work with "monadic values" and polymorphic functions "into the monad."
+
+A "monadic value" is any member of a type `M('t)`, for any type `'t`. For example, any `int list` is a monadic value for the list monad. We can think of these monadic values as the result of applying some function `phi`, whose type is `F('t)->M(F'('t))`. `'t` here is any collection of free type variables, and `F('t)` and `F'('t)` are types parameterized on `'t`. An example, with `M` being the list monad, `'t` being `('t1,'t2)`, `F('t1,'t2)` being `char * 't1 * 't2`, and `F'('t1,'t2)` being `int * 't1 * 't2`:
+
+<pre>
+ let phi = fun ((_:char, x y) -> [(1,x,y),(2,x,y)]
+</pre>
+
+
+
+Now where `gamma` is another function of type <code>F'('t) → M(G'('t))</code>, we define:
+
+<pre>
+ gamma =<< phi a =def. ((join G') -v- (M gamma)) (phi a)
+ = ((join G') -v- (M gamma) -v- phi) a
+ = (gamma <=< phi) a
+</pre>
+
+Hence:
+
+<pre>
+ gamma <=< phi = fun a -> (gamma =<< phi a)
+</pre>
+
+`gamma =<< phi a` is called the operation of "binding" the function gamma to the monadic value `phi a`, and is usually written as `phi a >>= gamma`.
+
+With these definitions, our monadic laws become:
+
+
+<pre>
+ Where phi is a polymorphic function of type F('t) -> M(F'('t))
+ gamma is a polymorphic function of type G('t) -> M(G'('t))
+ rho is a polymorphic function of type R('t) -> M(R'('t))
+ and F' = G and G' = R,
+ and a ranges over values of type F('t),
+ b ranges over values of type G('t),
+ and c ranges over values of type G'('t):
+
+ (i) γ <=< φ is defined,
+ and is a natural transformation from F to MG'
+ ==>
+ (i'') fun a -> gamma =<< phi a is defined,
+ and is a function from type F('t) -> M(G'('t))
+</pre>
+
+<pre>
+ (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
+ ==>
+ (fun a -> (rho <=< gamma) =<< phi a) = (fun a -> rho =<< (gamma <=< phi) a)
+ (fun a -> (fun b -> rho =<< gamma b) =<< phi a) = (fun a -> rho =<< (gamma =<< phi a))
+
+ (ii'') (fun b -> rho =<< gamma b) =<< phi a = rho =<< (gamma =<< phi a)
+</pre>
+
+<pre>
+ (iii.1) (unit G') <=< γ = γ
+ when γ is a natural transformation from some FG' to MG'
+ ==>
+ (unit G') <=< gamma = gamma
+ when gamma is a function of type F(G'('t)) -> M(G'('t))