\documentclass{scrartcl}
\usepackage[letterpaper]{geometry}
\usepackage{fullpage}
\usepackage{cmbright}
\usepackage[usenames,dvipsnames]{color}
\usepackage{listings}
% \newcommand{\both}[2]{\begin{tabular}{ p{4in} p{4in} } #1 && #2 \\ \end{tabular}}
\newcommand{\pos}[1]{\textcolor{BrickRed}{#1}}
\newcommand{\postt}[1]{\textcolor{BrickRed}{\texttt{#1}}}
\newcommand{\dual}[1]{\textcolor{NavyBlue}{#1}}
\newcommand{\dualtt}[1]{\textcolor{NavyBlue}{\texttt{#1}}}
\newenvironment{both}
  { \begin{tabular}{ p{3in}  p{3in} } }
  { \\ \end{tabular} }

\renewcommand{\ttdefault}{pcr}
\lstset{basicstyle=\ttfamily,columns=flexible,language=[LaTeX]TeX,%
        texcl,%set comments in an extra line
        mathescape=false,escapechar=|,
literate={data}{\bfseries\textcolor{BrickRed}{data }}1
         {codata}{\bfseries\textcolor{NavyBlue}{data }}1
         {record}{\bfseries\textcolor{NavyBlue}{record }}1
         {case}{\bfseries\textcolor{BrickRed}{case }}1
         {of}{\bfseries\textcolor{BrickRed}{of }}1
         {merge}{\bfseries\textcolor{NavyBlue}{merge }}1
         {from}{\bfseries\textcolor{NavyBlue}{from }}1
         {if}{\bfseries{if }}1
         {then}{\bfseries{then }}1
         {else}{\bfseries{else }}1
         {assert}{\bfseries{assert }}1
         {<+>}{{+ }}1
         {+}{\textcolor{BrickRed}{+ }}1
         {*}{\textcolor{NavyBlue}{* }}1
         {<pos>}{\color{BrickRed}}1
         {</pos>}{\normalcolor}1
         {<dual>}{\color{NavyBlue}}1
         {</dual>}{\normalcolor}1
         ,%
         texcsstyle=*\color{blue!70}\bfseries,
         texcs={end,begin,documentclass}
}
\begin{document}
\section{\pos{Data} and \dual{Codata}}

\begin{both}
    \pos{Data} is defined by its \pos{introduction} rules.
  & \dual{Codata} is defined by its \dual{elimination} rules.
\\
    We can define a \pos{data} type with
  & We can define a \dual{codata} type with
\\
  \begin{lstlisting}
  data <pos>Either</pos> a b
    = Left  a
    + Right b
  \end{lstlisting}
  &
  \begin{lstlisting}
  codata <dual>Both</dual> a b
    = first  a
    * second b
  \end{lstlisting}
\\
    This definition will effectively introduce two functions:
  & This definition will effectively introduce two functions:
\\
  \begin{lstlisting}
  Left  : a -> <pos>Either</pos> a b
  Right : b -> <pos>Either</pos> a b
  \end{lstlisting}
&
  \begin{lstlisting}
  first  : <dual>Both</dual> a b -> a
  second : <dual>Both</dual> a b -> b
  \end{lstlisting}
\\
    In order to \pos{destruct data} we have to use
    \pos{patterns} which let you match on \pos{constructors}.
  & In order to \dual{construct codata} we have to use
    \dual{copatterns} which let you match on \dual{destructors}.
\\
  \begin{lstlisting}
  case e of
     Left  x -> e1
     Right y -> e2
  \end{lstlisting}
&
  \begin{lstlisting}
  merge x from
     first  x <- e1
     second x <- e2
  \end{lstlisting}
\\
    Here, \postt{e} represents the \pos{value being
    destructed}, and each branch represents a \pos{constructor
    with which it might have been constructed}. We are effectively
    \pos{dispatching on possible pasts} of
    \postt{e}.
  & Here, \dual{\texttt{x}} represents the \dual{value being
    constructed}, and each branch represents a \dual{destructor
    with which it might eventually be destructed}. We are effectively
    \dual{dispatching on possible futures} of
    \dualtt{x}.
\\
\end{both}

\section{Codata, Records, and Copatterns}
\raggedright

In the same way that named sums are a natural way to represent data,
records are a natural way to represent codata. In lieu of the above
syntax, one often sees codata represented as something more like

\begin{lstlisting}
record <dual>Both</dual> a b = <dual>{</dual> .first : a, .second : b <dual>}</dual>

x : <dual>Both</dual> Int Bool
x = <dual>{</dual> .first = 2, .second = true <dual>}</dual>

assert x.first == 2
assert x.second == true
\end{lstlisting}

The \dualtt{merge} syntax is used here for conceptual
symmetry with \postt{case}. Additionally, the use of
copatterns is nicely dual with the extra expressivity that
patterns offer. For example, we can use nested patterns with
constructors of various types, as in this function which
processes a list of \postt{Either Int Bool} values
by summing the integers in the list until it reaches a
\postt{false} value or the end of the list:

\begin{lstlisting}
f : List (Either Int Bool) -> Int
f lst = case lst of
  Cons (Left i) xs  -> i <+> f xs
  Cons (Right b) xs -> if b then f xs else 0
  Nil               -> 0
\end{lstlisting}

Similarly, we can define an infinite stream of pairs using
nested copatterns as so:

\begin{lstlisting}
s : Int -> Stream (Both Int Bool)
s n = merge x from
  first (head x)  <- n
  second (head x) <- n > 0
  tail x          <- x
\end{lstlisting}

Copatterns are also practically expressive, as in this concise
and readable definition of the fibonacci numbers in terms of
the \dualtt{merge} expression:

\begin{lstlisting}
codata Stream a
  = head a
  * tail (Stream a)

zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c
zipWith f s1 s2 = merge x from
  head x <- f (head s1) (head s2)
  tail x <- zipWith f (tail s1) (tail s2)

fibs : Stream Int
fibs = merge x from
  head x        <- 0
  head (tail x) <- 1
  tail (tail x) <- zipWith (<+>) x (tail x)
\end{lstlisting}

\section{Row-Typed \dual{Co}data}

\begin{both}
    It is possible to build an \pos{open sum} by a small
    modification of the datatype mechanism. Instead of
    naming types and listing their associated
    \pos{constructors}, we represent a type as a
    \pos{list of constructors and types}.
  &
    It is possible to build an \dual{open product} by a small
    modification of the datatype mechanism. Instead of
    naming types and listing their associated
    \dual{destructors}, we represent a type as a
    \dual{list of destructors and types}.
\\
  {\color{BrickRed}
\begin{verbatim}
{- .. -} : [ Left: a + Right: b ]
\end{verbatim}
  }
  &
  {\color{NavyBlue}
\begin{verbatim}
{- .. -} : { first: a * second: b }
\end{verbatim}
  }
\\
    Use of a \pos{constructor} no longer specifies a
    specific type, but rather \pos{any type that can be
    constructed with that constructor}.
  &
    Use of a \dual{destructor} no longer specifies a
    specific type, but rather \dual{any type that can be
    destructed with that destructor}.
\\
\begin{lstlisting}
Left  : a -> <pos>[</pos> Left: a + ... <pos>]</pos>
Right : b -> <pos>[</pos> Right: b + ... <pos>]</pos>
\end{lstlisting}
  &
\begin{lstlisting}
first  : <dual>{</dual> first: a * ... <dual>}</dual> -> a
second : <dual>{</dual> second: b * ... <dual>}</dual> -> b
\end{lstlisting}
\\
    If we want to \pos{destruct} an open value like this, we
    can use a \postt{case} construct, as before.
  &
    If we want to \dual{construct} an open value like this, we
    can use a \dualtt{merge} construct, as before.
\\
  {\color{BrickRed}
\begin{verbatim}
f : [ Left Int + Right Bool ] -> Int
f e = case e of
        Left  i -> i
        Right b -> if b then 1 else 0
\end{verbatim}
  }
  &
  {\color{NavyBlue}
\begin{verbatim}
f : Int -> { First Int * Second Bool }
f i = merge x from
        first  x <- i
        second x <- i == 0
\end{verbatim}
}
\end{both}
\end{document}