Slides.tex

\documentclass{beamer}
\usepackage{amsmath}
\usepackage{listings}
\usepackage{listings}
\lstset{language=Haskell,basicstyle=\ttfamily}
%\usepackage{beamerthemesplit}
\usetheme{Szeged}

\title{Essence of Functional programming}
\subtitle{Part 2}
\author{Clara B. Behrmann \and Johan Brinch  \and  Frej Soya}
\date{\today}
\newcommand{\bind}{\texttt{>>=}}
\newcommand{\ret}{\texttt{return}}
\newcommand{\bs}{\texttt{\char`\\}}
\newcommand{\fs}{\char`/}   
\newcommand{\at}{\texttt{a}}
\newcommand{\kt}{\texttt{k}}
\newcommand{\mt}{\texttt{k}}
\begin{document}
\lstset{basicstyle=\footnotesize\ttfamily}
%\section*{Introduction}
\begin{frame}
  \titlepage
\end{frame}

\begin{frame}
  \tableofcontents
\end{frame}


\section{The Monad laws}
%\subsection{The 3 Invariants}
\subsection{}
\begin{frame}[fragile]
 \frametitle{Monad Laws}
The monad laws consist of 3 invariants, that any monad must adhere to:

\textbf{1. Left identity:}
\begin{lstlisting}
  return a >>= k = k a
\end{lstlisting}

\textbf{2. Right identity:}
\begin{lstlisting}
  m >>= return = m
\end{lstlisting}

%\begin{align*}
% \text{(1: Left identity)&\ret\ \at~ & &\bind~\texttt{k}& &= \texttt{k a} } \\ 
% &\mt~ & &\bind\ \ret&  &= \texttt{m} && \text{(2: Right identity)}	 \\
%\end{align*}
\textbf{3. Associativity:}
\begin{lstlisting}
     m >>= (\a -> (k a)  >>= (\b -> h b)) 
  = (m >>= (\a ->  k a)) >>= (\b -> h b)
\end{lstlisting}
\begin{align*}
%&&& \text{(3: Associativity)}  \\
%  &&  &\mt\ \bind\ \textbf{(}\texttt{\bs a -> (k a) \bind\ (\bs b -> h b)}\textbf{)} \\
% &=& \textbf{(}&\mt\ \bind\ \texttt{(\bs a -> k a)}\textbf{)} \texttt{ \bind\ (\bs b -> h b)} \\
 % &ToDO && \text{3: Associativity} 
\end{align*}
\end{frame}
\begin{frame}
How to ensure a monad follows the laws \ldots ?
\end{frame}
%\subsection{Using the invariants}
\begin{frame}[fragile]
\frametitle{The Error Monad}
In case you forgot $\ldots$
\begin{lstlisting}
data E = Suc a | Err String
Instance Monad E where
    return a       = Suc a     
    (Suc a) >>= k  = k a
    (Err s) >>= k  = Err s
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Left and Right Identities}
\textbf{Left identity}
\begin{lstlisting}
return a >>= k 
  = (Suc a) >>= k 
  = k a
\end{lstlisting}
%\end{frame}

%\begin{frame}[fragile]
%\frametitle{Right Identity}

\textbf{Right Identity:}\pause

By case analysis on E: Suc a, Err s
%  = (\k (Suc a) -> k a) (\a -> Suc a) (Suc a)
\begin{lstlisting}
(Suc a) >>= return 
  = (Suc a) >>= (\a -> Suc a)
  = (\a -> Suc a) a
  = (Suc a)
\end{lstlisting}\pause
%  = (\k (Err s) -> Err s) (\a -> Suc a) (Err s)
\begin{lstlisting}
(Err s) >>= return
  = (Err s) >>= (\a -> Suc a)
  = (Err s)
\end{lstlisting}
\end{frame}

%\begin{frame}[fragile]
%\frametitle{Associativity}

%\end{frame}

\section{Using the Monad Laws}
\begin{frame}
Why would I care to follow the monad laws\ldots ?
\end{frame}
\subsection{} 
\begin{frame}[fragile]
\frametitle{Monad syntactic sugar in haskell}
\begin{columns}[t]
  \begin{column}{5cm}
\begin{lstlisting}
do { x <- read
   ; y <- read
   ; return x+y
   }
\end{lstlisting}
  \end{column}
  \begin{column}{5cm}
\begin{lstlisting}
    read >>= \x ->    
    read >>= \y ->    
    return x+y
\end{lstlisting}
  \end{column}
\end{columns}

