\documentclass{beamer}
\usepackage{cmbright}
% \usepackage[usenames,dvipsnames]{color}
\usepackage{listings}
\usepackage{xcolor}
\newcommand{\pos}[1]{\textcolor{red}{#1}}
\newcommand{\postt}[1]{\textcolor{red}{\texttt{#1}}}
\newcommand{\dual}[1]{\textcolor{blue}{#1}}
\newcommand{\dualtt}[1]{\textcolor{blue}{\texttt{#1}}}

\lstset{ keywordstyle={\bfseries}
       , keywordstyle=[2]\color{red}\bfseries
       , keywordstyle=[3]\color{blue}\bfseries
       , basicstyle=\scriptsize\ttfamily,
       , morekeywords={where,let,in,instance,type},
       , morekeywords=[2]{data,case,of}
       , morekeywords=[3]{codata,merge}
       }

\newenvironment{both}
  { \begin{tabular}{ p{2in}  p{2in} } }
  { \\ \end{tabular} }
\renewcommand{\ttdefault}{pcr}

\title{Generalized Coalgebraic Codata Types}
\subtitle{Excessive Amounts of Duality}
\author{G.~Ritter \and K.~Foner}
\date{\today}
\subject{Computer Science}

\begin{document}

\frame{\titlepage}

\begin{frame}[fragile]
\frametitle{Data and Codata: An Introduction}
\begin{both}
\begin{lstlisting}
-------------------
-- Defining data --

data Either a b
  = Left  a
  | Right b

-----------------------
-- Constructing data --

Left  : a -> Either a b
Right : b -> Either a b

----------------------
-- Destructing data --

f : Either Int Bool -> Bool
f x = case x of
        Left i  -> i == 0
        Right b -> b
\end{lstlisting}
&
\begin{lstlisting}
---------------------
-- Defining codata --

codata Both a b
  = First  a
  & Second b

------------------------
-- Destructing codata --

First  : Both a b -> a
Second : Both a b -> b

-------------------------
-- Constructing codata --

g : Int -> Both Int Bool
g x = merge
        First  p <- x
        Second p <- x == 0
\end{lstlisting}
\\
\end{both}
\end{frame}

\begin{frame}[fragile]
\frametitle{Copatterns}
\begin{lstlisting}[basicstyle=\normalsize\ttfamily]
codata Stream a = Head a & Tail (Stream a)

zipWith : (a -> b -> c) -> Stream a ->
            Stream b -> Stream c
Head (zipWith f s1 s2) =
    f (Head s1) (Head s2)
Tail (zipWith f s1 s2) =
    zipWith f (Tail s1) (Tail s2)

fibs : Stream Int
Head fibs        = 0
Head (Tail fibs) = 1
Tail (fibsTail@(Tail fibs)) =
    zipWith (+) fibs fibsTail
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Copatterns}
\begin{lstlisting}[basicstyle=\normalsize\ttfamily]
codata Stream a = Head a & Tail (Stream a)

zipWith : (a -> b -> c) -> Stream a ->
            Stream b -> Stream c
Head (zipWith f s1 s2) =
    f (Head s1) (Head s2)
Tail (zipWith f s1 s2) =
    zipWith f (Tail s1) (Tail s2)

merge
  Head _                      = 0
  Head (Tail _)               = 1
  Tail (fibsTail@(Tail fibs)) =
    zipWith (+) fibs fibsTail
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Generalizing Types}
\begin{both}
\begin{lstlisting}
data T: * -> * where
  U : Int       -> T Int
  X : (T a,T a) -> T (a,a)

--

U : Int -> T Int
X : (T a,T a) -> T (a,a)

--

sum : T a -> Int
sum x = case x of
  U i      -> i
  X (a, b) -> sum a + sum b
\end{lstlisting}
&
\begin{lstlisting}
codata T': * -> * where
  U' : T' Int   -> Int
  X' : T' (a,a) -> (T' a,T' a)

--

U' : T' Int -> Int
X' : T' (a,a) -> (T' a,T' a)

--

split : Int -> T' a
split i = merge
  U' _ <- i
  X' _ <- ( split 1
          , split (i-1)
          )
\end{lstlisting}
\end{both}
\end{frame}

\begin{frame}[fragile]
\frametitle{GCCTs}
\begin{lstlisting}[basicstyle=\normalsize\ttfamily]
codata Wrapper: * -> * where
  G : Wrapper a   -> a
  Z : Wrapper Int -> Bool

mkBoolWrapper : Bool -> Wrapper Bool
G (mkBoolWrapper b) = b

mkIntWrapper : Int -> Wrapper Int
G (mkIntWrapper i) = i
Z (mkIntWrapper i) = i == 0

mkWrapper : a -> Wrapper a
G (mkWrapper x) = x
Z (mkWrapper x) = x == 0
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{NFA}
\begin{lstlisting}[basicstyle=\normalsize\ttfamily]
data S = A | B | C

codata FSA: S -> * where
  aToB : FSA A -> FSA B
  bToC : FSA B -> FSA C
  aToC : FSA A -> FSA C
  cToA : FSA C -> FSA A

aState : FSA A
aState = merge
  cToA (aToC a)        <- a
  cToA (bToC (aToB a)) <- a

cToA . bToC . aToB == id
cToA . aToB -- fails to type-check
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{NFA}
\begin{lstlisting}[basicstyle=\normalsize\ttfamily]
codata FSA: S -> * where
  aToB : FSA A -> FSA B
  bToC : FSA B -> FSA C
  aToC : FSA A -> FSA C
  cToA : FSA C -> FSA A
  matchedString : FSA A -> String

aState : FSA A
aState =
  let f str = merge
    cToA (aToC _)        <- f (str ++ "ca")
    cToA (bToC (aToB _)) <- f (str ++ "bca")
    matchedString _      <- str
  in f "a"
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{NFA}
\begin{lstlisting}[basicstyle=\normalsize\ttfamily]
codata FSA: S -> * where
  aToB : FSA A -> FSA B
  bToC : FSA B -> FSA C
  aToC : FSA A -> FSA C
  cToA : FSA C -> FSA A
  matchedString : FSA _ -> String

aState : FSA A
aState =
  let f str = merge
    cToA (aToC _)        <- f (str ++ "ca")
    cToA (bToC (aToB _)) <- f (str ++ "bca")
    matchedString _      <- str
    matchedString (aToB _) <- str ++ "b"
    matchedString (aToC _) <- str ++ "c"
    matchedString (bToC (aToB _)) <- str ++ "bc"
  in f "a"
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Operational}
\begin{lstlisting}[basicstyle=\normalsize\ttfamily]
data Oper : (* -> *) -> * -> * where
  Return : a -> Oper t a
  Bind   : t a -> (a -> Oper t b) -> Oper t b

instance Monad (Oper t) where
  return = Return
  Return x >>= g = g x
  Bind x f >>= g = Bind x (f >=> g)
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Co-operational}
\begin{lstlisting}[basicstyle=\normalsize\ttfamily]
codata Coop : (* -> *) -> * -> * where
  Extract : Coop t a -> a
  Extend  : Coop t a -> (Coop t a -> b) -> t b

instance Comonad (Coop t) where
  extract = Extract
  Extract (x <<= f)   = f x
  Extend  (x <<= f) g =
    Extend x (f =>= g)
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Co-operational}
\begin{lstlisting}[basicstyle=\normalsize\ttfamily]
codata Op : * -> * where
  Pop  : Op (a, b) -> a
  Drop : Op (a, b) -> Op b

type Stack a = Coop Op a

push : a -> Stack b -> Stack (a, b)
push x s = s <<= go
  where go y = (x, extract y)

dup : Stack (a, b) -> Stack (a, (a, b))
dup s = s <<= go
  where go y = (fst (extract y), extract y)
\end{lstlisting}
\end{frame}

\end{document}
