Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
monad_._haskell [2014/09/11 14:25] nikolaj |
monad_._haskell [2015/01/30 12:51] nikolaj |
||
|---|---|---|---|
| Line 59: | Line 59: | ||
| Here is what makes the use of predicates possible: Note that 'join [ [1,2],[],[3],[] ]' is '[1,2,3]' and this is part of the working of the list monads >>=. Since for x=2, y=2, the Bool 'x/=y' isn't 'True', the value '[]' is returned and consequently dropped from the resulting list. | Here is what makes the use of predicates possible: Note that 'join [ [1,2],[],[3],[] ]' is '[1,2,3]' and this is part of the working of the list monads >>=. Since for x=2, y=2, the Bool 'x/=y' isn't 'True', the value '[]' is returned and consequently dropped from the resulting list. | ||
| + | |||
| + | === Examples === | ||
| + | == Example: The List monad == | ||
| + | The list-functors $\text{fmap}$ maps functions $f :: a \to b$ to functions $T(f)$ defined by concatenation with Haskells $\text{map}$ function, i.e. $\text{fmap}\ f\ xs\ =\ [\ f\ a\ |\ a \leftarrow xs\ ]$, e.g. $\text{map}\ (x\mapsto x^2)\ [2,3,4]$ evaluates to $[4,9,16]$. $\text{return}$ then maps terms $x$ of type $a$ to terms $[x]$ (list with one member) of type $[a]$. $\text{join}$ is flatten, e.g. $\text{join}$ applied to the list of lists $[[7,9,3],[2],[5,10]]$ evaluates to $[7,9,3,2,5,10]$. | ||
| + | |||
| + | Now what the functor construction does for you is generating infinite depth (lists of lists of lists of…) and once you’ve proven your system monadic, you know that your arrows are structural throughout the system: E.g. let $f :: \text{Int}\to\text{Char}$, then | ||
| + | * $\text{map}\ f\ (\text{return}\ 3)$ is $\text{map}\ f\ [3]$ is $[f\ 3]$. | ||
| + | * $\text{return}\ (f\ 3)$ is $[f\ 3]$ as well. | ||
| + | Similarly, | ||
| + | * $\text{map}\ f\ (\text{join}\ [[7,3],[2]])$ is $\text{map}\ f\ [7,3,2]$ is $[f\ 7,f\ 3,f\ 2]$. | ||
| + | * $\text{join}\ (\text{map}\ (\text{map}\ f)\ [[7,3],[2]])$ is $\text{join}\ [(\text{map}\ f)\ [7,3],(\text{map}\ f)\ [2]]$ is $\text{join}\ [[f\ 7,f\ 3],[f\ 2]]$ is $[f\ 7,f\ 3,f\ 2]$ as well. | ||
| + | |||
| + | == Example: The Maybe monad == | ||
| + | Types $a$ get mapped to $\text{Maybe}\ a$. For each type $a$, the type $\text{Maybe}\ a$ contains a copy of all of $a$'s terms $x,y,\dots$, there written $\text{Just}\ x,\text{Just}\ y,\dots$, plus an additional term called $\text{Nothing}$. I.e. the maybe functor effectively adds an „exception“ term to all types of $\text{Hask}$. If $f:: a\to b$ and $x::a$, then the arrow image of the functor on $f$ is just the function which maps $\text{Just}\ x$ to $\text{Just}\ f(x)$ and | ||
| + | |||
| + | Return maps $x$ in $a$ to $\text{Just}\ x$ in $\text{Maybe}\ a$ and join maps $\text{Just}\ (\text{Just}\ x)$ to $\text{Just}\ x$ and in particular, $\text{Just}\ \text{Nothing}$ to $\text{Nothing}$. | ||
| == Lifting == | == Lifting == | ||
| Line 71: | Line 87: | ||
| (<*>) :: m (a -> b) -> m a -> m b | (<*>) :: m (a -> b) -> m a -> m b | ||
| (<*>) mg ma = liftM2 id mg my | (<*>) mg ma = liftM2 id mg my | ||
| + | -- or = join $ fmap (\g -> fmap g mx) mg | ||
| </code> | </code> | ||
| + | |||
| Note that conversely, '<*>' doesn't suffice to define a '>>='. | Note that conversely, '<*>' doesn't suffice to define a '>>='. | ||
| - | I'm going to explain what this (<*>) does in mathematical terminology: The Yoneda lemma implies that there is an isomorphism from $FA$ to $\mathrm{nat}(\mathrm{Hom}(A,B),FB)$. Consider a the category with exponential objects and arrows corresponding to components of the natural transformations (such as is the case for Hask, where the above map is $at\mapsto g\mapsto T(g)(ta):FA\to B^A\to FB$), then we can apply the functors arrow map to the latter and obtain a map $FA\to F\,B^A\to FFB)$ to. One could say that this is provides a way to "apply" $tg:F\,B^A$ to $ta:FA$. Note, however, that $T\,B^A$ isn't necessarily a honest function space anymore, so that's abuse of terminology. (For example, 'Noting :: Maybe (Int->Int)' isn't a function. Things still work out, however, because if you pass 'Noting', the outer arrow mapping in the described function takes care of it. In that case the 'tg' value doesn't even matter so this is hardly an "evaluation" of 'Nothing'.). Lastly, if the functor comes with a monadic 'join', then we can get rid of the second $F$ in $FFB$ in the type of the function, and then it's called '<*>'. | + | I'm going to explain what this (<*>) does in mathematical terminology: The Yoneda lemma implies that there is an isomorphism from $FA$ to $\mathrm{nat}(\mathrm{Hom}(A,B),FB)$. Consider a category with exponential objects and arrows corresponding to components of the natural transformations (such as is the case for Hask, where the above map is $at\mapsto g\mapsto T(g)(ta):FA\to B^A\to FB$), then we can apply the functors arrow map to the latter and obtain a map $FA\to F\,B^A\to FFB)$ to. One could say that this is provides a way to "apply" $tg:F\,B^A$ to $ta:FA$. Note, however, that $T\,B^A$ isn't necessarily a honest function space anymore, so that's abuse of terminology. (For example, 'Noting :: Maybe (Int->Int)' isn't a function. Things still work out, however, because if you pass 'Noting', the outer arrow mapping in the described function takes care of it. In that case the 'tg' value doesn't even matter so this is hardly an "evaluation" of 'Nothing'.). Lastly, if the functor comes with a monadic 'join', then we can get rid of the second $F$ in $FFB$ in the type of the function, and then it's called '<*>'. |
| == Alternative definitions == | == Alternative definitions == | ||
| Line 91: | Line 109: | ||
| === Reference === | === Reference === | ||
| + | [[http://en.wikipedia.org/wiki/Monad_%28category_theory%29|Monad (category theory)]], | ||
| + | [[http://de.wikipedia.org/wiki/Monade_%28Informatik%29|Monade (Informatik)]] | ||
| ==== Parents ==== | ==== Parents ==== | ||
| === Subset of === | === Subset of === | ||
| [[Applicative]] | [[Applicative]] | ||