%1-3 slides of examples comparing bind/unit with do-syntax (transliteration)
\end{frame}
\begin{frame}[fragile]
\frametitle{Monad Laws: What's the Point?}		
\begin{columns}[t]
{\onslide<1->
  \begin{column}{5cm}  
\begin{lstlisting}
skip_and_get = 
  do { lineA <- read
     ; lineB <- read 
     ; return lineB 
     }
\end{lstlisting}
  \end{column}  
  }  
{\onslide<3->  
  \begin{column}{5cm}
\begin{lstlisting}
skip_and_get =
  read >>= \lineA ->    
  read >>= \lineB ->    
  return lineB
\end{lstlisting}
  \end{column}
  }
\end{columns}
\begin{columns}[t]
{\onslide<2->
  \begin{column}{5cm}
  \textbf{Expected equivalence:}
\begin{lstlisting}
skip_and_get = 
  do { lineA <- read
     ; read
     }
\end{lstlisting}
  \end{column}
  }
  {\onslide<4->
  \begin{column}{5cm}
    \textbf{By right identity:}
\begin{lstlisting}
skip_and_get =
  read >>= \lineA ->    
  read
\end{lstlisting}
  \end{column}
  }
\end{columns}
\end{frame}


\begin{frame}[fragile]
\frametitle{What's the Point? Cont'd}
\begin{columns}[t]
{\onslide<1->
  \begin{column}{5cm}
\begin{lstlisting}
do { y <- do { x <- read
             ; f x
             }
   ; write y    
   }   
\end{lstlisting}
  \end{column}
  }
  {\onslide<3->
  \begin{column}{5cm}
\begin{lstlisting}
(read >>= (\x -> f x)) 
      >>= (\y -> write y)
      
\end{lstlisting}
  \end{column}
  }
\end{columns}
\begin{columns}[t]
  \begin{column}{5cm}
{\onslide<2->
  \textbf{Expected equivalence:}
\begin{lstlisting}

do { x <- read
   ; y <- f x
   ; write y 
   }
\end{lstlisting}
}
  \end{column}
  \begin{column}{5cm}
{\onslide<4->
\textbf{By Associativity:}
\begin{lstlisting}

read >>= ((\x -> f x) 
     >>= (\y -> write y))
\end{lstlisting}
}
  \end{column}
\end{columns}
\end{frame}


\begin{frame}
\large{$\dots$and now for something completely different$\dots$}
\end{frame}



%%\subsection{Monads and lists}
%\frame{
%\frametitle{For list monads}
%For the list monad together with the 3 invariants. The following invariants for Map and join apply.
%\begin{itemize}
%\item MapM 
%\item JoinM
%\item There are 7 extra invariants.
%\end{itemize}
%using the last one (8th) together with the 7 above, we can deduce the original 3 monad invariants 
%}

%\frame{
%\frametitle{Monads can generalise list comprehensions}
%Not that interesting?, Summary of another paper\\ 
%Basicly any list comprehension in haskell can be translated to a monad.  \\
%Thus list comphensions are syntactic sugar for some monads.
%}
\section{Intro to Continuations}
%\subsection{the CPS Intro}
\subsection{} 
\begin{frame}[fragile]
\frametitle{Continuation Passing Style}

\textbf{Continuation}\\
A continuation is a function representing the remainder of the program (with which to be continued). \\
Values are represented by functions that take such a continuation and return the final result. \\\ \\ 
\pause
\textbf{Monad of Continuations}
\begin{lstlisting}
type K a  = (a -> Answer) -> Answer

return :: a -> (a -> Answer) -> Answer
return a  = \c -> c a

>>= :: K a -> ( a -> K b ) -> K b
m >>= k   = \c -> m (\a -> k a c)
\end{lstlisting}

%>>= :: ((a -> Answer) -> Answer) -> (a -> Answer) -> ((a -> Answer) -> Answer) 
 
 
%The continuation monad ``\texttt{K}'' \\
%Expressing continuations using monads. \\
%TODO: Write the K monad in bind and return form.\\
\end{frame}


%\frame{
%\frametitle{CPS interpreter} 
%\emph{kill this slide}\\  
%Creating a CPS intepreter using monads.
%But this time wadlers also ``simplifies''
%\begin{itemize}
%\item By removing each of occurrence of \bind 
%\item adding  ``bits'' to front to capture the continuation
%\item adding ``bits to the end pass the continuation
%\end{itemize}
% Each operation passes on the actual computation to the next function as a 'continuation'
%}


\begin{frame}[fragile]
\frametitle{Continuation Example?}
\lstset{basicstyle=\footnotesize\ttfamily}
This is how numbers are added in Continuation Passing Style.
\begin{lstlisting}
n23 :: (a -> Answer) -> Answer
n23 = \c -> c 23

cplus :: ((a -> Answer) -> Answer) -> 
         ((a -> Answer) -> Answer) -> 
          (a -> Answer) -> Answer
          
cplus a' b' = 
  \c -> c (a' (\a -> b' (\b -> a + b)))
\end{lstlisting}
\pause Simple as pie, innit?
\end{frame}

\begin{frame}[fragile]
\frametitle{Explaining Black Magic:}
\lstset{basicstyle=\footnotesize\ttfamily}
Now, let's compute \texttt{cplus n23 n19}: 
\begin{lstlisting}
cplus a' b' = 
  \c -> c (a' (\a -> b' (\b -> a + b)))
