\documentclass[twocolumn]{scrartcl}
\usepackage[letterpaper]{geometry}
\usepackage{fullpage}
\usepackage{cmbright}
\usepackage{listings}
\usepackage{xcolor}
\usepackage{pgf}
\usepackage{tikz}
\usetikzlibrary{arrows,automata}
% \newcommand{\both}[2]{\begin{tabular}{ p{4in} p{4in} } #1 && #2 \\ \end{tabular}}

\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}
       }
\renewcommand{\ttdefault}{pcr}

\begin{document}
\section{GCCTs For The Layperson}

A GCCT is, to a first approximation, a kind of \textit{lazy record}.
It is \textit{lazy} because the fields it contains must be evaluated
only when they are accessed: this allows GCCTs to represent infinite
structures, even in a language in which all programs must terminate
such as Idris or Coq. It is a \textit{record} in the sense that the
only relevant way to manipulate a GCCT is through a set of
\textit{projections} or \textit{destructors}.

GCCTs differ from records in that some of their projections may
be restricted based on the type of the value from which they are
projecting, and that this restriction can be checked at compile-time.
For example, the following GCCT represents pairs of arbitrary values:

\begin{lstlisting}
codata Pair a b where
  fst : Pair a b -> a
  snd : Pair a b -> b
\end{lstlisting}

but here the same GCCT is extended with a third projection, which is
only available if the two projected values are of the same type and
permit equality:

\begin{lstlisting}
codata Pair' a b where
  fst    :           Pair a b -> a
  snd    :           Pair a b -> b
  eqPair : (Eq a) => Pair a a -> Bool
\end{lstlisting}

This means that the following functions are well-typed:

\begin{lstlisting}
f : Pair' Int Bool -> Int
f x = fst x

g : Pair' Int Int -> Bool
g x = eqPair x
\end{lstlisting}

but the following would fail to even compile, because the \texttt{eqPair}
projection is not valid when the type arguments to \texttt{Pair'} are
non-identical:

\begin{lstlisting}
h : Pair' Int Bool -> Bool
h x = eqPair x
\end{lstlisting}

\section{Why GCCTs?}

Consider the task of writing a stateful server that has the following
behavior:

\begin{itemize}
\item Wait for a handshake
\item Accumulate a list of values of some type
\item Once the last one has arrived, perform some kind of processing
  on the list of values and respond with a resulting value
\end{itemize}

We can diagram this using a simple state transition diagram:

{ \centering
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm,
                    semithick]
  \tikzstyle{every state}=[fill=white,draw=black,text=black]
  \node[state] (A) {Init};
  \node[state] (B) [above right of=A] {Loop};
  \node[state] (C) [below right of=B] {Done};

  \path (A) edge node {handshake} (B)
        (B) edge [loop above] node {add value} (B)
        (B) edge node {finalize} (C)
        (C) edge node {restart} (A);
\end{tikzpicture}
}

Using GCCTs, we can reify the state of the server into a single type
from which we can transition as well as examine the relevant available
values in a given state. More than that, the type system will ensure
that we cannot access those values outside of the state in which they are
relevant, and furthermore
that we cannot transition into an invalid state: we are limited to the
transitions we define.

\begin{lstlisting}
codata Server : State -> * -> * where
  handshake : Server Init a -> Server Loop a

  addValue    : Server Loop a -> Server Loop a
  accumulated : Server Loop a -> List a
  finalize    : Server Loop a -> Server Done a

  finalValue : Server Done a -> a
  restart    : Server Done a -> Server Init a
\end{lstlisting}

This hints that GCCTs are a way of encoding complicated descriptions of
protocols in a way that allows static reasoning about the protocols.
GCCTs may prove to be a convenient way of representing session types or


\end{document}