gdritter repos gcct / master
Rudimentary proposal draft Getty Ritter 9 years ago
2 changed file(s) with 135 addition(s) and 0 deletion(s). Collapse all Expand all
+7
-0
proposal/Makefile less more
1 all: gcct.pdf
2
3 gcct.pdf: gcct.tex
4 pdflatex gcct.tex
5
6 clean:
7 rm -rf gcct.aux gcct.log gcct.pdf
+128
-0
proposal/gcct.tex less more
1 \documentclass[twocolumn]{scrartcl}
2 \usepackage[letterpaper]{geometry}
3 \usepackage{fullpage}
4 \usepackage{cmbright}
5 \usepackage{listings}
6 \usepackage{xcolor}
7 \usepackage{pgf}
8 \usepackage{tikz}
9 \usetikzlibrary{arrows,automata}
10 % \newcommand{\both}[2]{\begin{tabular}{ p{4in} p{4in} } #1 && #2 \\ \end{tabular}}
11
12 \lstset{ keywordstyle={\bfseries}
13 , keywordstyle=[2]\color{red}\bfseries
14 , keywordstyle=[3]\color{blue}\bfseries
15 , basicstyle=\scriptsize\ttfamily,
16 , morekeywords={where,let,in,instance,type},
17 , morekeywords=[2]{data,case,of}
18 , morekeywords=[3]{codata,merge}
19 }
20 \renewcommand{\ttdefault}{pcr}
21
22 \begin{document}
23 \section{GCCTs For The Layperson}
24
25 A GCCT is, to a first approximation, a kind of \textit{lazy record}.
26 It is \textit{lazy} because the fields it contains must be evaluated
27 only when they are accessed: this allows GCCTs to represent infinite
28 structures, even in a language in which all programs must terminate
29 such as Idris or Coq. It is a \textit{record} in the sense that the
30 only relevant way to manipulate a GCCT is through a set of
31 \textit{projections} or \textit{destructors}.
32
33 GCCTs differ from records in that some of their projections may
34 be restricted based on the type of the value from which they are
35 projecting, and that this restriction can be checked at compile-time.
36 For example, the following GCCT represents pairs of arbitrary values:
37
38 \begin{lstlisting}
39 codata Pair a b where
40 fst : Pair a b -> a
41 snd : Pair a b -> b
42 \end{lstlisting}
43
44 but here the same GCCT is extended with a third projection, which is
45 only available if the two projected values are of the same type and
46 permit equality:
47
48 \begin{lstlisting}
49 codata Pair' a b where
50 fst : Pair a b -> a
51 snd : Pair a b -> b
52 eqPair : (Eq a) => Pair a a -> Bool
53 \end{lstlisting}
54
55 This means that the following functions are well-typed:
56
57 \begin{lstlisting}
58 f : Pair' Int Bool -> Int
59 f x = fst x
60
61 g : Pair' Int Int -> Bool
62 g x = eqPair x
63 \end{lstlisting}
64
65 but the following would fail to even compile, because the \texttt{eqPair}
66 projection is not valid when the type arguments to \texttt{Pair'} are
67 non-identical:
68
69 \begin{lstlisting}
70 h : Pair' Int Bool -> Bool
71 h x = eqPair x
72 \end{lstlisting}
73
74 \section{Why GCCTs?}
75
76 Consider the task of writing a stateful server that has the following
77 behavior:
78
79 \begin{itemize}
80 \item Wait for a handshake
81 \item Accumulate a list of values of some type
82 \item Once the last one has arrived, perform some kind of processing
83 on the list of values and respond with a resulting value
84 \end{itemize}
85
86 We can diagram this using a simple state transition diagram:
87
88 { \centering
89 \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm,
90 semithick]
91 \tikzstyle{every state}=[fill=white,draw=black,text=black]
92 \node[state] (A) {Init};
93 \node[state] (B) [above right of=A] {Loop};
94 \node[state] (C) [below right of=B] {Done};
95
96 \path (A) edge node {handshake} (B)
97 (B) edge [loop above] node {add value} (B)
98 (B) edge node {finalize} (C)
99 (C) edge node {restart} (A);
100 \end{tikzpicture}
101 }
102
103 Using GCCTs, we can reify the state of the server into a single type
104 from which we can transition as well as examine the relevant available
105 values in a given state. More than that, the type system will ensure
106 that we cannot access those values outside of the state in which they are
107 relevant, and furthermore
108 that we cannot transition into an invalid state: we are limited to the
109 transitions we define.
110
111 \begin{lstlisting}
112 codata Server : State -> * -> * where
113 handshake : Server Init a -> Server Loop a
114
115 addValue : Server Loop a -> Server Loop a
116 accumulated : Server Loop a -> List a
117 finalize : Server Loop a -> Server Done a
118
119 finalValue : Server Done a -> a
120 restart : Server Done a -> Server Init a
121 \end{lstlisting}
122
123 This hints that GCCTs are a way of encoding complicated descriptions of
124 protocols in a way that allows static reasoning about the protocols.
125 GCCTs may prove to be a convenient way of representing session types or
126
127
128 \end{document}