-
-
+
(iii.1) (unit G') <=< γ = γ
when γ is a natural transformation from some FG' to MG'
==>
(unit G') is a transformation from G' to MG', so:
- (unit G') <=< γ becomes: ((join G') (M unit G') γ)
+ (unit G') <=< γ becomes: ((join G') (M (unit G')) γ)
+ which is: ((join G') ((M unit) G') γ)
substituting in (iii.1), we get:
- ((join G') (M unit G') γ) = γ
+ ((join G') ((M unit) G') γ) = γ
- which will be true for all γ just in case:
- ((join G') (M unit G')) = the identity transformation, for any G'
-
- which will in turn be true just in case:
- (iii.1') (join (M unit) = the identity transformation
+ which is:
+ (((join (M unit)) G') γ) = γ
+ [-- Are the next two steps too cavalier? --]
+ which will be true for all γ just in case:
+ for any G', ((join (M unit)) G') = the identity transformation
+ which will in turn be true just in case:
+ (iii.1') (join (M unit)) = the identity transformation
+
+
(iii.2) γ = γ <=< (unit G)
when γ is a natural transformation from G to some MR'G
==>
- unit <=< γ becomes: ((join R'G) (M γ) unit)
+ γ <=< (unit G) becomes: ((join R'G) (M γ) (unit G))
substituting in (iii.2), we get:
γ = ((join R'G) (M γ) (unit G))
which by lemma 2, yields:
- γ = ((join R'G) ((unit MR'G) γ)
+ γ = (((join R'G) ((unit MR'G) γ)
+
+ which is:
+ γ = (((join (unit M)) R'G) γ)
+
+ [-- Are the next two steps too cavalier? --]
which will be true for all γ just in case:
- ((join R'G) (unit MR'G)) = the identity transformation, for any R'G
+ for any R'G, ((join (unit M)) R'G) = the identity transformation
which will in turn be true just in case:
(iii.2') (join (unit M)) = the identity transformation
@@ -483,25 +497,20 @@ The base category C will have types as elements, and monadic functions as
A monad `M` will consist of a mapping from types `'t` to types `M('t)`, and a mapping from functions f:C1→C2 to functions M(f):M(C1)→M(C2). This is also known as liftM f 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 f:x→y 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" in question.
-
-A "monadic value" is any member of a type M('t), for any type 't. For example, a list is a monadic value for the list monad. We can think of these monadic values as the result of applying some function (φ : F('t) → M(F'('t))) to an argument `a` of type `F('t)`.
-
+In functional programming, instead of working with natural transformations we work with "monadic values" and polymorphic functions "into the monad."
-Let `'t` be a type variable, and `F` and `F'` be functors, and let `phi` be a polymorphic function that takes arguments of type `F('t)` and yields results of type `MF'('t)` in the monad `M`. An example with `M` being the list 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`:
let phi = fun ((_:char, x y) -> [(1,x,y),(2,x,y)]
-Here phi is defined when `'t = 't1*'t2`, `F('t1*'t2) = char * 't1 * 't2`, and `F'('t1 * 't2) = int * 't1 * 't2`.
-Now where `gamma` is another function into monad `M` of type F'('t) → MG'('t), we define:
+Now where `gamma` is another function of type F'('t) → M(G'('t)), we define:
gamma =<< phi a =def. ((join G') -v- (M gamma)) (phi a)
-
= ((join G') -v- (M gamma) -v- phi) a
= (gamma <=< phi) a
@@ -518,59 +527,59 @@ With these definitions, our monadic laws become:
- Where phi is a polymorphic function from type F('t) -> M F'('t)
- and gamma is a polymorphic function from type G('t) -> M G' ('t)
- and rho is a polymorphic function from type R('t) -> M R' ('t)
+ 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) for some type 't,
- and b ranges over values of type G('t):
+ 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)
-
-
+ and is a function from type F('t) -> M(G'('t))
+
+
(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)
+
-
-
+
(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 FQ'('t) -> M G'('t)
+ when gamma is a function of type F(G'('t)) -> M(G'('t))
fun b -> (unit G') =<< gamma b = gamma
(unit G') =<< gamma b = gamma b
- As below, return will map arguments c of type G'('t)
- to the monadic value (unit G') b, of type M G'('t).
+ Let return be a polymorphic function mapping arguments of any
+ type 't to M('t). In particular, it maps arguments c of type
+ G'('t) to the monadic value (unit G') c, of type M(G'('t)).
(iii.1'') return =<< gamma b = gamma b
+
-
-
+
(iii.2) γ = γ <=< (unit G)
when γ is a natural transformation from G to some MR'G
==>
gamma = gamma <=< (unit G)
- when gamma is a function of type G('t) -> M R' G('t)
+ when gamma is a function of type G('t) -> M(R'(G('t)))
- gamma = fun b -> gamma =<< ((unit G) b)
+ gamma = fun b -> gamma =<< (unit G) b
- Let return be a polymorphic function mapping arguments
- of any type 't to M('t). In particular, it maps arguments
- b of type G('t) to the monadic value (unit G) b, of
- type M G('t).
+ As above, return will map arguments b of type G('t) to the
+ monadic value (unit G) b, of type M(G('t)).
gamma = fun b -> gamma =<< return b
@@ -588,7 +597,7 @@ Summarizing (ii''), (iii.1''), (iii.2''), these are the monadic laws as usually
* `return =<< gamma b = gamma b`
- Usually written reversed, and with `u` standing in for `phi a`:
+ Usually written reversed, and with `u` standing in for `gamma b`:
`u >>= return = u`
@@ -596,6 +605,6 @@ Summarizing (ii''), (iii.1''), (iii.2''), these are the monadic laws as usually
Usually written reversed:
- return b >>= gamma = gamma b
+ `return b >>= gamma = gamma b`