effektsysteme.tex

% Kompilieren mit: TEXINPUTS=minted/source: pdflatex -shell-escape %
\documentclass[12pt,compress,ngerman,utf8,t]{beamer}
\usepackage[ngerman]{babel}
\usepackage{ragged2e}
\usepackage{comment}
\usepackage{minted}
\usepackage{wasysym}
\usepackage{tikz}
\usetikzlibrary{calc}
\usepackage[all]{xy}
\usepackage[protrusion=true,expansion=false]{microtype}

\title[Effektsysteme]{\smiley{} Effektsysteme \smiley}
\author[Augsburger Curry Club]{
  Ingo Blechschmidt \\[0.1em] \scriptsize\texttt{<iblech@speicherleck.de>}}
\date[2015-11-05]{\vspace*{-1.5em}\scriptsize Augsburger Curry-Club \\ 5.
November 2015}

\usetheme{Warsaw}

\useinnertheme{rectangles}

\usecolortheme{seahorse}
\definecolor{mypurple}{RGB}{150,0,255}
\setbeamercolor{structure}{fg=mypurple}

\usefonttheme{serif}
\usepackage[T1]{fontenc}
\usepackage{libertine}

\definecolor{darkred}{RGB}{220,0,0}
\newcommand{\hcancel}[5]{%
    \tikz[baseline=(tocancel.base)]{
        \node[inner sep=0pt,outer sep=0pt] (tocancel) {#1};
        \draw[darkred, line width=1mm] ($(tocancel.south west)+(#2,#3)$) -- ($(tocancel.north east)+(#4,#5)$);
    }%
}%

\newcommand{\slogan}[1]{%
  \begin{center}%
    \setlength{\fboxrule}{2pt}%
    \setlength{\fboxsep}{-3pt}%
    {\usebeamercolor[fg]{item}\fbox{\usebeamercolor[fg]{normal
    text}\parbox{0.9\textwidth}{\begin{center}#1\end{center}}}}%
  \end{center}%
}

\renewcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\Id}{\mathrm{Id}}
\newcommand{\Hask}{\mathrm{Hask}}

\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{headline}{}

\setbeamertemplate{title page}[default][colsep=-1bp,rounded=false,shadow=false]
\setbeamertemplate{frametitle}[default][colsep=-2bp,rounded=false,shadow=false,center]

\newcommand*\oldmacro{}%
\let\oldmacro\insertshorttitle%
\renewcommand*\insertshorttitle{%
  \oldmacro\hfill\insertframenumber\,/\,\inserttotalframenumber\hfill}

\newcommand{\hil}[1]{{\usebeamercolor[fg]{item}{\textbf{#1}}}}
\setbeamertemplate{frametitle}{%
  \vskip1em%
  \leavevmode%
  \begin{beamercolorbox}[dp=1ex,center]{}%
      \usebeamercolor[fg]{item}{\textbf{\textsf{\Large \insertframetitle}}}
  \end{beamercolorbox}%
}

\setbeamertemplate{footline}{%
  \leavevmode%
  \hfill%
  \begin{beamercolorbox}[ht=2.25ex,dp=1ex,right]{}%
    \usebeamerfont{date in head/foot}
    \insertframenumber\,/\,\inserttotalframenumber\hspace*{1ex}
  \end{beamercolorbox}%
  \vskip0pt%
}

\newcommand{\backupstart}{
  \newcounter{framenumberpreappendix}
  \setcounter{framenumberpreappendix}{\value{framenumber}}
}
\newcommand{\backupend}{
  \addtocounter{framenumberpreappendix}{-\value{framenumber}}
  \addtocounter{framenumber}{\value{framenumberpreappendix}}
}

\setbeameroption{show notes}
\setbeamertemplate{note page}[plain]

\begin{document}

\frame{\titlepage}

\frame{\tableofcontents}

\section{Spezifikation von Instruktionen}
\begin{frame}[fragile]\frametitle{Gewünschte Instruktionen}
  \begin{minted}{haskell}
type St = ...
data StateI :: * -> * where
    Get :: StateI St
    Put :: St -> StateI ()
  \end{minted}

  \vfill
  \slogan{Freie Funktoren und freie Monaden liefern ein allgemeines
  Konstruktionsrezept für Monaden mit gewünschter operationeller Semantik.}
\end{frame}

\begin{frame}[fragile]\frametitle{Gewünschte Instruktionen}
  \begin{minted}{haskell}
type St = ...
data StateI :: * -> * where
    Get :: StateI St
    Put :: St -> StateI ()

type Env = ...
data ReaderI :: * -> * where
    Ask :: ReaderI Env

type Log = ...
data WriterI :: * -> * where
    Tell :: Log -> WriterI ()
  \end{minted}
\end{frame}

\begin{frame}[fragile]\frametitle{Gewünschte Instruktionen}
  \begin{minted}{haskell}
type Err = ...
data ErrorI :: * -> * where
    Throw :: Err -> ErrorI a

data IOI :: * -> * where
    PutStrLn :: String -> IOI ()
    GetLine  :: IOI String
    Exit     :: IOI a
  \end{minted}
\end{frame}


\section{Freie Funktoren}
\begin{frame}[fragile]\frametitle{Freie Funktoren}
  Wir können aus einem Typkonstruktor \texttt{t :: * -> *} auf unspektakulärste
  Art und Weise einen Funktor machen:

  \begin{minted}{haskell}
class Functor f where
    fmap :: (a -> b) -> (f a -> f b)

data FreeF t a = MkFreeF (exists r. (t r, r -> a))
data FreeF t a = forall r. MkFreeF (t r) (r -> a)
-- MkFreeT :: t r -> (r -> a) -> FreeF t a

liftF :: t a -> FreeF t a
liftF x = MkFreeF x id

instance Functor (FreeF t) where
    fmap phi (MkFreeF x h) = MkFreeF x (phi . h)
  \end{minted}
\end{frame}

\note{\justifying
  Wenn \texttt{t} ein Funktor \emph{wäre}, so könnte man eine Funktion
  \texttt{r -> a} zu einer Funktion \texttt{t r -> t a} liften. Wenn \texttt{t}
  kein Funktor ist, geht das nicht.
  \medskip

  Der freie Funktor \texttt{FreeF t} über \texttt{t} \emph{cheatet}: Ein Wert
  vom Typ \texttt{Free t a} besteht aus einem Wert \texttt{x :: t r} zusammen
  mit einer Funktion \texttt{f :: r -> a}. Anschaulich stellen wir uns diese
  Kombination als das vor, was \texttt{fmap f x} ergäbe, wenn \texttt{t} ein
  Funktor wäre.
  \medskip

  Die Implementierung von \texttt{fmap phi} für \texttt{FreeF t} ist dann rein
  \emph{formal}: Anstatt \texttt{phi} wirklich auf einen Wert vom Typ \texttt{t
  r} anzuwenden (was unmöglich ist), notieren wir uns nur die Information, dass
  \texttt{phi} anzuwenden \emph{wäre}.
  \par
}

\note{\justifying
  Das Paar bestehend aus dem \emph{freien Funktor~\texttt{FreeF t} über~\texttt{t}}
  und der Funktion~\texttt{liftF} erfüllt folgende \emph{universelle
  Eigenschaft}:
  \medskip

  Ist~\texttt{G} irgendein Funktor und~\texttt{phi :: t a -> G a} irgendeine
  Funktion, so existiert genau eine Funktion~\texttt{phi' :: FreeF t a -> G a}
  mit~\texttt{phi' . liftF = phi}.
  \[ \xymatrix{
    \texttt{t} \ar@{=>}[rr]^{\texttt{phi}} \ar@{=>}[rd]_{\texttt{liftF}} && G \\
    & \texttt{FreeF t} \ar@{==>}[ru]_{\texttt{phi'}}
  } \]
}

\note{\justifying
  Einen Typkonstruktor~\texttt{t :: * -> *} kann man auch als einen
  Funktor~$\Hask_0 \to \Hask$ auffassen. Dabei hat die Kategorie~$\Hask_0$
  dieselben Objekte wie~$\Hask$, enthält aber nur Identitätsmorphismen.
  \medskip

  Der freie Funktor über~\texttt{t} ist dann die \emph{Links-Kan-Erweiterung}
  von~\texttt{t} längs der Inklusion~$\Hask_0 \hookrightarrow \Hask$.
  Die angegebene Definition von~\texttt{FreeF t} ist nichts anderes als die
  \emph{Koendeformel} für Links-Kan-Erweiterungen.
  \medskip
  \[ \xymatrixcolsep{4pc}\xymatrixrowsep{4pc}\xymatrix{
    \Hask \ar@{-->}[rd]^{\texttt{FreeF t}} \\
    \Hask_0 \ar[r]^{\texttt{t}} \ar@{^{(}->}[u] & \Hask
  } \]
  \medskip

  \[
    \texttt{FreeF t a} = \int^{r \in \Hask_0} (\texttt{t r}, \texttt{r -> a})
  \]
}

\begin{frame}[plain]
  \begin{center}
    \includegraphics[height=\textheight]{images/kan-extension}
  \end{center}
\end{frame}

\begin{frame}[fragile]\frametitle{Beispiel: Zustand}
  \begin{minted}{haskell}
class Functor f where
    fmap :: (a -> b) -> (f a -> f b)

data FreeF t a = forall r. MkFreeF (t r) (r -> a)

data StateI :: * -> * where
    Get :: StateI St
    Put :: St -> StateI ()

-- `FreeF StateI` ist isomorph zu:
data StateF a = Get (St -> a) | Put St a
  \end{minted}
\end{frame}

\note{\justifying
  Offensichtlich wird \texttt{StateF} zu einem Funktor. Das
  zugehörige~\texttt{fmap} ist recht langweilig:

  \inputminted{haskell}{images/statef-functor.hs}

  Genauso langweilig sind die Funktor-Instanzen von anderen Typkonstruktoren
  der Form~\texttt{FreeF t}.\par
}

\section{Freie Monaden}
\begin{frame}[fragile]\frametitle{Freie Monaden}
  Wir können aus einem Funktor \texttt{f :: * -> *} auf unspektakulärste
  Art und Weise eine Monade machen:
  \begin{minted}{haskell}
data FreeM f a = Pure a | Roll (f (FreeM f a))

instance (Functor f) => Monad (FreeM f) where
    return x = Pure x

    Pure x >>= k = k x
    Roll u >>= k = Roll (fmap (>>= k) u)
  \end{minted}
\end{frame}

\note{\justifying
  Mehr zu freien Monaden in einem separaten Foliensatz:
  \medskip

  \url{http://curry-club-augsburg.de/posts/2015-08-14-ankuendigung-siebtes-treffen.html}
}

\begin{frame}[fragile]\frametitle{Zusammengesetzt}
  \begin{minted}{haskell}
data FreeF t a = forall r. MkFreeF (t r) (r -> a)
data FreeM f a = Pure a | Roll (f (FreeM f a))

-- Also ist `FreeM (FreeF t) a` isomorph zu:
data Prog t a =
    Pure a | forall r. Step (t r) (r -> Prog t a)

data StateI :: * -> * where
    Get :: StateI St
    Put :: St -> StateI ()
-- `Prog StateI a` ist isomorph zu:
data StateProg a
    = Pure a
    | Get    (St -> StateProg a)
    | Put St (StateProg a)
  \end{minted}
\end{frame}

\note{\justifying
  Auch ohne die Motivation über freie Funktoren und freie Monaden besitzt
  \texttt{Prog} eine anschauliche Bedeutung. Wir können uns einen Wert vom
  Typ~\texttt{Prog t a} als eine Folge von Instruktionen vorstellen, die
  schlussendlich einen Wert vom Typ~\texttt{a} produziert. Welche Instruktionen
  vorkommen können, entscheidet~\texttt{t}.
  \medskip

  Ein Wert vom Typ~\texttt{Prog t a} ist entweder von der Form~\texttt{Pure x},
  also ein triviale Folge von Instruktionen mit Produktionswert~\texttt{x},
  oder von der Form~\texttt{Step u k}. Dabei kodiert~\texttt{u} eine
  Instruktion, die bei Ausführung einen Wert~\texttt{x :: r} produziert, und
  die Continuation~\texttt{k :: r -> Prog t a} gibt an, wie es danach weitergehen
  soll.
  \par
}

\begin{frame}[fragile]\frametitle{Operationelle Semantik}
  \begin{minted}{haskell}
data StateProg a
    = Pure a
    | Get    (St -> StateProg a)
    | Put St (StateProg a)

interpret :: StateProg a -> (St -> (a,St))
interpret (Pure x)     st = (x, st)
interpret (Get  k)     st = interpret (k st) st
interpret (Put  st' u) st = interpret u      st'
  \end{minted}
\end{frame}

\begin{frame}[fragile]\frametitle{In Kürze}
  \begin{minted}{haskell}
-- Die freie Monade über dem freien Funktor über t:
data Prog t a =
    Pure a | forall r. Step (t r) (r -> Prog t a)
  \end{minted}

  \begin{itemize}
    \item Werte vom Typ \texttt{Prog t a} sind rein syntaktische Beschreibungen
    von Aktionsfolgen.
    Insbesondere gelten keinerlei besondere Rechenregeln, wie zum
    Beispiel \texttt{Put x (Put x' m) == Put x' m}.
    \item Erst durch Angabe eines Interpreters wird die Konstruktion zum Leben
    erweckt.
    \item Man kann leicht Instruktionsspezifikationen miteinander kombinieren!
    \item In der naiven Implementierung: Effizienzproblem mit linksassoziativer
    Verwendung von \texttt{(>{}>=)}
  \end{itemize}
\end{frame}

\note{\justifying
  Ein und dieselbe freie Monade kann mehrere verschiedene Interpreter zulassen.
  Zum Beispiel kann man in Produktion einen Interpreter verwenden, der eine
  Datenbank anspricht, und zum Testen einen, der fiktive Werte vortäuscht
  (Mocking).
  \medskip

  Siehe unbedingt auch:
  \begin{itemize}
    \item Heinrich Apfelmus. \emph{The Operational Monad Tutorial}. 2010.

    \url{http://apfelmus.nfshost.com/articles/operational-monad.html}
  \end{itemize}
}

\begin{frame}[fragile]\frametitle{Beispiel: Einfaches Multitasking}
  \begin{minted}{haskell}
data ProcessI :: (* -> *) -> * -> * where
    Lift  :: m a -> ProcessI m a
    Stop  :: ProcessI m a
    Fork  :: ProcessI m Bool  -- wie in Unix
    Yield :: ProcessI m ()

-- Interpreter, der nur bei Aufruf von `Yield` die
-- Kontrolle an den nächsten Prozess weitergibt
runCoop   :: (Monad m) => Prog (ProcessI m) a -> m ()

-- Interpreter, der nach jeder Aktion in der Basis-
-- monade die Kontrolle weitergibt
runForced :: (Monad m) => Prog (ProcessI m) a -> m ()
  \end{minted}
\end{frame}

\note{\justifying
  Siehe Beispielcode:
  \medskip

  \url{https://github.com/iblech/vortrag-haskell/blob/master/effektsysteme.hs}
}


\section{Einschub: Koprodukt von Monaden}

\begin{frame}[fragile]\frametitle{Einschub: Koprodukt von Monaden}
  Sind \texttt{m} und \texttt{n} Monaden, so kann man eine Monade bauen, die
  die Fähigkeiten von \texttt{m} und \texttt{n} vereint. Diese heißt
  \emph{Koprodukt} von \texttt{m} und \texttt{n}.
  \medskip

  \small
  \begin{minted}{haskell}
data Sum    m n a = Inl (m a) | Inr (n a)
type Coprod m n a = Prog (Sum m n) a

-- Coprod m n vereint m und n:
inl :: m a -> Coprod m n a    inr :: n a -> Coprod m n a
inl x = Step (Inl x) Pure     inr x = Step (Inr x) Pure

-- Ausführung mit (universelle Eigenschaft):
elim :: (Monad m, Monad n, Monad s)
     => (m a -> s a) -> (n a -> s a)
     -> (Coprod m n a -> s a)
elim = ...
  \end{minted}
\end{frame}

\begin{frame}[fragile]\frametitle{Beispiel: State s $\amalg$ Error e}
  \begin{minted}{haskell}
type Err e = Either e

ex :: Coprod (State Int) (Err String) Int
ex = do
    st <- inl get
    if st <= 0 then inr (Left "Fehler") else do
    inl $ put (st - 1)
    return $ st^2 + st + 1
  \end{minted}
\end{frame}

\note{\justifying
  Ausführung durch Angabe einer Monade, in die man \texttt{State Int} und
  \texttt{Err String} einbetten kann -- zum Beispiel \texttt{IO}:

  \inputminted{haskell}{images/run-coproduct.hs}
}


\section{Effektsysteme}

\begin{frame}[fragile]\frametitle{Effektsysteme}
  \slogan{Effektsysteme lösen das Problem der fehlenden Kompositionalität von Monaden.}

  Die Monade \texttt{Eff r} ist wie \texttt{Prog t}, nur
  \medskip

  \begin{itemize}
    \item performant bezüglich \texttt{(>{}>=)} und
    \item mit \texttt{r} als \emph{Liste} von möglichen Instruktionen (auf
    Typebene) anstatt mit \texttt{t} als Instruktionen kodierenden
    \emph{Typkonstruktor}.
  \end{itemize}

  \begin{minted}{haskell}
    ask :: (Member (Reader env) r) => Eff r env
    get :: (Member (State st)   r) => Eff r st
    put :: (Member (State st)   r) => st -> Eff r ()
    -- Typen schreiben r nicht eindeutig vor!
  \end{minted}
\end{frame}

\note{\justifying
  Wenn man nachträglich seinen Transformerstack ändert, muss man viele
  Typsignaturen und gelegentlich auch einige Codefragmente anpassen (zum
  Beispiel \texttt{lift} in \texttt{lift . lift} ändern). Das ist mühsam.
  \medskip

  Bei Verwendung von \texttt{Eff} muss man das nicht.
  \medskip

  Werte vom Typ \texttt{Eff r a} sind wie bei \texttt{Prog t a} auch nur
  \emph{Beschreibungen} von auszuführenden Aktionen; erst durch Angabe von
  Interpretern können sie ausgeführt werden. Interpreter können leicht
  miteinander kombiniert werden.
  \par
}

\begin{frame}[fragile]\frametitle{Interpreter}
  \begin{minted}{haskell}
type Env = ...
data Reader :: * -> * where
    Get :: Reader Env

ask :: (Member Reader r) => Eff r Env
ask = Roll (inj Get) (tsingleton Pure)

runReader :: Env -> Eff (Reader ’: r) a -> Eff r a
runReader e m = loop m where
    loop (Pure x)   = return x
    loop (Roll u q) = case decomp u of
        Right Get -> loop $ qApp q e
        Left  u   -> Roll u (tsingleton (qComp q loop))
-- kürzer:
runReader e = handleRelay return (\Get k -> k e)
  \end{minted}
\end{frame}

\note{\justifying
  Siehe unbedingt:
  \begin{itemize}
    \item Oleg Kiselyov, Hiromi Ishii. \emph{Freer Monads, More Extensible
    Effects.} 2015.

    \url{http://okmij.org/ftp/Haskell/extensible/more.pdf}

    \item Oleg Kiselyov, Amr Sabry, Cameron Swords.
    \emph{Extensible Effects. An Alternative to Monad Transformers.} 2013.

    \url{http://okmij.org/ftp/Haskell/extensible/exteff.pdf}

    \item Andrej Bauer, Matija Pretnar. \emph{Programming with Algebraic
    Effects and Handlers.} 2012.

    \url{http://arxiv.org/abs/1203.1539}
  \end{itemize}
}

\end{document}