Index: doc/generic_types/generic_types.tex
===================================================================
--- doc/generic_types/generic_types.tex	(revision 1c2c25378f0dba8478443afe179a6e47254093ed)
+++ doc/generic_types/generic_types.tex	(revision 06ccbc7c96f8bd0a8f66a7a54e38755a5299ee74)
@@ -42,5 +42,5 @@
 literate={-}{\raisebox{-0.15ex}{\texttt{-}}}1 {^}{\raisebox{0.6ex}{$\scriptscriptstyle\land\,$}}1
 	{~}{\raisebox{0.3ex}{$\scriptstyle\sim\,$}}1 {_}{\makebox[1.2ex][c]{\rule{1ex}{0.1ex}}}1 {`}{\ttfamily\upshape\hspace*{-0.1ex}`}1
-	{<-}{$\leftarrow$}2 {=>}{$\Rightarrow$}2,
+	{<-}{$\leftarrow$}2 {=>}{$\Rightarrow$}2 {->}{$\rightarrow$}2,
 % moredelim=**[is][\color{red}]{®}{®},					% red highlighting ®...® (registered trademark symbol) emacs: C-q M-.
 % moredelim=**[is][\color{blue}]{ß}{ß},					% blue highlighting ß...ß (sharp s symbol) emacs: C-q M-_
@@ -70,4 +70,28 @@
 }
 \email{a3moss@uwaterloo.ca}
+
+\author{Robert Schluntz}
+\affiliation{%
+	\institution{University of Waterloo}
+	\department{David R. Cheriton School of Computer Science}
+	\streetaddress{Davis Centre, University of Waterloo}
+	\city{Waterloo}
+	\state{ON}
+	\postcode{N2L 3G1}
+	\country{Canada}
+}
+\email{rschlunt@uwaterloo.ca}
+
+\author{Peter Buhr}
+\affiliation{%
+	\institution{University of Waterloo}
+	\department{David R. Cheriton School of Computer Science}
+	\streetaddress{Davis Centre, University of Waterloo}
+	\city{Waterloo}
+	\state{ON}
+	\postcode{N2L 3G1}
+	\country{Canada}
+}
+\email{pabuhr@uwaterloo.ca}
 
 \terms{generic, types}
@@ -115,5 +139,5 @@
 \begin{lstlisting}
 forall(otype T)
