\documentclass[11pt]{beamer}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[english,polish]{babel}
\usetheme{metropolis}

\usepackage{minted}

\begin{document}
	\author{Tomasz Kulis}
	\title{Kontynuacje (i inne abstrakcje)}
	%\subtitle{}
	%\logo{}
	\institute{KSI$^4$}
	\date{2024-05-11}
	%\subject{}
	%\setbeamercovered{transparent}
	%\setbeamertemplate{navigation symbols}{}
	\begin{frame}[plain]
		\maketitle
	\end{frame}
	
	\section{Wprowadzenie}
	\begin{frame}[fragile]
		\frametitle{Funkcje i składnia}

\begin{minted}[escapeinside=||]{haskell}
times2 x = x * 2
\end{minted}

\begin{minted}[escapeinside=||]{scheme}
(define (times2 arg)
  (* arg 2))
\end{minted}

\pause

\begin{minted}[escapeinside=||]{haskell}
factorial 0 = 1
factorial n = n * (factorial (n - 1))
\end{minted}


\begin{minted}[escapeinside=||]{scheme}
(define (factorial n)
  (if (eq? n 0) 1 (* n (factorial (- n 1)))))
\end{minted}
\pause
\begin{minted}[escapeinside=||]{haskell}
map (\x -> x * x) [1, 2, 3] |$\equiv$| [1, 4, 9] 
\end{minted}
\begin{minted}[escapeinside=||]{scheme}
(map (lambda (x) (* x x)) '(1 4 9)) |$\equiv$| '(1 4 9)
\end{minted}

\end{frame}
	\begin{frame}[fragile]
		\frametitle{Kontynuacje}
\begin{minted}{scheme}
(* (+ 1 2) (- 3 7) 5)
\end{minted}
\begin{onlyenv}<2>
\begin{minted}{scheme}
((lambda (x) 
	(* x (- 3 7) 5))
	(+ 1 2))
\end{minted}
\end{onlyenv}
\begin{onlyenv}<3->
\begin{minted}[escapeinside=||]{scheme}
(|\colorbox{lime}{(lambda (x)}|
	|\colorbox{lime}{(* x (- 3 7) 5))}|
	(+ 1 2))
\end{minted}
\end{onlyenv}
\begin{onlyenv}<4->
\begin{minted}[escapeinside=||]{scheme}
(* |$\square$| (- 3 7) 5) ;; kontynuacja
\end{minted}
\onslide<4>{Kontynuacja to abstrakcyjne pojęcie opisujące aktualny stan przebiegu programu, w szczególności nadchodzącej ewaluacji.}
\end{onlyenv}
\end{frame}
\begin{frame}[fragile]
	\frametitle{Kontynuacje}
	Przykład zastosowania kontynuacji poza informatyką można znaleźć
	np. w analizie -- obliczając pochodną złożenia rozbijamy funkcję
	na najbardziej zewnętrzną kontynuację.
	\begin{align*}
		(\sqrt{\cos(x)})' \\
		(\sqrt{\,\cdot\,}(\cos(x)))' \\
		(\sqrt{\,\cdot\,})'(\cos(x)) \cdot (\cos(x))' \\
		\frac{1}{2\sqrt{\cos(x)}} \cdot (-\sin(x))
	\end{align*}
\end{frame}
\begin{frame}[fragile]
\frametitle{Ale dlaczego?}
\begin{onlyenv}<1->
\begin{minted}{scheme}
(define (factorial n)
  (if (eq? n 0) 1 (* n (factorial (- n 1)))))

(factorial 4)
\end{minted}
\end{onlyenv}

\begin{onlyenv}<2->
\begin{minted}{scheme}
(* 4 (factorial 3))
(* 4 (* 3 (factorial 2)))
(* 4 (* 3 (* 2 (factorial 1))))
(* 4 (* 3 (* 2 (* 1 (factorial 0)))))
(* 4 (* 3 (* 2 (* 1 1))))
(* 4 (* 3 (* 2 1)))
(* 4 (* 3 2))
(* 4 6)
24
\end{minted}
\end{onlyenv}

\end{frame}

\begin{frame}[fragile]
	\frametitle{Ale dlaczego?}

\begin{onlyenv}<1->
	\begin{minted}{scheme}
(define (factorial2 a n)
  (if (eq? n 0) a (factorial2 (* n a) (- n 1))))

(factorial2 4)
\end{minted}
\end{onlyenv}

\begin{onlyenv}<2->
\begin{minted}{scheme}
(factorial2 1 4)
(factorial2 (* 1 4) 3)
(factorial2 (* 4 3) 2)
(factorial2 (* 12 2) 1)
(factorial2 (* 24 1) 0)
24
	\end{minted}
\end{onlyenv}
	
\end{frame}
\begin{frame}[fragile]
		\frametitle{CPS}
		Continuation Passing Style to paradygmat programowania, w którym każda (nieprymitywna) funkcja ma typ postaci
		\texttt{... -> (b -> r) -> r}, gdzie ostatni argument to funkcja reprezentująca kontynuację obliczeń.
\pause
\vspace*{-0.5em}
\begin{minted}{scheme}
(define (*# x y cont) (cont (* x y)))
(define (-# x y cont) (cont (- x y)))
(define (eq?# x y cont) (cont (eq? x y)))

(define (factorial# n acc cont) 
  (eq?# n 0 (lambda (b)
    (if b
      (cont acc)
        (*# n acc (lambda (acc2)
          (-# n 1 (lambda (n2)
            (factorial# n2 acc2 cont)))))))))
\end{minted}
\end{frame}
	\begin{frame}
		\frametitle{CPS}
		Specyfika ewaluacji CPS sprawia, że każda ewaluacja następuje ogonowo rekurencyjnie.

		CPS wykorzystywany jest np. w kompilatorach i interpreterach języków --
		rozbicie wyrażenia na CPS pozwala na jego efektywną i schematyczną ewaluację.		
	\end{frame}
\section*{\texttt{call/cc}, czyli \texttt{goto} języków funkcyjnych}
	\begin{frame}[fragile]
		\frametitle{\texttt{call-with-current-continuation}}
		Funkcja \texttt{call-with-current-continuation} (zazwyczaj nazywana \text{call/cc} w związku z jej aliasem w językach Scheme) przyjmuje jako argument inną funkcję jednoargumentową, i przekazuje jej ,,funkcję zwrotu do obecnej kontynuacji''. Co to oznacza?
\pause
\begin{minted}{scheme}
(define (call/cc-example)
  (call/cc (lambda (cont) (+ 1 2 (cont 3)))))
\end{minted}

\pause
	 \text{call/cc} przekazuje swojemu argumentowi funkcję podobną do \texttt{goto} lecz przyjmującą wartość, i na jej wykonaniu skacze do miejsca wywołania \text{call/cc}, przekazując otrzymaną wartość jako wartość wywołania \text{call/cc}
	\end{frame}
\begin{frame}[fragile]
		\frametitle{Pętle przez \texttt{call/cc}}
\vspace*{-0.3em}
\begin{minted}{scheme}
(define loop-cont #f)
(define (example-loop)
  (match (call/cc (lambda (cont)
                    (set! loop-cont cont)
                    0))
    [5 'done]
    [x (display x)
       (loop-cont (+ x 1))]))
\end{minted}
\pause
\vspace*{-0.3em}
\begin{minted}{scheme}
(define (example-break)
  (call/cc (lambda (break)
    (for-each (lambda (x)
      (if (> x 3)
        (break x)
        (display x)))
      '(1 2 3 4 5)))))
\end{minted}
	\end{frame}
	\begin{frame}[fragile]
		\frametitle{Wyjątki przez \texttt{call/cc}}
		Uogólniając poprzedni przykład z \texttt{break}, możemy wykorzystać \texttt{call/cc} do zaimplementowania wyjątków.
\begin{minted}{scheme}
(define (div# fail a b)
    (if (eq? b 0) 
        (fail 'divby0)
        (/ a b)))

(define (example-nothrow)
    (call/cc (lambda (throw)
       (map (div# throw 10) '(1 2 3)))))

(define (example-throws)
    (call/cc (lambda (throw)
       (map (div# throw 10) '(4 1 0)))))
\end{minted}		
\end{frame}
\begin{frame}[fragile]
		\frametitle{Wyjątki przez \texttt{call/cc}}
\begin{minted}{scheme}
(define (catch (handler block cont))
    (cont 
        (match (call/cc (lambda (back) 
            (block (lambda (x) (list 'error x)))))
            [(list 'error err) (handler err)]
            [x x]))
\end{minted}
\end{frame}
	\begin{frame}[fragile]
		\frametitle{Korutyny przez \texttt{call/cc}}
\begin{minted}{scheme}
(define (printer other)
    (display "Example1")
    (set! other (call/cc other))
    (display "Example2")
    (set! other (call/cc other))
    (display "Example3"))

(define (sleeper other)
    (sleep 5)
    (set! other (call/cc other))
    (sleep 10)
    (set! other (call/cc other))
    (sleep 15)zz
    (set! other (call/cc other)))
\end{minted}
\end{frame}
	\begin{frame}[fragile]
		\frametitle{Delimited Continuations}
		Istnieje również wariant \texttt{call/cc} o bardziej lokalnym działaniu -- tzw ,,delimited continuations''.
		\pause
\begin{minted}{scheme}
(reset (* 2 (shift b (- 7 (b (* 3 4))))))
\end{minted}
\pause
\begin{minted}{scheme}
(reset (* 2 (shift b (- 7 (b 12)))))
(- 7 (* 2 12))
-17
\end{minted}
\pause
\begin{minted}{scheme}
(reset ((lambda (val) cont...) 
    (shift k expr...)))
(reset ((lambda (k) expr...) 
    (lambda (val) (reset cont...))))
\end{minted}
		\pause
		\texttt{reset} w tym przypadku rozdziela kontynuację \texttt{shift} od reszty programu -- stąd wynika ich nazwa. Warto zaznaczyć, że można zaimplementować ten rodzaj kontynuacji korzystając z \texttt{call/cc}.
\end{frame}
\begin{frame}[fragile]
	\frametitle{\texttt{catch/throw} jako Delimited Continuations}
Okazuje się, że jest wiele operacji które można zaimplementować jako delimited kontynuacje -- przykładem jest np. para \texttt{catch/throw}:
\begin{minted}{scheme}
(catch (lambda (x) x + 2)
    (+ 1 2 3 (throw 14) 5))
\end{minted}
\pause
Można zaimplementować te procedury np. przez \texttt{reset/shift}:
\vspace*{-0.3em}
\begin{minted}{scheme}
(define (catch handler body)
	(match (reset (body))
		[(cons 'thrown error) (handler error)]
		[val val]))

(define (throw value)
	(shift ignored
		(cons 'thrown value)))
\end{minted}
\end{frame}
\begin{frame}[fragile]
	\frametitle{Generatory przez Delimited Continuations}
	\begin{minted}[fontsize=\fontsize{10pt}{0pt}]{scheme}
(define (append value) (shift cont (cons x (cont '()))))
(reset ((lambda ()
    (append 1)
    (append 2)
    (append 3)
    '())))
\end{minted}		
\pause
Ogólniej:
\begin{minted}{scheme}
(define (yield value) (shift cont (pair value cont)))
\end{minted}
\end{frame}
\begin{frame}[fragile]
\frametitle{\texttt{dynamic-wind}}
Scheme udostępnia dodatkową funkcję przydatną do korzystania z kontynuacji: \texttt{dynamic-wind}.
\begin{minted}{scheme}
(dynamic-wind
	enter
	body
	leave)
\end{minted}
\pause
\begin{minted}{scheme}
(define inwind #f)
(dynamic-wind
 (lambda () (displayln "entry"))
 (lambda () (call/cc (lambda (cont) (set! inwind cont))))
 (lambda () (displayln "exit")))
\end{minted}

\end{frame}

	\section{\texttt{(call/cc (lambda (return) ...))} \\ ... czyli dygresja o monadach}
	\begin{frame}[fragile]
		\frametitle{Funkcje kontratakują}
		Zastanówmy się nad matematycznym obiektem funkcji:
		$$\exp: \mathbb{R} \ni x \mapsto e^x \in \mathbb{R}$$
		Zauważmy, że każdemu elementowi dziedziny odpowiada dokładnie jeden -- co więcej, w każdym momencie zachodzi $exp(x) = exp(x)$ -- wartość funkcji nie zależy od żadnego stanu poza jej argumentami.
		\pause
		
		Funkcję (procedurę) nazywamy czysto funkcyjną (ang. \textit{purely functional}) gdy:
		\begin{enumerate}
			\item<3-> Jej wynik wykonania wynosi tyle samo dla takich samych argumentów
			\item<4-> Nie wpływa na zewnętrzny stan programu -- nie ma ,,efektów ubocznych''
		\end{enumerate}
		\end{frame}
	\begin{frame}[fragile]
		\frametitle{Funkcje kontratakują}
		Funkcję (procedurę) nazywamy czysto funkcyjną (ang. \textit{purely functional}) gdy:
		\begin{enumerate}
			\item Jej wynik wykonania wynosi tyle samo dla takich samych argumentów
			\item Nie wpływa na zewnętrzny stan programu -- nie ma ,,efektów ubocznych''
		\end{enumerate}
			Operowanie tylko na takich funkcjach ma wiele zalet:
		\begin{enumerate}		
			\item<2-> Podczas ewaluacji możemy podstawić $f(x, y, z)$ za jego wartość bez martwienia się kolejnością ewaluacji
			\item<3-> Możemy nie wywoływać funkcji -- jeżeli nie jest to wymagane, możemy nie obliczać wartości funkcji.
			\item<4-> Możemy bardzo łatwo zrównoleglić wykonania funkcji -- brak zmian stanu implikuje brak problemów z synchronizacją
		\end{enumerate}
	\end{frame}
	\begin{frame}[fragile]
		\frametitle{Funkcje kontratakują}
		Oczywiście nie jest taka interpretacja bez wad -- główne z nich to:
		\begin{enumerate}
			\item<2-> Dla każdej zmiany stanu potrzebujemy go skopiować (nie możemy zmodyfikować wartości argumentu)
			\item<3-> Brak możliwości komunikacji z programem -- Input/Output nie spełnia założeń bycia czysto funkcyjnym, więc zamiast działającego komputera
			mamy grzejnik
		\end{enumerate}
		\onslide<4->{Nie będziemy przejmować się tymi problemami na tym wykładzie -- od tego momentu poprzez ,,funkcja'' mamy na myśli procedurę czysto funkcyjną.}
	\end{frame}
	\begin{frame}[fragile]
		\frametitle{Funkcje kontratakują}
		Załóżmy, że chcemy dodać do języka funkcję obliczającą odwrotność liczby $k$ w grupie $\mathbb{Z}_n$.
		Będzie to funkcja rodzaju \texttt{Int -> Int -> ...}. Jaki typ powinna zwrócić ta funkcja?

\pause
		Jeżeli zwrócimy \text{Int} to nastąpi problem gdy liczba nie jest względnie pierwsza z $n$ -- wtedy nie istnieje taka odwrotność.
\pause		

		Oczywiście moglibyśmy wykorzystać wcześniej wspomniane \texttt{catch/throw} -- jednak jako że chcemy, aby funkcja nie miała efektów ubocznych możemy podejść do tego problemu inaczej...
	\end{frame}
\begin{frame}[fragile]
\frametitle{Maybe/Optional}
Zdefiniujmy typ:
\vspace*{-0.3em}
\begin{minted}{haskell}
data Maybe a = Just a | Nothing
\end{minted}
\vspace*{-0.3em}
Nasz typ może posiadać dwa rodzaje wartości -- \texttt{Just a} oznaczający jakiś wynik lub \texttt{Nothing} oznaczający brak wartości.
Zauważmy, że możemy teraz zdefiniować naszą funkcję jako zwracającą typ Maybe zamiast zwykłego Inta:
\vspace*{-0.3em}
\begin{minted}{haskell}
inv a n = if gcd a n == 1
            then Just (calcInv a n)
            else Nothing
\end{minted}
\vspace*{-0.3em}
\pause

Ale co jeżeli chcemy coś zrobić z wynikiem funkcji -- np. dodać 2 -- mamy do wyboru dwie opcje:
\begin{itemize}
	\item Wyjść z kontekstu \texttt{Maybe}, przyjmując jakąś wartość domyślną gdy wynik pierwotnej funkcji to \texttt{Nothing}
	\item Pozostać w kontekście \texttt{Maybe}...
\end{itemize}
\end{frame}
\begin{frame}[fragile]
	\frametitle{Czym jest funktor?}
	Funktorem nazywamy typ danych parametryzowany jednym typem wraz z definiowaną funkcją
\begin{minted}{haskell}
map :: (a -> b) -> (Functor a -> Functor b)
\end{minted}
spełniającą dodatkowe dwa założenia:
\begin{enumerate}
	\item<2-> \mintinline{haskell}|map (\x -> x) x = x| -- identyczność jest zachowana
	\item<3-> \mintinline{haskell}|map f (map g x) = map (\a -> f (g a)) x| -- operacja jest łączna względem złożenia funkcji
\end{enumerate}
\pause
\pause
\pause
Dobrze znanym przykładem funktora jest lista wraz ze standardową operacją mapy po elementach.
\end{frame}
\begin{frame}[fragile]
\frametitle{Funktor Maybe}	
Dla typu \texttt{Maybe} możemy zdefiniować funktor w następujący sposób:
\begin{minted}{haskell}
map f Nothing = Nothing
map f (Just a) = Just (f a)
\end{minted}

Łatwo można potwierdzić, że powyższa definicja spełnia prawa funktorów. Rozwiązuje to wcześniej napotkany problem wychodzenia z kontekstu -- korzystając z \text{map} możemy obliczyć funkcję $f$ pozostając w kontekście typu \texttt{Maybe}: \mintinline{haskell}|f x = map (\x -> x + 2) (inv x)|.
\pause

Ale co jeżeli chcielibyśmy obliczyć odwrotność tej nowej liczby? Zauważmy, że aplikując ponownie \texttt{map} otrzymamy element typu \mintinline{haskell}|Maybe (Maybe x)|. Czy mamy jak pozbyć się jednej z warstw \texttt{Maybe}?
\end{frame}
\begin{frame}[fragile]
\frametitle{Czym jest monada?}
Monada to koncept często powtarzający się w programowaniu funkcyjnym, pozwalającym
opisywać standardowo stanowe operacje bez wykonywania ich efektów ubocznych.

\pause	
Formalniej, monadą nazywamy funktor dla którego zdefiniowane są dodatkowe operacje:
\begin{minted}{haskell}
unit :: a -> Monad a
join :: Monad (Monad a) -> Monad a
\end{minted}

\pause	
W moim przekonaniu najłatwiej myśleć o nich jako o kontekście nad którym możemy wykonywać obliczenia: 
wtedy \texttt{map} to dekorator na funkcji pozwalający jej pracować nad danym kontekstem, \texttt{unit} do nadanie wartości ,,domyślnego'' kontekstu, a ,,join'' pozwala na połączenie kontekstów dwóch wcześniej wykonanych operacji.
warstwy kontekstu.
	\end{frame}
	\begin{frame}[fragile]
		\frametitle{Monada Maybe}
		Wracając do \texttt{Maybe} możemy zdefiniować funkcję monadyczne w następujący sposób:
\begin{minted}{haskell}
map func (Just a) = Just (func a)
map Nothing = Nothing

unit value = Just value

join (Just val) = val
join Nothing = Nothing	
\end{minted}
\pause

\begin{minted}{haskell}
map (\x -> x + 2) (inv 2 7) == Just 6
map (\x -> x + 2) (inv 3 9) == Nothing
\end{minted}
	\end{frame}
	\begin{frame}[fragile]
		\frametitle{Prawa monad}
		Monady muszą spełniać następujące prawa:
		\begin{enumerate}
			\item<1-> \mintinline{haskell}|map (\a -> a) x == x| -- identyczność to el. neutralny \texttt{map}, przeniesione z funktora
			\item<2-> \mintinline{haskell}|map f (map g x) == map (\e -> f (g e)) x| -- łączność \texttt{map} względem siebie, jak w funktorze
			\item<3-> \mintinline{haskell}|join (unit x) == x| -- \texttt{unit} to el. neutralny \texttt{join}
			\item<4-> \mintinline{haskell}|join (map join x) == join (join x)| -- łączność \texttt{join} względem siebie
			\item<5-> \mintinline{haskell}|join (map (map f x)) == map f (join x)| -- relacja na \text{map} i \text{join}
		\end{enumerate}
	\end{frame}
	\begin{frame}[fragile]
		\frametitle{Monada -- równoważne definicje}
		W programowaniu często korzysta się z alternatywnej definicji monady, gdzie \texttt{join} zastąpione jest przez operator \verb|>>=| (tzw. bind).
		
		Operator ten o typie \texttt{Monad a -> (a -> Monad b) -> Monad b} można zdefiniować jako \mintinline{haskell}|monad >>= func = join (map func monad)|. Zachodzi wtedy \mintinline{haskell}|join m == (m >>= (\x -> x))|.
		Z wcześniej opisanych praw wynikają prawa o el. neutralnym i łączności \verb|>>=| -- w związku z tym jest on bardzo przydatny w programowaniu, ponieważ pozwala on ,,łączyć'' kolejne operacje w pewnym kontekście.
		
		\pause
		Jeszcze inną równoważną definicją jest operator ,,kompozycji'' 
		\hspace*{-1.5em}\mintinline{haskell}|(>=>) :: (a -> Monad b) -> (b -> Monad c) -> (a -> Monad c)| -- podczas gdy jest on również bardzo interesujący, nie będziemy się w niego zagłębiać.
				
	\end{frame}
	\begin{frame}[fragile]
		\frametitle{Either}
\begin{minted}{haskell}
data Either l r = Left l | Right r

map :: (a -> b) -> (Either l a -> Either l b)
map func (Right val) = Right (func val) 
map func (Left e) = (Left e)

unit value = Right value

join (Right value) = value
join (Left value) = Left value
\end{minted}
	\end{frame}
	\begin{frame}[fragile]
		\frametitle{List}
\begin{minted}{haskell}
data List x = Nil | Cons x (List x)

concat :: List x -> List x -> List x
concat Nil other = other
concat (Cons x rest) other = Cons x (concat rest other)

map :: (a -> b) -> (List a -> List b)
map func Nil = Nil
map func (Cons a rest) = Cons (func a) (map func rest)

join Nil = Nil
join (Cons list rest) = concat list (join rest)
\end{minted}
	\end{frame}
	\begin{frame}[fragile]
		\frametitle{Identity}
\begin{minted}{haskell}
data Identity a = Identity a
map func (Identity a) = Identity (f a)

unit a = Identity a

join (Identity (Identity a)) = Identity a
\end{minted}
	\end{frame}
	
	\section{\texttt{(return '())} \\ ... czyli co to ma do kontynuacji}
	\begin{frame}[fragile]
		\frametitle{Kontynuacja jako monada}
		Zastanowimy się, czy nie da się zdefiniować operacji dla funkcji przyjmujących kontynuacje \texttt{(a -> r) -> r} względem typu \texttt{a}.
		\pause
		Definicja \texttt{unit} wynika naturalnie z dostępnych nam wartości:
\begin{minted}{haskell}
unit :: a -> (a -> r) -> r
unit a = \cont -> cont a
\end{minted}
\pause
	Definicja \texttt{map} również przychodzi wraz z analizą dostępnych nam typów:
\begin{minted}{haskell}
map :: (a -> b) -> ((a -> r) -> r) -> ((b -> r) -> r)
map func ext = \cont -> ext (\val -> cont (func val))
\end{minted}
	Ostatnia definicja -- \texttt{join} -- również powstaje z rozumowania na typach:
\begin{minted}{haskell}
join :: (((a -> r) -> r) -> r) -> r
join cont = \c -> cont (\a -> a c)
\end{minted}
\end{frame}
	\begin{frame}[fragile]
		\frametitle{Kontynuacja jako \textbf{uniwersalna} monada}
		Łatwo można zweryfikować, że dane operacje spełniają prawa monad. Ciekawsze jest zachowanie operatora \verb|>>=|. Po rozpisaniu definicji otrzymujemy \mintinline{haskell}|val >>= fun = \cont -> val $ \res -> (fun res) cont|. Okazuje się, że mając ,,wartość'' w kontekście kontynuacji \texttt{(a -> r) -> r} i \texttt{a -> (b -> r) -> r}, to operator \verb|>>=| równoważny jest złożenia funkcji stylu CPS. 
		\pause
		
		W 1994 roku Andrzej Filinski wykazał, że każda monada o obliczalnych funkcjach może zostać zaimplementowana korzystając z monadu kontynuacji w języku z leniwą ewaluacją.	
	\end{frame}
	
	\begin{frame}[fragile]
		\frametitle{Maybe jako Kontynuacje}
\begin{minted}{haskell}
nothing :: (a -> Maybe r) -> Maybe r
nothing = (\x -> Nothing)

just :: a -> (a -> Maybe r) -> Maybe r
just a = (\c -> c a)
-- czyli just a = unit a
\end{minted}
\pause
\begin{minted}[fontsize=\fontsize{10pt}{0pt}]{haskell}
join (just nothing) == \c -> (\x -> x nothing) (\a -> a c) 
    == \c -> (\a -> a c) nothing == \c -> (nothing c) 
    == \c -> Nothing == nothing
join (nothing) == \c -> (\x -> Nothing) (\a -> a c) 
    == \c -> Nothing == nothing
join (just (just v)) == \c -> (\x -> x (\y -> y v)) (\a -> a c)
    == \c -> (\a -> a c) (\y -> y v) == \c -> (\y -> y v) c
    == \c -> (c v) = just v
\end{minted}
	\end{frame}

	\begin{frame}
		\frametitle{Kontynuacja tematu}
		\begin{itemize}
			\item \url{http://hjemmesider.diku.dk/~andrzej/papers/RM-abstract.html} -- oryginalna publikacja dotycząca monadów i kontynuacji
			\item \url{https://www.youtube.com/watch?v=TE48LsgVlIU} -- wykład o kontynuacjach, w szczególności o delimited continuations
			\item \url{https://wiki.haskell.org/All_About_Monads} -- fragment wiki Haskella opisujący najczęściej używane monady
		\end{itemize}
	\end{frame}
\end{document}
