Merge branch 'master' of ssh://server.philosophy.fas.nyu.edu/Users/lambda/lambda

[lambda.git] / advanced_topics / monads_in_category_theory.mdwn

diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index e77de46..0cdb5ab 100644 (file)
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -18,6 +18,10 @@ me to be a reasonable way to put the pieces together. We very much welcome
 feedback from anyone who understands these issues better, and will make
 corrections.
 
 feedback from anyone who understands these issues better, and will make
 corrections.
 

+Thanks Wren Thornton for helpful comments on these notes (not yet incorporated).
+
+[This page](http://en.wikibooks.org/wiki/Haskell/Category_theory) was a helpful starting point.
+

 
 Monoids
 -------
 
 Monoids
 -------


@@ -486,6 +490,7 @@ Collecting the results, our monad laws turn out in this format to be:
        (iii.2') (join (unit M)) = the identity transformation
 </pre>
 
        (iii.2') (join (unit M)) = the identity transformation
 </pre>
 

+In category-theory presentations, you may see `unit` referred to as <code>&eta;</code>, and `join` referred to as <code>&mu;</code>. Also, instead of the monad `(M, unit, join)`, you may sometimes see discussion of the "Kleisli triple" `(M, unit, =<<)`. Alternatively, `=<<` may be called <code>&#8902;</code>. These are interdefinable (see below).

 
 
 Getting to the functional programming presentation of the monad laws
 
 
 Getting to the functional programming presentation of the monad laws


@@ -494,12 +499,12 @@ In functional programming, `unit` is sometimes called `return` and the monad law
 
 The base category <b>C</b> will have types as elements, and monadic functions as its morphisms. The source and target of a morphism will be the types of its argument and its result. (As always, there can be multiple distinct morphisms from the same source to the same target.)
 
 
 The base category <b>C</b> will have types as elements, and monadic functions as its morphisms. The source and target of a morphism will be the types of its argument and its result. (As always, there can be multiple distinct morphisms from the same source to the same target.)
 

-A monad `M` will consist of a mapping from types `'t` to types `M('t)`, and a mapping from functions <code>f:C1&rarr;C2</code> to functions <code>M(f):M(C1)&rarr;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&rarr;y</code> into the function that maps `[x1,x2...]` to `[y1,y2,...]`.
+A monad `M` will consist of a mapping from types `'t` to types `M('t)`, and a mapping from functions <code>f:C1&rarr;C2</code> to functions <code>M(f):M(C1)&rarr;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&rarr;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."
 
 
 
 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`:
+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>
        let phi = fun ((_:char), x, y) -> [(1,x,y),(2,x,y)]


@@ -508,7 +513,7 @@ A "monadic value" is any member of a type `M('t)`, for any type `'t`. For exampl
 [-- I intentionally chose this polymorphic function because simpler ways of mapping the polymorphic monad operations from functional programming onto the category theory notions can't accommodate it. We have all the F, MF' (unit G') and so on in order to be able to be handle even phis like this. --]
 
 
 [-- I intentionally chose this polymorphic function because simpler ways of mapping the polymorphic monad operations from functional programming onto the category theory notions can't accommodate it. We have all the F, MF' (unit G') and so on in order to be able to be handle even phis like this. --]
 
 

-Now where `gamma` is another function of type <code>F'('t) &rarr; M(G'('t))</code>, we define:
+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)
 
 <pre>
        gamma =<< phi a  =def. ((join G') -v- (M gamma)) (phi a)