-T identity(T x) {
+T identity(T x) {is_
     return x;
 }
@@ -121,5 +145,7 @@
 int forty_two = identity(42); // T is bound to int, forty_two == 42
 \end{lstlisting}
-The @identity@ function above can be applied to any complete object type (or ``@otype@''). The type variable @T@ is transformed into a set of additional implicit parameters to @identity@, which encode sufficient information about @T@ to create and return a variable of that type. The \CFA{} implementation passes the size and alignment of the type represented by an @otype@ parameter, as well as an assignment operator, constructor, copy constructor and destructor. Here, the runtime cost of polymorphism is spread over each polymorphic call, due to passing more arguments to polymorphic functions; preliminary experiments have shown this overhead to be similar to \CC{} virtual function calls. 
+The @identity@ function above can be applied to any complete object type (or ``@otype@''). The type variable @T@ is transformed into a set of additional implicit parameters to @identity@, which encode sufficient information about @T@ to create and return a variable of that type. The \CFA{} implementation passes the size and alignment of the type represented by an @otype@ parameter, as well as an assignment operator, constructor, copy constructor and destructor. If this extra information is not needed, the type parameter can be declared as @dtype T@, where @dtype@ is short for ``data type''.
+
+Here, the runtime cost of polymorphism is spread over each polymorphic call, due to passing more arguments to polymorphic functions; preliminary experiments have shown this overhead to be similar to \CC{} virtual function calls. An advantage of this design is that, unlike \CC{} template functions, \CFA{} @forall@ functions are compatible with separate compilation.
 
 Since bare polymorphic types do not provide a great range of available operations, \CFA{} provides a \emph{type assertion} mechanism to provide further information about a type:
@@ -166,4 +192,15 @@
 \end{lstlisting}
 
+@otype@ is essentially syntactic sugar for the following trait:
+\begin{lstlisting}
+trait otype(dtype T | sized(T)) {
+	// sized is a compiler-provided pseudo-trait for types with known size & alignment
+	void ?{}(T*);  // default constructor
+	void ?{}(T*, T);  // copy constructor
+	T ?=?(T*, T);  // assignment operator
+	void ^?{}(T*);  // destructor
+};
+\end{lstlisting}
+
 Semantically, traits are simply a named lists of type assertions, but they may be used for many of the same purposes that interfaces in Java or abstract base classes in \CC{} are used for. Unlike Java interfaces or \CC{} base classes, \CFA{} types do not explicitly state any inheritance relationship to traits they satisfy; this can be considered a form of structural inheritance, similar to implementation of an interface in Go, as opposed to the nominal inheritance model of Java and \CC{}. Nominal inheritance can be simulated with traits using marker variables or functions:
 \begin{lstlisting}
@@ -200,4 +237,77 @@
 While a nominal-inheritance system with associated types could model one of those two relationships by making @El@ an associated type of @Ptr@ in the @pointer_like@ implementation, few such systems could model both relationships simultaneously.
 
+\section{Generic Types}
+
+The generic types design for \CFA{} must integrate efficiently and naturally with the existing polymorphic functions in \CFA{}, while retaining backwards compatibility with C; maintaining separate compilation is a particularly important constraint on the design. However, where the concrete parameters of the generic type are known, there should not be extra overhead for the use of a generic type.
+
+A generic type can be declared by placing a @forall@ specifier on a @struct@ or @union@ declaration, and instantiated using a parenthesized list of types after the type name:
+\begin{lstlisting}
+forall(otype R, otype S) struct pair {
+    R first;
+    S second;
+};
+
+forall(otype T)
+T value( pair(const char*, T) *p ) { return p->second; }
+
+forall(dtype F, otype T)
+T value_p( pair(F*, T*) p ) { return *p.second; }
+
+pair(const char*, int) p = { "magic", 42 };
+int magic = value( &p );
+
+pair(void*, int*) q = { 0, &p.second };
+magic = value_p( q );
+double d = 1.0;
+pair(double*, double*) r = { &d, &d };
+d = value_p( r );
+\end{lstlisting}
+
+\CFA{} classifies generic types as either \emph{concrete} or \emph{dynamic}. Dynamic generic types vary in their in-memory layout depending on their type parameters, while concrete generic types have a fixed memory layout regardless of type parameters. A type may have polymorphic parameters but still be concrete; \CFA{} refers to such types as \emph{dtype-static}. Polymorphic pointers are an example of dtype-static types -- @forall(dtype T) T*@ is a polymorphic type, but for any @T@ chosen, @T*@ will have exactly the same in-memory representation as a @void*@, and can therefore be represented by a @void*@ in code generation.
+
+The \CFA{} compiler instantiates concrete generic types by template-expanding them to fresh struct types; concrete generic types can therefore be used with zero runtime overhead. To enable interoperation between equivalent instantiations of a generic type, the compiler saves the set of instantiations currently in scope and re-uses the generated struct declarations where appropriate. As an example, the concrete instantiation for @pair(const char*, int)@ would look something like this:
+\begin{lstlisting}
+struct _pair_conc1 {
+	const char* first;
+	int second;
+};
+\end{lstlisting}
+
+A concrete generic type with dtype-static parameters is also expanded to a struct type, but this struct type is used for all matching instantiations. In the example above, the @pair(F*, T*)@ parameter to @value_p@ is such a type; its expansion would look something like this, and be used as the type of the variables @q@ and @r@ as well, with casts for member access where appropriate:
+\begin{lstlisting}
+struct _pair_conc0 {
+	void* first;
+	void* second;
+};
+\end{lstlisting}
+
+\TODO{} Maybe move this after the rest of the discussion.
+This re-use of dtype-static struct instantiations enables some useful programming patterns at zero runtime cost. The most important such pattern is using @forall(dtype T) T*@ as a type-checked replacement for @void*@, as in this example, which takes a @qsort@ or @bsearch@-compatible comparison routine and creates a similar lexicographic comparison for pairs of pointers:
+\begin{lstlisting}
+forall(dtype T)
+int lexcmp( pair(T*, T*)* a, pair(T*, T*)* b, int (*cmp)(T*, T*) ) {
+	int c = cmp(a->first, b->first);
+	if ( c == 0 ) c = cmp(a->second, b->second);
+	return c;
+}
+\end{lstlisting}
+Since @pair(T*, T*)@ is a concrete type, there are no added implicit parameters to @lexcmp@, so the code generated by \CFA{} will be effectively identical to a version of this written in standard C using @void*@, yet the \CFA{} version will be type-checked to ensure that the fields of both pairs and the arguments to the comparison function match in type.
+
+\TODO{} The second is zero-cost ``tag'' structs.
+
+\section{Tuples}
+
+\TODO{} Integrate Rob's work
+
+\TODO{} Check if we actually can use ttype parameters on generic types (if they set the complete flag, it should work, or nearly so).
+
+\section{Related Work}
+
+\TODO{} Talk about \CC{}, Cyclone, \etc{}
+
+\section{Conclusion}
+
+\TODO{}
+
 \bibliographystyle{ACM-Reference-Format}
 \bibliography{generic_types}