From: Nathaniel Wesley Filardo Date: Thu, 2 Apr 2015 04:18:23 +0000 (-0400) Subject: Some old notes probably deserve to be public X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=5c671ebe227f3147294dc1ca1581e93c2099ecd1;p=ctcheat Some old notes probably deserve to be public --- diff --git a/algebras.tex b/algebras.tex new file mode 100644 index 0000000..c11dadc --- /dev/null +++ b/algebras.tex @@ -0,0 +1,336 @@ +\documentclass[letterpaper]{article} +\DeclareSymbolFont{AMSb}{U}{msb}{m}{n} +\DeclareMathAlphabet{\mathbbm}{U}{bbm}{m}{n} + +\title{Functors, Fixed Points, and Algebras; Oh My!} + +\usepackage{amsmath,amssymb,amsthm,latexsym} +\usepackage{fancyhdr} +\usepackage[tiny,center,compact,sc]{titlesec} +\usepackage[cm]{fullpage} +\usepackage{pstricks} +\usepackage{graphicx} +\usepackage{verbatim} +\usepackage{bm} +\usepackage{ifthen} +\usepackage{epsfig} +\usepackage{tikz} + \usetikzlibrary{arrows,calc,matrix,positioning,scopes} +\usepackage{textcomp} +\usepackage{url} +\usepackage{multirow} +\usepackage{hyperref} +\usepackage{listings} + \lstloadlanguages{Haskell} +\usepackage{breakurl} + +\renewcommand{\baselinestretch}{0.9} + +%\newtheorem{thm}{Thm}[section] +%\newtheorem{dfn}{Def}[section] + +\setlength{\parindent}{0pt} +\setlength{\parskip}{3pt} + +%Scalable bracket-like +\newcommand{\paren}[1]{\left({#1}\right)} +\newcommand{\brak}[1]{\left[{#1}\right]} +\newcommand{\abs}[1]{\left\lvert{#1}\right\rvert} +\newcommand{\ang}[1]{\left\langle{#1}\right\rangle} +\newcommand{\set}[1]{\left\{#1\right\}} + +%Mathematics +\newcommand{\condexp}[1]{\ifthenelse{\equal{#1}{false}}{}{^{#1}}} +\newcommand{\dd}[3][false]{\frac{d\condexp{#1}{#2}}{d{#3}\condexp{#1}}} +\newcommand{\pd}[3][false]{\frac{\partial\condexp{#1}{#2}}{\partial{#3}\condexp{#1}}} + +\newcommand{\ifrac}[2]{{#1}/{#2}} + +%Quantum Mechanics +\newcommand{\ket}[1]{\left\lvert{#1}\right\rangle} +\newcommand{\bra}[1]{\left\langle{#1}\right\rvert} +\newcommand{\braket}[2]{\left\langle{#1}\middle\vert{#2}\right\rangle} +\newcommand{\Braket}[3]{\left\langle{#1}\middle\vert{#2}\middle\vert{#3}\right\rangle} +\newcommand{\dyad}[2]{\left\lvert{#1}\middle\rangle\middle\langle{#2}\right\rvert} + +\DeclareMathOperator{\mm}{\mid\mid} + +\newcommand{\defn}[1]{{\bf #1}} + +\begin{document} +\maketitle + +For a given endofunctor $F : \mathcal{C} \to \mathcal{C}$, let +% +\begin{itemize} +% + \item $(\mu F, in)$ denote its initial algebra ($in : F(\mu F) \to \mu F$) + A {\em catamorphism} $h$ is the unique arrow from an initial algebra to + any other $a$; it must be the solution to the equation $h \circ in = a + \circ F h$. +% + \item $(\nu F, out)$ denote its terminal coalgebra ($out : \nu F \to F(\nu + F)$) An {\em anamorphism} of a coalgebra $c$ is the unique solution to $c + \circ h = F h \circ out$. +% +\end{itemize} + + +\section{Special Fixed Points} + +\subsection{Carrier of Initial Algebra Implies Fixed Point} + +Assume that $(\mu F, in)$ exists; then $(F(\mu F), F(in))$ is also an +$F$-algebra (because $F(in) : F(F(\mu F)) \to F(\mu F)$) and the following +diagram exists in $\mathcal{C}$: +% +\begin{center}\begin{tikzpicture} + + \matrix (m) [matrix of math nodes, row sep=3em, column sep=6em] + % + { F(\mu F) & F(F(\mu F)) & F(\mu F) \\ \mu F & F(\mu F) & \mu F \\ }; + + \path [->] (m-1-1) edge node [above] {$F(\phi_F(F(in))$} (m-1-2) ; + + \path [->] (m-1-2) edge node [above] {$F(in)$} (m-1-3) ; + + \path [->] (m-1-1) edge node [left] {$in$} (m-2-1) ; + + \path [->] (m-1-2) edge node [left] {$F(in)$} (m-2-2) ; + + \path [->] (m-2-1) edge node [below] {$\phi_F(F(in))$} (m-2-2) ; + + \path [->] (m-2-2) edge node [below] {$in$} (m-2-3) ; + + \path [->] (m-1-3) edge node [right] {$in$} (m-2-3) ; + + \node at ($(m-1-1)!0.5!(m-2-2)$) {$\circ$} ; + + \node at ($(m-1-2)!0.5!(m-2-3)$) {$\circ$} ; + +\end{tikzpicture}\end{center} +% +where $\phi_F(F(in))$ is the catamorphism of $F(in)$: the unique arrow +guaranteed to exist by initiality of $(\mu F, in)$ such that the left square +commutes. The right square trivially commutes and is rendered only for +convenience. (Note that $\phi_F(in) = id$ by initiality!) + +We see that $in \circ \phi_F(F(in))$ (the bottom two arrows of the diagram) +form an algebra homomorphism from $(\mu F, in)$ to itself. By initiality, +this must be the identity: $in \circ \phi_f(F(in)) = 1_{\mu F}$. + +The top-left and middle edges compose to give $F(in) \circ F(\phi_F(F(in))$, +which is just $F(in \circ \phi_F(F(in)))$ (because functors distribute over +compostion), which we know to be $F(1_{\mu F})$, which is $1_{F(\mu F)}$ +(because functors send identity arrows to identity arrows). By commutation +of the left square, the left and bottom-left arrows' composition, +$\phi_F(F(in)) \circ in = 1_{F(\mu F)}$. + +All told, then, $in$ is an isomorphism with inverse $in^{-1} = \phi_F(F(in))$. +That is, $\mu F$ satisfies the equation $\mu F \simeq F(\mu F)$, so $\mu F$ +is a fixed point of $F$. (This is apparently known as ``Lambek's Lemma''.) + +\subsection{Carrier of Final Coalgebra Implies Fixed Point} + +The above argument dualizes in a straightforward way. +% +\begin{center}\begin{tikzpicture} + + \matrix (m) [matrix of math nodes, row sep=3em, column sep=6em] + % + { F(\nu F) & F(F(\nu F)) & F(\nu F) \\ \nu F & F(\nu F) & \nu F \\ }; + + \path [<-] (m-1-1) edge node [above] {$F(\psi_F(F(out))$} (m-1-2) ; + + \path [<-] (m-1-2) edge node [above] {$F(out)$} (m-1-3) ; + + \path [<-] (m-1-1) edge node [left] {$out$} (m-2-1) ; + + \path [<-] (m-1-2) edge node [left] {$F(out)$} (m-2-2) ; + + \path [<-] (m-2-1) edge node [below] {$\psi_F(F(out))$} (m-2-2) ; + + \path [<-] (m-2-2) edge node [below] {$out$} (m-2-3) ; + + \path [<-] (m-1-3) edge node [right] {$out$} (m-2-3) ; + + \node at ($(m-1-1)!0.5!(m-2-2)$) {$\circ$} ; + + \node at ($(m-1-2)!0.5!(m-2-3)$) {$\circ$} ; + +\end{tikzpicture}\end{center} +% +Where $\psi_F(F(out))$ is the anamorphism guaranteed by terminality of $(\nu +F, out)$. $\psi_F(F(out)) \circ out = 1_{\nu F}$ by terminality (and +$\psi_F(out) = id$; also note that dualization has swapped which half of the +isomorphism follows immediately!). In the other direction, $out \circ +\psi_F(F(out)) = F(\psi_F(F(out))) \circ F(out) = F(\psi_F(F(out)) \circ +out) = F(1_{\nu_F}) = 1_{F(\nu_F)}$. + +Thus $out$ is an isomorphism with inverse $out^{-1} = \psi_F(F(out))$ and +$\nu_F$ satisfies $\nu_F \simeq F(\nu F)$, making it another fixed point. + +\subsection{Other Fixed Points} + +We know that {\em any} fixed point of $F$ in fact, call it $\theta F$, has +the property of being isomorphic to $F(\theta F)$. + +\subsubsection{An Example or Two of Fixed Points} + +For the purpose of this section, consider the lovely binary tree functor on +the category $\mathbf{Set}$, which has (countable) (co)products, initial +object $\emptyset$ and terminal object $1$; i.e., $T x = 1 + x \times x$. +Then, +% +\begin{itemize} +% + \item One fixed point, in fact the smallest, of $F$ is the collection of + {\em finite} binary trees with $1$ at its leaves. This is the usual thing + obtained by inflation. +% + \item The largest is binary trees with {\em countable} (including finite) + paths (and $1$ leaves). This cannot be defined by inflation but is + clearly closed under $T$: taking the product of two such such objects is + clearly another such object. +% + \item Another intermediate structure $\theta T$ is less obvious: trees + which may descend {\em left} countably many times but {\em right} only + finitely many times. Again, we cannot grow this by inflation but can + argue that the product of any two such objects is, indeed, another such + object. +% +\end{itemize} +% +Note that, indeed, as we might expect, $\mu T \subsetneq \theta T \subsetneq +\nu T$. The ``other $\theta T$'' (which swaps left and right) is also +between $\mu T$ and $\nu T$, but is not comparable to $\theta T$: fixed +points form a partial order with a single bottom and single top. + +Consider a different functor, the diagonal product functor $\Delta x = x +\times x$, which is like $T$ except that it omits the ``$1 +$'' part. In +this case, +% +\begin{itemize} +% + \item $\mu \Delta = \emptyset$. There's nothing to force us away and + $\Delta \emptyset = \emptyset \times \emptyset \simeq \emptyset$. +% + \item The terminal object $1$ is $\nu \Delta$: $\Delta 1 = 1 \times 1 + \simeq 1$. For ease of understanding, this is the singleton set whose + element represents a tree that is its own root's left and right child. +% + \item There are no other fixed points of $\Delta$. (Stated without + proof!) +% +\end{itemize} +% +As before, $\mu \Delta \subseteq \nu \Delta$. + +\subsection{Induced Duals} + +Because of the two isomorphisms above, we know that $(\mu F, \phi_F(F(in))) = +(\mu F, in^{-1})$ exists and is a coalgebra; similarly, $(\nu F, +\psi_F(F(out))) = (\nu F, out^{-1})$ exists and is an algebra. That is, we +have these diagrams (on the left are $F$-algebras and on the right are +$F$-coalgebras; both diagrams take place in $\mathcal{C}$): +% +\begin{center}\begin{tikzpicture} + + \matrix (m) [matrix of math nodes, row sep=3em, column sep=6em] + % + { F(\mu F) & F(\nu F) & & F(\mu F) & F(\nu F) \\ + \mu F & \nu F & & \mu F & \nu F \\ } ; + + \path [->] (m-1-1) edge node [left] {$in$} (m-2-1) ; + \path [->] (m-1-2) edge node [right] {$out^{-1}$} (m-2-2) ; + \path [->] (m-2-1) edge node [below] {$\phi_F(out^{-1})$} (m-2-2) ; + \path [->] (m-1-1) edge node [above] {$F(\phi_F(out^{-1}))$} (m-1-2) ; + \node at ($(m-1-1)!0.5!(m-2-2)$) {$\circ$} ; + + \path [->] (m-2-4) edge node [left] {$in^{-1}$} (m-1-4) ; + \path [->] (m-2-5) edge node [right] {$out$} (m-1-5) ; + \path [->] (m-2-4) edge node [below] {$\psi_F(in^{-1})$} (m-2-5) ; + \path [->] (m-1-4) edge node [above] {$F(\psi_F(in^{-1}))$} (m-1-5) ; + \node at ($(m-1-4)!0.5!(m-2-5)$) {$\circ$} ; + +\end{tikzpicture}\end{center} +% +where, again, $\phi_F(out^{-1}) = \phi_F(\psi_F(F(out)))$ is the unique arrow that +makes the diagram commute, guaranteed to exist by initiality of $(\mu F, +in)$ and, dually, $\psi_F(\phi_F(F(in))) = \psi_F(in^{-1})$ by terminality of +$(\nu F, out)$. Note that this existence argument does {\em not} make these +arrows equal. + +\subsubsection{Example Induced Coalegbra} + +For this section, we're going to write fuctions in Haskell, though only for +its syntax. Please read all definitions as strict and total! + +Consider the List (of $A$s) $\mathbf{Set}$ endo-functor $ListF~x = 1 + A \times +x$. Let's give it a Haskell rendering, choosing $A = \text{Int}$ just to +dodge polymorphism: +% +\begin{lstlisting}[language=Haskell] +data ListF rec = FNil | FCons Int rec +\end{lstlisting} +% +$\mu L$ is (isomorphic to) the traditional \textsc{lisp}-y lists whose +elements are of type $A$: +% +\begin{lstlisting}[language=Haskell] +data MuListF = MLNil | MLCons Int MuListF +\end{lstlisting} +% +$in : L (\mu L) \to \mu L$ sends $1$ to the empty +list and $a \times l$ to the list whose head is $a$ and tail is $l$: +% +\begin{lstlisting}[language=Haskell] +_in :: ListF MuListF -> MuListF +_in FNil = MLNil +_in (FCons i l) = MLCons i l +\end{lstlisting} +% +Moreover, we know (stated without proof) that $L$'s catamorphism is an +uncurried foldr: looking at the type, we see $\phi_L : \forall_X . (L X \to +X) \to (\mu L \to X)$. (Expanding things a bit, this is $\forall_X . ((1 + +A \times X) \to X) \to \mu L \to X$ which is iso to $\forall_X . (A \to X +\to X) \to X \to \mu L \to X$.) In particular, it is +% +\begin{lstlisting}[language=Haskell] +phiL :: forall a . (ListF a -> a) -> MuListF -> a +phiL f MLNil = f (FNil) +phiL f (MLCons i l) = f (FCons i (phiL f l)) +\end{lstlisting} +% +As required, $\phi_L(in) = id$: +% +\begin{lstlisting}[language=Haskell] +phiL _in MLNil = _in FNil = MLNil + +phiL _in (MLCons i l) + = _in (FCons i (phiL f l)) + = _in (FCons i l) -- induction + = MLCons i l +\end{lstlisting} +% +$in^{-1} = \phi_L(L(in))$ instantiates $\phi_L$ with $X = L (\mu L)$. The +function $L(in) : L (L \mu L) \to L \mu L$ then is just \texttt{fmap in}. +So $in^{-1} = \phi_L(L(in)) : \mu L \to L \mu L$ is +\begin{lstlisting}[language=Haskell] +phiL (fmap _in) MLNil = (fmap _in) FNil = FNil + +phiL (fmap _in) (MLCons i l) + = (fmap _in) (FCons i (phiL (fmap _in) l)) + = FCons i (_in (phiL (fmap _in) l)) + = FCons i l +\end{lstlisting} + +\subsubsection{Example Induced Algebra} + +$\nu L$ is the set of possibly-infinite lists: it contains all of $\mu L$ as +well as the non-terminating lists. $out$ sends nil to the left $1$ and a +list with cons cell top to the right product of its head and tail. So what +is $\psi_L$? We know from looking at the diagram that it must have type +$\forall_X . (X \to L X) \to X \to \nu L$. + +\end{document} diff --git a/monads.tex b/monads.tex new file mode 100644 index 0000000..306bdab --- /dev/null +++ b/monads.tex @@ -0,0 +1,195 @@ +\documentclass[10pt,letterpaper]{article} +\DeclareSymbolFont{AMSb}{U}{msb}{m}{n} +\DeclareMathAlphabet{\mathbbm}{U}{bbm}{m}{n} + +\usepackage{amsmath,amssymb,amsthm,latexsym} +\usepackage{fancyhdr} +\usepackage[tiny,center,compact,sc]{titlesec} +\usepackage[cm]{fullpage} +\usepackage{pstricks} +\usepackage{graphicx} +\usepackage{verbatim} +\usepackage{bm} +\usepackage{ifthen} +\usepackage{epsfig} +\usepackage[all]{xypic} +\usepackage{textcomp} +\usepackage{url} +\usepackage{multirow} +\usepackage{hyperref} +\usepackage{breakurl} +\usepackage{listings} + +\renewcommand{\baselinestretch}{0.9} + +%\newtheorem{thm}{Thm}[section] +%\newtheorem{dfn}{Def}[section] + +\setlength{\parindent}{0pt} +\setlength{\parskip}{3pt} + +%Scalable bracket-like +\newcommand{\paren}[1]{\left({#1}\right)} +\newcommand{\brak}[1]{\left[{#1}\right]} +\newcommand{\abs}[1]{\left\lvert{#1}\right\rvert} +\newcommand{\ang}[1]{\left\langle{#1}\right\rangle} +\newcommand{\set}[1]{\left\{#1\right\}} + +%Mathematics +\newcommand{\condexp}[1]{\ifthenelse{\equal{#1}{false}}{}{^{#1}}} +\newcommand{\dd}[3][false]{\frac{d\condexp{#1}{#2}}{d{#3}\condexp{#1}}} +\newcommand{\pd}[3][false]{\frac{\partial\condexp{#1}{#2}}{\partial{#3}\condexp{#1}}} + +\newcommand{\ifrac}[2]{{#1}/{#2}} + +%Quantum Mechanics +\newcommand{\ket}[1]{\left\lvert{#1}\right\rangle} +\newcommand{\bra}[1]{\left\langle{#1}\right\rvert} +\newcommand{\braket}[2]{\left\langle{#1}\middle\vert{#2}\right\rangle} +\newcommand{\Braket}[3]{\left\langle{#1}\middle\vert{#2}\middle\vert{#3}\right\rangle} +\newcommand{\dyad}[2]{\left\lvert{#1}\middle\rangle\middle\langle{#2}\right\rvert} + +\DeclareMathOperator{\mm}{\mid\mid} + +\newcommand{\defn}[1]{{\bf #1}} +\newcommand{\natto}{\overset{\cdot}{\to}} + +\lstset{mathescape=true} + +\begin{document} + +\section{Expanding The Diagrams} + +The definition and diagrams given in ACC (\S20.1) are sort of terse, so I +have taken the liberty of applying the notation in (\S6.2) and (\S3.23, +footnote 15) and applying the functors to particular objects $X,Y \in +\mathbf{X}$: +\begin{itemize} + \item The definition now reads as: A \defn{monad} on $\mathbf{X}$ is $(T : \mathbf{X} \to \mathbf{X}, + \eta : id_{\mathbf{X}} \natto T, \mu : T^2 \natto T)$ s.t. + \[\forall_X \quad + \xymatrix{ + T^3X \ar[r]^{T(\mu_X)} \ar[d]^{\mu_{TX}} & T^2X \ar[d]^{\mu_{X}} \\ + T^2X \ar[r]^{\mu_X} & TX + } \quad \xymatrix{ + TX \ar[r]^{T(\eta_X)} \ar[dr]_{id_{TX}} & T^2X \ar[d]^{\mu_X} & TX \ar[l]_{\eta_{TX}} \ar[dl]^{id_{TX}} \\ + & TX & + }\] + \item The naturality conditions unpack to be + \[\forall_{X,Y,f} \quad \xymatrix{ + X \ar[r]^{\eta_X} \ar[d]^f & TX \ar[d]^{Tf} \\ + Y \ar[r]^{\eta_Y} & TY + }\quad\xymatrix{ + T^2X \ar[r]^{\mu_X} \ar[d]^{T^2f} & TX \ar[d]^{Tf} \\ + T^2Y \ar[r]^{\mu_Y} & TY + }\] +\end{itemize} + +\section{Translation into Haskell} + +\url{http://en.wikibooks.org/wiki/Haskell/Category_theory#The_monad_laws_and_their_importance} +may be of use, and I am going to try a brief, more equational, exposition +here (with many more parens than strictly necessary; deal with it). + +$\eta$ pretty clearly corresponds to \texttt{return}, and $Tf$ is +\texttt{fmap f}. The naturality condition on $\eta$ is clear: +\begin{lstlisting}[language=Haskell] + fmap f . return -- top right +=== return . f -- bottom left +\end{lstlisting} +This is properly read as a constraint (part of the definition) of +\texttt{return} ($\eta$) in terms of \texttt{fmap} applied at the type +(constructor / functor) associated with our monad (i.e., the morphism part +of the functor). + +Similarly, $\mu$ corresponds to \texttt{join}, whose Haskell definition +is +\begin{lstlisting} +join :: m (m a) -> m a +join mma = (mma >>= id) -- or just "join = (>>= id)" +\end{lstlisting} +(Haskell, by convention, uses \texttt{m} for $T$; sorry for the confusion.) +Its naturality condition says that +\begin{lstlisting} + (fmap f) . join -- top right +=== join . (fmap (fmap f)) -- bottom left +\end{lstlisting} +This says, basically, that you can first run your inner monadic thingie and +then apply a ``lifted'' function to the result, or you can lift the function +twice, so that it applies inside your inner monadic thingie and {\em then} +run the inner thing. Again, this should be taken as a constraint (part of +the definition) on join ($\mu$) in terms of \texttt{fmap}. + +And now the other two laws, which are more interesting and can nicely be +executed in terms of Haskell's \verb|>>=|. First, we have: +\[ \mu_X \circ T(\mu_X) = \mu_X \circ \mu_{TX} \] +or +\begin{lstlisting} +join . (fmap join) === join . join +\end{lstlisting} +Which is easy enough to see: +\begin{lstlisting} + join (fmap join mmmx) += (mmmx >>= return . join) >>= id -- defn join, fmap += (mmmx >>= (\mmx -> return (join mmx))) >>= id -- syntax += (mmmx >>= (\mmx -> return (mmx >>= id))) >>= id -- defn join += mmmx >>= (\mmx -> (return (mmx >>= id) >>= id)) -- assoc >>= += mmmx >>= (\mmx -> id (mmx >>= id)) -- left-identity >>= += mmmx >>= (\mmx -> mmx >>= id) -- apply += mmmx >>= (\mmx -> mmx) >>= id -- assoc >>= += (mmmx >>= id) >>= id -- assoc >>= += join (join mmmx) -- defn join, join +\end{lstlisting} +If we label our \text{mmmx} object as $\mathtt{m_1 m_2 m_3 x}$, this +says, in some pseudo-notation, that $\mathtt{join (m_1 (m_{23} x))}$ +is the same as $\mathtt{join (m_{12} (m_3 x))}$. + +And for the last, we have: +\[ id = \mu_X \circ T(\eta_X) = \mu_X \circ \eta_{TX} \] +or +\begin{lstlisting} +id === join . (fmap return) === \tx -> join . (return tx) +\end{lstlisting} +(note that we do not interpret $\eta_{TX}$ as \texttt{return . return}, but +as \texttt{return tx}! There's no guarantee that a (generalized) element of +$TX$ is the result of $\eta_X$ -- consider, for example, the \texttt{Either +e} (i.e., $(e+)$) monads!) +which again admits executable rewriting (I have taken the liberty of +subscripting some functions, just to make the rewrites clearer.) +\begin{lstlisting} + join (fmap return tx) += join (tx >>= return$_1$ . return$_2$) -- defn fmap += (tx >>= return$_1$ . return$_2$) >>= id -- defn join += (tx >>= (\x -> return$_1$ (return$_2$ x))) >>= id -- syntax += tx >>= (\x -> ((return$_1$ (return$_2$ x)) >>= id) -- assoc >>= += tx >>= (\x -> id (return$_2$ x)) -- left-identity >>= += tx >>= (\x -> return$_2$ x) -- apply += tx >>= return$_2$ -- syntax += tx -- right-identity >>= +\end{lstlisting} +and +\begin{lstlisting} + \tx -> join . (return tx) += \tx -> ((return tx) >>= id) -- defn join += \tx -> (id tx) -- left-identity >>= += \tx -> tx -- apply += id -- defn +\end{lstlisting} + +\section{Speaking of Haskell} + +For the curious, \verb|>>=| can be implemented in terms of join (which makes +the above arguments circular (sorry!), but puts Haskell's typical treatment +of Monads on firmer ground): +\begin{lstlisting} +(>>=) :: m a -> (a -> m b) -> m b +ma >>= f = join (fmap f ma) +-- = (fmap f ma) >>= id +-- = (ma >>= return . f) >>= id +-- = ma >>= (\a -> (return (f a) >>= id)) +-- = ma >>= (\a -> id (f a)) +-- = ma >>= \a -> f a +-- = ma >>= f +\end{lstlisting} + +\end{document}