\end{lstlisting}
\pause
\begin{lstlisting}
cplus n23 n19
= \c -> c (n23          (\a -> n19 (\b ->  a + b))) 
= \c -> c ((\c -> c 23) (\a -> n19 (\b ->  a + b)))
= \c -> c (             (\a -> n19 (\b ->  a + b)) 23)
= \c -> c (                    n19 (\b -> 23 + b))
= \c -> c (           (\c -> c 19) (\b -> 23 + b))
= \c -> c (                        (\b -> 23 + b) 19)
= \c -> c (                               23 + 19)
= \c -> c                                 42
\end{lstlisting}
\lstset{language=Haskell}

%Example with add
%Instead of evaluating the actual ``add``. The ``add'' computations is passed on to the next expression the interpreter meets. \\
%This is done for all Terms, not just add.

\end{frame}



\begin{frame}[fragile]
\frametitle{CPS adding in a monad}
Using Monads to express CPS, readable code is an actual option:

\begin{lstlisting}
n19 >>= (n23 >>= plus)
\end{lstlisting}
Which we can now fold out using the definition of \texttt{>>=}:
\pause
\begin{lstlisting}
m >>= k = \c -> m (\a -> k a c)

  (n23 >>= plus)
= \c -> n23 (\a -> plus a c))
\end{lstlisting}
Which returns a function, that given an argument returns a variable, that
given a continuation returns a value. Unfold once more:
\pause
\begin{lstlisting}
  n19 >>= (\c -> n23 (\a -> plus a c))
= \c1 -> n19 (\b -> (\c -> (n23 (\a -> plus a c)) b c1))
\end{lstlisting}

\pause And lo! This is roughly the same as the old \texttt{cplus}.
\end{frame}



\section{CPS and Monads}
\subsection{}
%\subsection{Monads can express CPS}
\begin{frame}[fragile]
\frametitle{Expressing Monads as CPS}
\textbf{A CPS interpreter can act as a monad interpreter}
\begin{lstlisting}
type Answer = M a

promoteK    :: M a -> K a
promoteK m  =  \c -> m >>= c

showK    :: K a -> String
showK n  =  showM (n unitM)
\end{lstlisting}


%By selecting the right type for \texttt{Answer}, the CPS interpreter can act as the original monad based interpreter. \\
%TODO: Write the definitions of PromoteK, ShowK\\
\end{frame}


\begin{frame}[fragile]
\frametitle{CPS also preserves Modularity}
``Promoting'' an error:
\begin{lstlisting}
errorK   :: String -> K a
errorK s =  promoteK (errorE s)
         =  \c -> (errorE s) >>= c
         =  \c -> (Err s) >>= c
         =  \c ->  Err s
\end{lstlisting}

%Wadler shows it's just as simple with the CPS style monad interpreter as using the monad interpreter. \\ 
%Examples with Error, State and Output monad. (Not that simple but anyhow).
\end{frame}


%\subsection{CPS can express Monads}
\begin{frame}[fragile]
\frametitle{Comparing CPS and Monads}
%Wadler compares CPS and Monads
\begin{itemize}
\item Monads can express CPS
\item CPS can express Monads
\item[$\rightarrow$] CPS always provides an escape facility
\end{itemize}
\end{frame}

\section{Callcc}
\subsection{} 
\begin{frame}[fragile]
\frametitle{Call with Current Continuation}

\begin{lstlisting}
(callcc f)
\end{lstlisting}

\begin{itemize}
\item Call \texttt{f} with the current continuation wrapped in a
  function, \texttt{c}
\item When \texttt{f} calls \texttt{c} the program ``continues''
  execution from where \texttt{callcc} was originally called
\item The expression involving the \texttt{callcc} call returns the
  value passed to the continuation \texttt{c}
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\frametitle{Example Usage}
\begin{itemize}
\item Web Application: Wiki
  \begin{enumerate}
  \item User wants to delete a wiki page
  \item $\rightarrow$ ensure user is logged in 
  \item $\rightarrow$ get confirmation
  \item Delete page
  \end{enumerate}
\end{itemize}

\pause

\lstset{basicstyle=\footnotesize\ttfamily}
\begin{lstlisting}
(fun (delete-page name)
 (unless (get-session-value 'user)
   (setf (get-session-value 'user) 
         (callcc 'wiki-login)))
 (callcc 'wiki-delete-confirm name)
 (delete-page-now name))
\end{lstlisting}
\small
\emph{Courtesy of Troels}

\end{frame}

%\subsection{Examples}
%\frame{
%\frametitle{Example A}
%A
% }
%\frame{
%\frametitle{Example B}
%B
% }
%\frame{
%\frametitle{Example C}
%C
% }

\begin{frame}[fragile]
\section{Conclusion}
\subsection{}
Monads can
\begin{itemize}
\item[$\rightarrow$] add impure features to pure languages
\item[$\rightarrow$] improve modularity
\item[$\rightarrow$] simplify code (hide common operations)
\item[$\rightarrow$] $\dots$ continuations wrapped in Monads yields
  simpler programs
\end{itemize}
\end{frame}


\begin{frame}
\frametitle{Questions?}
\section{Questions?}
\begin{itemize}
\item Monads
\item[$\rightarrow$] $\dots$ Monad laws
\item Continuations
\item[$\rightarrow$] $\dots$ Callcc
\end{itemize}
\end{frame}

\end{document}