Index: doc/proposals/ctordtor/Makefile
===================================================================
--- doc/proposals/ctordtor/Makefile	(revision 981bdc611ba9967f6a7ef2dec163e17a63effb7d)
+++ doc/proposals/ctordtor/Makefile	(revision 981bdc611ba9967f6a7ef2dec163e17a63effb7d)
@@ -0,0 +1,81 @@
+## Define the appropriate configuration variables.
+
+MACROS = ../../LaTeXmacros
+BIB = ../../bibliography
+
+TeXLIB = .:$(MACROS):$(MACROS)/listings:$(MACROS)/enumitem:$(BIB)/:
+LaTeX  = TEXINPUTS=${TeXLIB} && export TEXINPUTS && latex -halt-on-error
+BibTeX = BIBINPUTS=${TeXLIB} && export BIBINPUTS && bibtex
+
+## Define the text source files.
+
+SOURCES = ${addsuffix .tex, \
+ctor \
+}
+
+FIGURES = ${addsuffix .tex, \
+}
+
+PICTURES = ${addsuffix .pstex, \
+}
+
+PROGRAMS = ${addsuffix .tex, \
+}
+
+GRAPHS = ${addsuffix .tex, \
+}
+
+## Define the documents that need to be made.
+
+DOCUMENT = ctor.pdf
+
+# Directives #
+
+all : ${DOCUMENT}
+
+clean :
+	rm -f *.bbl *.aux *.dvi *.idx *.ilg *.ind *.brf *.out *.log *.toc *.blg *.pstex_t *.cf \
+		${FIGURES} ${PICTURES} ${PROGRAMS} ${GRAPHS} ${basename ${DOCUMENT}}.ps ${DOCUMENT}
+
+# File Dependencies #
+
+${DOCUMENT} : ${basename ${DOCUMENT}}.ps
+	ps2pdf $<
+
+${basename ${DOCUMENT}}.ps : ${basename ${DOCUMENT}}.dvi
+	dvips $< -o $@
+
+${basename ${DOCUMENT}}.dvi : Makefile ${GRAPHS} ${PROGRAMS} ${PICTURES} ${FIGURES} ${SOURCES} ${basename ${DOCUMENT}}.tex \
+		$(MACROS)/common.tex $(MACROS)/indexstyle $(BIB)/cfa.bib
+	# Conditionally create an empty *.ind (index) file for inclusion until makeindex is run.
+	if [ ! -r ${basename $@}.ind ] ; then touch ${basename $@}.ind ; fi
+	# Must have *.aux file containing citations for bibtex
+	if [ ! -r ${basename $@}.aux ] ; then ${LaTeX} ${basename $@}.tex ; fi
+	-${BibTeX} ${basename $@}
+	# Some citations reference others so run steps again to resolve these citations
+	${LaTeX} ${basename $@}.tex
+	-${BibTeX} ${basename $@}
+	# Make index from *.aux entries and input index at end of document
+	makeindex -s $(MACROS)/indexstyle ${basename $@}.idx
+	${LaTeX} ${basename $@}.tex
+	# Run again to get index title into table of contents
+	${LaTeX} ${basename $@}.tex
+
+predefined :
+	sed -f predefined.sed ${basename ${DOCUMENT}}.tex > ${basename $@}.cf
+
+## Define the default recipes.
+
+%.tex : %.fig
+	fig2dev -L eepic $< > $@
+
+%.ps : %.fig
+	fig2dev -L ps $< > $@
+
+%.pstex : %.fig
+	fig2dev -L pstex $< > $@
+	fig2dev -L pstex_t -p $@ $< > $@_t
+
+# Local Variables: #
+# compile-command: "make" #
+# End: #
Index: doc/proposals/ctordtor/ctor.tex
===================================================================
--- doc/proposals/ctordtor/ctor.tex	(revision 981bdc611ba9967f6a7ef2dec163e17a63effb7d)
+++ doc/proposals/ctordtor/ctor.tex	(revision 981bdc611ba9967f6a7ef2dec163e17a63effb7d)
@@ -0,0 +1,330 @@
+% inline code ©...© (copyright symbol) emacs: C-q M-)
+% red highlighting ®...® (registered trademark symbol) emacs: C-q M-.
+% blue highlighting ß...ß (sharp s symbol) emacs: C-q M-_
+% green highlighting ¢...¢ (cent symbol) emacs: C-q M-"
+% LaTex escape §...§ (section symbol) emacs: C-q M-'
+% keyword escape ¶...¶ (pilcrow symbol) emacs: C-q M-^
+% math escape $...$ (dollar symbol)
+
+\documentclass[twoside,11pt]{article}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Latex packages used in the document (copied from CFA user manual).
+\usepackage[T1]{fontenc}                                % allow Latin1 (extended ASCII) characters
+\usepackage{textcomp}
+\usepackage[latin1]{inputenc}
+\usepackage{fullpage,times,comment}
+\usepackage{epic,eepic}
+\usepackage{upquote}									% switch curled `'" to straight
+\usepackage{calc}
+\usepackage{xspace}
+\usepackage{graphicx}
+\usepackage{varioref}									% extended references
+\usepackage{listings}									% format program code
+\usepackage[flushmargin]{footmisc}						% support label/reference in footnote
+\usepackage{latexsym}                                   % \Box glyph
+\usepackage{mathptmx}                                   % better math font with "times"
+\usepackage[usenames]{color}
+\usepackage[pagewise]{lineno}
+\renewcommand{\linenumberfont}{\scriptsize\sffamily}
+\input{common}                                          % bespoke macros used in the document
+\usepackage[dvips,plainpages=false,pdfpagelabels,pdfpagemode=UseNone,colorlinks=true,pagebackref=true,linkcolor=blue,citecolor=blue,urlcolor=blue,pagebackref=true,breaklinks=true]{hyperref}
+\usepackage{breakurl}
+\renewcommand{\UrlFont}{\small\sf}
+
+\setlength{\topmargin}{-0.45in}							% move running title into header
+\setlength{\headsep}{0.25in}
+
+\usepackage{caption}
+\usepackage{subcaption}
+\usepackage{bigfoot}
+\usepackage{amsmath}
+
+\interfootnotelinepenalty=10000
+
+\title{
+\Huge \vspace*{1in} Constructors and Destructors in \CFA \\
+\vspace*{1in}
+}
+
+\author{
+\huge Rob Schluntz \\
+\Large \vspace*{0.1in} \texttt{rschlunt@uwaterloo.ca} \\
+\Large Cheriton School of Computer Science \\
+\Large University of Waterloo
+}
+
+\date{
+\today
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\bigO}[1]{O\!\left( #1 \right)}
+
+\begin{document}
+\pagestyle{headings}
+% changed after setting pagestyle
+\renewcommand{\sectionmark}[1]{\markboth{\thesection\quad #1}{\thesection\quad #1}}
+\renewcommand{\subsectionmark}[1]{\markboth{\thesubsection\quad #1}{\thesubsection\quad #1}}
+\pagenumbering{roman}
+% \linenumbers                                            % comment out to turn off line numbering
+
+\maketitle
+\thispagestyle{empty}
+
+\clearpage
+\thispagestyle{plain}
+\pdfbookmark[1]{Contents}{section}
+\tableofcontents
+
+\clearpage
+\thispagestyle{plain}
+\pagenumbering{arabic}
+
+
+
+\section{Introduction}
+Unguided manual resource management is difficult.
+Part of the difficulty results from not having any guarantees about the current state of an object.
+Objects can be internally composed of pointers which may reference resources that may or may not need to be manually released, and keeping track of that state for each object can be difficult for the end user.
+
+Constructors and destructors provide a mechanism which bookend the lifetime of an object, allowing the designer of an object to establish invariants for objects of a specific type.
+Constructors guarantee that object initialization code is run before the object can be used, while destructors provide a mechanism that is guaranteed to be run immediately before an object's lifetime ends.
+Constructors and destructors can help to simplify resource management when used in a disciplined way.
+In particular, when all resources are acquired in a constructor, and all resources are released in a destructor, no resource leaks are possible.
+This pattern is a popular idiom in several languages, such as \CC, known as RAII (Resource Acquisition Is Initialization).
+
+
+\section{Design}
+\label{s:Design}
+In designing constructors and destructors for \CFA, the primary goals were ease of use and maintaining backwards compatibility.
+
+In C, when a variable is defined, its value is initially undefined unless it is explicitly initialized or allocated in the static area.
+\begin{lstlisting}
+int main() {
+  int x;
+  int y = 5;
+  x = y;
+}
+\end{lstlisting}
+In the example above, ©x© is defined and left uninitialized, while ©y© is defined and initialized to 5.
+In the last line, ©x© is assigned the value of ©y©.
+The key difference between assignment and initialization being that assignment occurs on a live object (i.e. an object that contains data).
+It is important to note that this means ©x© could have been used uninitialized prior to being assigned, while ©y© could not be used uninitialized.
+Use of uninitialized variables commonly yields undefined behaviour, which is a common source of bugs in C programs. % TODO: *citation*
+
+A constructor is a special function which provides a way of ensuring that some form of object initialization is performed.
+This goal is achieved through a guarantee that a constructor will be called implicitly on every object that is allocated, immediately after the object's definition.
+Since a constructor is called on every object, it is impossible to forget to initialize a single object, as long as all constructors perform some sensible form of initialization.
+
+In \CFA, a constructor is a function with the name ©?{}©.
+Every constructor must have a return type of ©void© and at least one parameter, the first of which is colloquially referred to as the \emph{this} parameter, as in many object-oriented programming languages.
+The ©this© parameter must have a pointer type, whose base type is the type of object that the function constructs.
+There is currently a proposal to add reference types to \CFA.
+Once this proposal has been implemented, the ©this© parameter should instead be a reference type with the same restrictions.
+
+% \begin{lstlisting}
+% void ?{}(int * i) {
+%   *i = 0;
+% }
+% int x, y = 1, z;
+% \end{lstlisting}
+% In this example, a constructor is defined which initializes variables of type ©int© to 0.
+
+Consider the definition of a simple type which encapsulates a dynamic array of ©int©s.
+
+\begin{lstlisting}
+struct Array {
+  int * data;
+  int len;
+}
+\end{lstlisting}
+
+In C, if the user creates an ©Array© object, the fields ©data© and ©len© will be uninitialized by default.
+It is the user's responsibility to remember to initialize both of the fields to sensible values.
+In \CFA, the user can define a constructor to handle initialization of ©Array© objects.
+
+\begin{lstlisting}
+void ?{}(Array * arr){
+  arr->len = 10;
+  arr->data = malloc(sizeof(int)*len);
+  for (int i = 0; i < arr->len; ++i) {
+    arr->data[i] = 0;
+  }
+}
+Array x;
+\end{lstlisting}
+
+This constructor will initialize ©x© so that its ©length© field has the value 10, and its ©data© field holds a pointer to a block of memory large enough to hold 10 ©int©s, and sets the value of each element of the array to 0.
+This particular form of constructor is called the \emph{default constructor}, because it is called an object defined without an initializer.
+A default constructor is a constructor which takes a single argument, the ©this© parameter.
+
+In \CFA, a destructor is a function much like a constructor, except that its name is ©^?{}©.
+A destructor for the ©Array© type can be defined as such.
+\begin{lstlisting}
+void ^?{}(Array * arr) {
+  free(arr->data);
+}
+\end{lstlisting}
+Since the destructor is automatically called for all objects of type ©Array©, the memory associated with an ©Array© will automatically be freed when the object's lifetime ends.
+% The exact guarantees made by \CFA with respect to the calling of destructors will be discussed in detail [later].
+
+As discussed previously, the distinction between initialization and assignment is important.
+Consider the following example.
+\begin{lstlisting}
+Array x;
+Array y;
+Array z = x;
+y = x;
+\end{lstlisting}
+By the previous definition of the default constructor for ©Array©, ©x© and ©y© are initialized to valid arrays of length 10 after their respective definitions.
+On line 3, ©z© is initialized with the value of ©x©, while on line ©4©, ©y© is assigned the value of ©x©.
+The key distinction between initialization and assignment is that a value about to be initialized does not hold any meaningful values, whereas an object about to be assigned might.
+In particular, these cases cannot be handled the same way because in the former case ©z© does not currently own an array, while ©y© does.
+
+\begin{lstlisting}
+void ?{}(Array * arr, Array other) {
+  arr->len = other.len;
+  arr->data = malloc(sizeof(int)*arr->len)
+  for (int i = 0; i < arr->len; ++i) {
+    arr->data[i] = other.data[i];
+  }
+}
+Array ?=?(Array * arr, Array other) {
+  ^?{}(arr);
+  ?{}(arr, other);
+  return *arr;
+}
+\end{lstlisting}
+The two functions above handle these cases.
+The first function is called a \emph{copy constructor}, because it constructs its argument from a single value of the same type.
+The second function is the standard copy assignment operator.
+These four functions are special in that they control the state of most objects.
+
+% TODO: start new section here? this is where the definition of the rules begins to become more formal, whereas everything leading up to this was mostly exposition by example
+\subsection{Function Generation Details}
+By default, every type is defined to have the core set of functions described previously.
+To mimic the behaviour of plain C, the default constructor and destructor for all of the basic types are defined to do nothing, while the copy constructor and assignment operator perform a bitwise copy of the source parameter.
+
+There are several options for user-defined types: structures, unions, and enumerations.
+To aid in ease of use, the standard set of four functions is automatically generated for a user-defined type after its definition is completed.
+
+The generated functions for enumerations are the simplest.
+Since enumerations in C are essentially just another integral type, the generated functions behave in the same way that the builtin functions for the basic types work.
+
+For structures, the situation is more complicated.
+For a structure ©S© with members ©M$_0$©, ©M$_1$©, ... ©M$_{N-1}$©, each function ©f© in the standard set will call ©f(s->M$_i$, ...)© for each ©$i$©.
+That is, a default constructor for ©S© will default construct the members of ©S©, the copy constructor with copy construct them, and so on.
+ % TODO: description VERY weak. Flesh out details
+For example given the struct definition
+\begin{lstlisting}
+struct A {
+  B b;
+  C c;
+}
+\end{lstlisting}
+The following functions are implicitly generated.
+\begin{lstlisting}
+void ?{}(A * this) {
+  ?{}(&this->b);
+  ?{}(&this->c);
+}
+void ?{}(A * this, A other) {
+  ?{}(&this->b, other.b);
+  ?{}(&this->c, other.c);
+}
+A ?=?(A * this, A other) {
+  ?=?(&this->b, other.b);
+  ?=?(&this->c, other.c);
+}
+void ^?{}(A * this) {
+  ^?{}(&this->b);
+  ^?{}(&this->c);
+}
+\end{lstlisting}
+
+In addition to the standard set, a set of \emph{field constructors} is also generated for structures.
+The field constructors are constructors that consume a prefix of the struct's member list.
+That is, $N$ constructors are built of the form ©void ?{}(S *, T$_{\text{M}_0}$)©, ©void ?{}(S *, T$_{\text{M}_0}$, T$_{\text{M}_1}$)©, ..., ©void ?{}(S *, T$_{\text{M}_0}$, T$_{\text{M}_1}$, ..., T$_{\text{M}_{N-1}}$)©, where members are copy constructed if they have a corresponding positional argument and are default constructed otherwise.
+The addition of field constructors allows structs in \CFA to be used naturally in the same ways that they could be used in C (i.e. to initialize any prefix of the struct).
+Extending the previous example, the following constructors are implicitly generated for ©A©.
+\begin{lstlisting}
+void ?{}(A * this, B b) {
+  ?{}(&this->b, b);
+  ?{}(&this->c);
+}
+void ?{}(A * this, B b, C c) {
+  ?{}(&this->b, b);
+  ?{}(&this->c, c);
+}
+\end{lstlisting}
+
+For unions, the default constructor and destructor do nothing, as it's not obvious which member if any should be constructed.
+For copy constructor and assignment operations, a bitwise ©memcpy© is applied.
+An alterantive to this design is to always construct and destruct the first member of a union, to match with the C semantics of initializing the first member of the union.
+This approach ultimately feels subtle and unsafe.
+Another option is to, like \CC, disallow unions from containing members which are themselves managed types.
+This is a reasonable approach from a safety standpoint, but is not very C-like.
+Since the primary purpose of a union is to provide low-level memory optimization, it is assumed that the user has a certain level of maturity.
+It is therefore the responsibility of the user to define the special functions explicitly if they are appropriate, since it is impossible to accurately predict the ways that a union is intended to be used at compile-time.
+
+Arrays are a special case in the C type system.
+C arrays do not carry around their size, making it impossible to write a standalone \CFA function which constructs or destructs an array while maintaining the standard interface for constructors and destructors.
+Instead, \CFA defines the initialization and destruction of an array recursively.
+That is, when an array is defined, each of its elements will be constructed in order from element 0 up to element $n-1$.
+When an array is to be implicitly destructed, each of its elements is destructed in reverse order from element $n-1$ down to element 0.
+
+\subsection{Using Constructors and Destructors}
+Implicitly generated constructor and destructor calls ignore the outermost type qualifiers on a type by way of a cast on the first argument to the function.
+This mechanism allows the same constructors and destructors to be used for qualified objects as for unqualified objects.
+Since this applies only to implicitly generated constructor calls, the language will not allow qualified objects to be re-initialized with a constructor without an explicit cast.
+
+Unlike \CC, \CFA provides an escape hatch that allows a user to decide at an object's definition whether it should be managed or not.
+An object initialized with \lstinline{@=} is guaranteed to be initialized like a C object, and will not be implicitly destructed.
+This feature provides all of the freedom that C programmers are used to having to optimize the program, while maintaining safety as a sensible default.
+In addition to freedom, \lstinline{@=} provides a simple path to migrating legacy C code to Cforall, in that objects can be moved from C-style initialization to \CFA gradually and individually.
+It is worth noting that the use of unmanaged objects can be tricky to get right, since there is no guarantee that the proper invariants will be established on an unmanaged object.
+It is recommended that most objects are managed by sensible constructors and destructors, except where absolutely necessary.
+
+When the user defines any constructor, the intrinsic/generated functions become invisible.
+In the current implementation, the default constructor and copy constructor are only hidden when explicitly overriden, since the derefence operator ©*?© is currently an ©otype© function, which would make it impossible to override a constructor, due to the lack of assertion-satifying funcitons.
+There is a proposal which decouples size/alignment type information from ©otype©, and implementing this would allow constructors and destructors to be hidden by the same rules that \CC uses.
+
+% TODO discuss compile time "checks" for subobjects when defining ctor/dtor for struct
+When defining a constructor or destructor for a struct ©S©, any members that are not explicitly constructed or destructed will be implicitly constructed or destructed automatically.
+If an explicit call is present, then that call is taken in preference to any implicitly generated call.
+A consequence of this rule is that it is possible, unlike \CC, to precisely control the order of construction and destruction of subobjects on a per-constructor basis, whereas in \CC subobject initialization and destruction is always performed based on the declaration order.
+Finally, it is illegal for a subobject to be explicitly constructed after it is used for the first time.
+If the translator cannot be reasonably sure that an object is constructed prior to its first use, but may be constructed afterward, and error is emitted.
+To override this rule, \lstinline{@=} can be used to force the translator to trust the programmer's discretion.
+This form of \lstinline{@=} is not yet implemented.
+
+% TODO discuss error if initializer nesting is too deep or contains designations
+Despite great effort, some forms of C syntax do not work well with constructors in \CFA.
+In particular, constructor calls cannot contain designations, since this is equivalent to allowing designations on the arguments to arbitrary function calls.
+In C, function prototypes are permitted to have arbitrary parameter names, including no names at all, which may have no connection to the actual names used at function definition.
+Furthermore, a function prototype can be repeated an arbitrary number of times, each time using different names.
+As a result, it was decided that any attempt to resolve designated function calls with C's function prototype rules would be brittle, and thus it is not sensible to allow designations in constructor calls.
+In addition, constructor calls cannot have a nesting depth greater than the number of array components in the type of the initialized object, plus one.
+In C, having a greater nesting depth would mean that the programmer intends to initialize subobjects with the nested initializer.
+The reason for this omission is to both simplify the mental model for using constructors, and to make the case of initialization simpler for the resolver.
+If this were allowed, it would be necessary for the expression resolver to decide whether each argument to the constructor call could initialize to some argument to one of the available constructors, making the problem highly recursive and potentially much more expensive.
+It should be noted that if an object does not have a non-trivial constructor, it can still make use of designations and nested initializers in \CFA.
+
+% TODO section on where destruction occurs - probably belongs in implementation section? or part of it does, anyway
+Destructors are automatically called at the end of the block in which the object was declared.
+In addition to this, destructors are automatically called when statements manipulate control flow to leave the block in which the object is declared, e.g. with return, break, continue, and goto statements.
+
+% TODO discuss copy construction for function parameters and return values
+When a function is called, the arguments supplied to the call are subject to implicit copy construction, and the return value is subject to destruction.
+When a value is returned from a function, the copy constructor is called to pass the value back to the call site.
+Exempt from these rules are intrinsic and builtin functions.
+
+% TODO discuss ©= + copy construction?
+
+% \subsection{Implementation}
+% Discuss the implementation details of constructors and destructors.
+
+\end{document}
Index: doc/proposals/tuples/Makefile
===================================================================
--- doc/proposals/tuples/Makefile	(revision 981bdc611ba9967f6a7ef2dec163e17a63effb7d)
+++ doc/proposals/tuples/Makefile	(revision 981bdc611ba9967f6a7ef2dec163e17a63effb7d)
@@ -0,0 +1,81 @@
+## Define the appropriate configuration variables.
+
+MACROS = ../../LaTeXmacros
+BIB = ../../bibliography
+
+TeXLIB = .:$(MACROS):$(MACROS)/listings:$(MACROS)/enumitem:$(BIB)/:
+LaTeX  = TEXINPUTS=${TeXLIB} && export TEXINPUTS && latex -halt-on-error
+BibTeX = BIBINPUTS=${TeXLIB} && export BIBINPUTS && bibtex
+
+## Define the text source files.
+
+SOURCES = ${addsuffix .tex, \
+tuples \
+}
+
+FIGURES = ${addsuffix .tex, \
+}
+
+PICTURES = ${addsuffix .pstex, \
+}
+
+PROGRAMS = ${addsuffix .tex, \
+}
+
+GRAPHS = ${addsuffix .tex, \
+}
+
+## Define the documents that need to be made.
+
+DOCUMENT = tuples.pdf
+
+# Directives #
+
+all : ${DOCUMENT}
+
+clean :
+	rm -f *.bbl *.aux *.dvi *.idx *.ilg *.ind *.brf *.out *.log *.toc *.blg *.pstex_t *.cf \
+		${FIGURES} ${PICTURES} ${PROGRAMS} ${GRAPHS} ${basename ${DOCUMENT}}.ps ${DOCUMENT}
+
+# File Dependencies #
+
+${DOCUMENT} : ${basename ${DOCUMENT}}.ps
+	ps2pdf $<
+
+${basename ${DOCUMENT}}.ps : ${basename ${DOCUMENT}}.dvi
+	dvips $< -o $@
+
+${basename ${DOCUMENT}}.dvi : Makefile ${GRAPHS} ${PROGRAMS} ${PICTURES} ${FIGURES} ${SOURCES} ${basename ${DOCUMENT}}.tex \
+		$(MACROS)/common.tex $(MACROS)/indexstyle $(BIB)/cfa.bib
+	# Conditionally create an empty *.ind (index) file for inclusion until makeindex is run.
+	if [ ! -r ${basename $@}.ind ] ; then touch ${basename $@}.ind ; fi
+	# Must have *.aux file containing citations for bibtex
+	if [ ! -r ${basename $@}.aux ] ; then ${LaTeX} ${basename $@}.tex ; fi
+	-${BibTeX} ${basename $@}
+	# Some citations reference others so run steps again to resolve these citations
+	${LaTeX} ${basename $@}.tex
+	-${BibTeX} ${basename $@}
+	# Make index from *.aux entries and input index at end of document
+	makeindex -s $(MACROS)/indexstyle ${basename $@}.idx
+	${LaTeX} ${basename $@}.tex
+	# Run again to get index title into table of contents
+	${LaTeX} ${basename $@}.tex
+
+predefined :
+	sed -f predefined.sed ${basename ${DOCUMENT}}.tex > ${basename $@}.cf
+
+## Define the default recipes.
+
+%.tex : %.fig
+	fig2dev -L eepic $< > $@
+
+%.ps : %.fig
+	fig2dev -L ps $< > $@
+
+%.pstex : %.fig
+	fig2dev -L pstex $< > $@
+	fig2dev -L pstex_t -p $@ $< > $@_t
+
+# Local Variables: #
+# compile-command: "make" #
+# End: #
Index: doc/proposals/tuples/tuples.tex
===================================================================
--- doc/proposals/tuples/tuples.tex	(revision 981bdc611ba9967f6a7ef2dec163e17a63effb7d)
+++ doc/proposals/tuples/tuples.tex	(revision 981bdc611ba9967f6a7ef2dec163e17a63effb7d)
@@ -0,0 +1,336 @@
+% inline code ©...© (copyright symbol) emacs: C-q M-)
+% red highlighting ®...® (registered trademark symbol) emacs: C-q M-.
+% blue highlighting ß...ß (sharp s symbol) emacs: C-q M-_
+% green highlighting ¢...¢ (cent symbol) emacs: C-q M-"
+% LaTex escape §...§ (section symbol) emacs: C-q M-'
+% keyword escape ¶...¶ (pilcrow symbol) emacs: C-q M-^
+% math escape $...$ (dollar symbol)
+
+\documentclass[twoside,11pt]{article}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Latex packages used in the document (copied from CFA user manual).
+\usepackage[T1]{fontenc}                                % allow Latin1 (extended ASCII) characters
+\usepackage{textcomp}
+\usepackage[latin1]{inputenc}
+\usepackage{fullpage,times,comment}
+\usepackage{epic,eepic}
+\usepackage{upquote}									% switch curled `'" to straight
+\usepackage{calc}
+\usepackage{xspace}
+\usepackage{graphicx}
+\usepackage{varioref}									% extended references
+\usepackage{listings}									% format program code
+\usepackage[flushmargin]{footmisc}						% support label/reference in footnote
+\usepackage{latexsym}                                   % \Box glyph
+\usepackage{mathptmx}                                   % better math font with "times"
+\usepackage[usenames]{color}
+\usepackage[pagewise]{lineno}
+\renewcommand{\linenumberfont}{\scriptsize\sffamily}
+\input{common}                                          % bespoke macros used in the document
+\usepackage[dvips,plainpages=false,pdfpagelabels,pdfpagemode=UseNone,colorlinks=true,pagebackref=true,linkcolor=blue,citecolor=blue,urlcolor=blue,pagebackref=true,breaklinks=true]{hyperref}
+\usepackage{breakurl}
+\renewcommand{\UrlFont}{\small\sf}
+
+\setlength{\topmargin}{-0.45in}							% move running title into header
+\setlength{\headsep}{0.25in}
+
+\usepackage{caption}
+\usepackage{subcaption}
+\usepackage{bigfoot}
+
+\interfootnotelinepenalty=10000
+
+\title{
+\Huge \vspace*{1in} Tuple Design in \CFA \\
+\vspace*{1in}
+}
+
+\author{
+\huge Rob Schluntz \\
+\Large \vspace*{0.1in} \texttt{rschlunt@uwaterloo.ca} \\
+\Large Cheriton School of Computer Science \\
+\Large University of Waterloo
+}
+
+\date{
+\today
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\bigO}[1]{O\!\left( #1 \right)}
+
+\begin{document}
+\pagestyle{headings}
+% changed after setting pagestyle
+\renewcommand{\sectionmark}[1]{\markboth{\thesection\quad #1}{\thesection\quad #1}}
+\renewcommand{\subsectionmark}[1]{\markboth{\thesubsection\quad #1}{\thesubsection\quad #1}}
+\pagenumbering{roman}
+% \linenumbers                                            % comment out to turn off line numbering
+
+\maketitle
+\thispagestyle{empty}
+
+\clearpage
+\thispagestyle{plain}
+\pdfbookmark[1]{Contents}{section}
+\tableofcontents
+
+\clearpage
+\thispagestyle{plain}
+\pagenumbering{arabic}
+
+
+\section{Introduction}
+This document describes my understanding of the existing tuple design~\cite{Buhr94a,Till89}, mixed with my thoughts on improvements after various discussions with Peter, Aaron, and Thierry.
+
+\section{Tuple Expressions}
+A tuple expression is an expression which produces a fixed-size, ordered list of values of heterogeneous types.
+The type of a tuple expression is the tuple of the subexpression types.
+In Cforall, a tuple expression is denoted by a list of expressions enclosed in square brackets.
+
+For example, the expression ©[5, 'x', 10.5]© has type ©[int, char, double]©.
+Tuples are a compile-time phenomenon and have little to no run-time presence.
+
+\subsection{Tuple Variables}
+It is possible to have variables of tuple type, pointer to tuple type, and array of tuple type.
+Tuple types can be composed of any types, except for array types \footnote{I did not see this issue mentioned at all in the original design. A tuple containing an array type seems to make sense up until you try to use a tuple containing an array type as a function parameter. At this point you lose information about the size of the array, which makes tuple assignment difficult. Rather than allowing arrays in most situations and disallowing only as function parameters, it seems like it would be better to be consistent across the board.}.
+
+\begin{lstlisting}
+[double, int] di;
+[double, int] * pdi
+[double, int] adi[10];
+\end{lstlisting}
+The program above declares a variable of type ©[double, int]©, a variable of type pointer to ©[double, int]©, and an array of ten ©[double, int]©.
+
+\subsection{Flattening and Structuring}
+In Cforall, tuples do not have a rigid structure.
+In function call contexts, tuples support implicit flattening and restructuring \footnote{In the original tuple design, four tuple coercions were described: opening, closing, flattening, and structuring. I've combined flattening with opening and structuring with closing in my description, as the distinctions do not seem useful in Cforall since these coercions happen only as arguments to function calls, and I believe all of the semantics are properly covered by the simplified descriptions.}. Tuple flattening recursively expands a tuple into the list of its basic components. Tuple structuring packages a list of expressions into a value of tuple type.
+
+\begin{lstlisting}
+int f(int, int);
+int g([int, int]);
+int h(int, [int, int]);
+[int, int] x;
+int y;
+
+f(x);
+g(y, 10);
+h(x, y);
+\end{lstlisting}
+In Cforall, each of these calls is valid.
+In the call to ©f©, ©x© is implicitly flattened so that the components of ©x© are passed as the two arguments to ©f©.
+For the call to ©g©, the values ©y© and ©10© are structured into a single argument of type ©[int, int]© to match the type of the parameter of ©g©.
+Finally, in the call to ©h©, ©y© is flattened to yield an argument list of length 3, of which the first component of ©x© is passed as the first parameter of ©h©, and the second component of ©x© and ©y© are structured into the second argument of type ©[int, int]©.
+
+\section{Functions}
+\subsection{Argument Passing}
+In resolving a function call, all of the arguments to the call are flattened.
+While determining if a particular function/argument-list combination is valid, the arguments are structured to match the shape of each formal parameter, in order.
+
+For example, given a function declaration ©[int] f(int, [double, int])©, the call ©f([5, 10.2], 0)© can be satisfied by first flattening the tuple to yield the expression ©f(5, 10.2, 0)© and then structuring the argument list to match the formal parameter list structure as ©f(5, [10.2, 0])©.
+
+\subsection{Multiple-Return-Value Functions}
+Functions can be declared to return more than one value.
+Multiple return values are packaged into a tuple value when the function returns.
+A multiple-returning function with return type ©T© can return any expression which is implicitly convertible to ©T©.
+
+\subsection{Tuple Assignment}
+An assignment where the left side of the assignment operator has a tuple type is called tuple assignment.
+There are two kinds of tuple assignment depending on whether the right side of the assignment operator has a tuple type or a non-tuple type, called Multiple Assignment and Mass Assignment respectively.
+Let $L_i$ for $i$ in $[0, n)$ represent each component of the flattened left side, $R_i$ represent each component of the flattened right side of a multiple assignment, and $R$ represent the right side of a mass assignment.
+
+For a multiple assignment to be valid, both tuples must have the same number of elements when flattened. Multiple assignment assigns $R_i$ to $L_i$ for each $i$.
+That is, ©?=?(&$L_i$, $R_i$)© must be a well-typed expression.
+
+Mass assignment assigns the value $R$ to each $L_i$. For a mass assignment to be valid, ©?=?(&$L_i$, $R$)© must be a well-typed expression.
+This differs from C cascading assignment (e.g. ©a=b=c©) in that conversions are applied to $R$ in each individual assignment, which prevents data loss from the chain of conversions that can happen during a cascading assignment.
+
+Both kinds of tuple assignment have parallel semantics, such that each value on the left side and right side is evaluated \emph{before} any assignments occur.
+Tuple assignment is an expression where the result type is the type of the left side of the assignment, as in normal assignment (i.e. the tuple of the types of the left side expressions) \footnote{This is a change from the original tuple design, wherein tuple assignment was a statement. This decision appears to have been made in an attempt to fix what was seen as a problem with assignment, but at the same time this doesn't seem to fit C or Cforall very well. In another language, tuple assignment as a statement could be reasonable, but I don't see a good justification for making this the only kind of assignment that isn't an expression. In this case, I would value consistency over idealism}.
+These semantics allow cascading tuple assignment to work out naturally in any context where a tuple is permitted.
+
+The following example shows multiple, mass, and cascading assignment in one expression
+\begin{lstlisting}
+  int a, b;
+  double c, d;
+  [void] f([int, int]);
+  f([c, a] = [b, d] = 1.5);
+\end{lstlisting}
+First a mass assignment of ©1.5© into ©[b, d]©, which assigns ©1.5© into ©b©, which is truncated to ©1©, and ©1© into ©d©, producing the tuple ©[1, 1.5]© as a result.
+That tuple is used as the right side of the multiple assignment (i.e. ©[c, a] = [1, 1.5]©) which assigns ©1© into ©c© and ©1.5© into ©a©, which is truncated to ©1©, producing the result ©[1, 1]©.
+Finally, the tuple ©[1, 1]© is used as an expression in the call to ©f©.
+
+\subsection{Tuple Construction}
+Tuple construction and destruction follow the same rules and semantics as tuple assignment, except that in the case where there is no right side, the default constructor or destructor is called on each component of the tuple.
+
+It is possible to define constructors and assignment functions for tuple types that provide new semantics.
+For example, the function ©void ?{}([T, U] *, S);© can be defined to allow a tuple variable to be constructed from a value of type ©S©. Due to the structure of generated constructors, it is possible to pass a tuple to a generated constructor for a type with a member prefix that matches the type of the tuple (e.g. an instance of ©struct S { int x; double y; int z }© can be constructed with a tuple of type ©[int, double]©, `out of the box').
+
+\section{Other Tuple Expressions}
+\subsection{Member Tuple Expression}
+It is possible to access multiple fields from a single expression using a Member Tuple Expression \footnote{Called ``record field tuple'' in the original design, but there's no reason to limit this feature to only structs, so ``field tuple'' or ``member tuple'' feels more appropriate.}.
+The result is a single tuple-valued expression whose type is the tuple of the types of the members.
+A member tuple expression has the form ©a.[x, y, z];© where ©a© is an expression with type ©T©, where ©T© supports member access expressions, and ©x, y, z© are all members of ©T© with types ©T$_x$©, ©T$_y$©, and ©T$_z$© respectively.
+Then the type of ©a.[x, y, z]© is ©[T$_x$, T$_y$, T$_z$]©.
+It is possible for a member tuple expression to contain other member access expressions, e.g. ©a.[x, y.[i, j], z.k]©.
+This expression is equivalent to ©[a.x, [a.y.i, a.y.j], a.z.k]©.
+It is guaranteed that the aggregate expression to the left of the ©.© on a member tuple expression is evaluated once.
+
+\subsection{Tuple Indexing}
+Sometimes it is desirable to access a single component of a tuple-valued expression without creating unnecessary temporary variables to assign to.
+Given a tuple-valued expression ©e© and a compile-time constant integer $i$ where $0 \leq i < n$, where $n$ is the number of components in ©e©, ©e.i© will access the $i$\textsuperscript{th} component of ©e©.
+% \footnote{If this syntax cannot be parsed, we can make it ©_i©, and a semantic check ensures that ©_i© has the right form. The capability to access a component of a tuple is helpful internally, and there doesn't seem to be a disadvantage to exposing it to users. On the other hand, it is more general than casting and much more explicit, while also being less verbose.}.
+It is possible to use a member tuple expression with tuple indexing to manually restructure a tuple (rearrange components, drop components, duplicate components, etc.).
+
+% TODO: mention that Tuple.member_name and Aggregate.index could have sensible semantics, but introduce complexity into the model. Agg.idx could mean get the ith member of the aggregate (further, this could be extended for enumerations as well, where the LHS is a type instead of a value), but it's not clear there is a compelling use-case. Tuple.member_name can either mean "distribute the member across the elements of the tuple" [effectively a compile-time map], or alternatively array.member_name (to mean basically the same thing). The problem with this is that it takes this expression's meaning from being clear at compile-time to needing resolver support, as the member name needs to appropriately distribute across every member of the tuple, which could itself be a tuple, etc. Again, the extra complexity is not currently justified.
+
+For example
+\begin{lstlisting}
+  [int, double] x;
+  [double, int, double] y = [x.1, x.0, x.1];  // (1)
+
+  [int, int, int] f();
+  [x.0, y.1] = f().[0, 2];                    // (2)
+\end{lstlisting}
+
+(1) ©y© is initialized using a tuple expression which selects components from the tuple variable ©x©.
+
+(2) A mass assignment of the first and third components from the return value of ©f© into the first component of ©x© and the second component of ©y©.
+
+\subsection{Casting}
+A cast to tuple type is valid when $T_n \leq S_m$, where $T_n$ is the number of components in the target type and $S_m$ is the number of components in the source type, and for each $i$ in $[0, n)$, $S_i$ can be cast to $T_i$.
+Excess elements ($S_j$ for all $j$ in $[n, m)$) are evaluated, but their values are discarded so that they are not included in the result expression.
+This naturally follows the way that a cast to void works in C.
+
+For example,
+\begin{lstlisting}
+  [int, int, int] f();
+  [int, [int, int], int] g();
+
+  ([int, double])f();           // (1)
+  ([int, int, int])g();         // (2)
+  ([void, [int, int]])g();      // (3)
+  ([int, int, int, int])g();    // (4)
+  ([int, [int, int, int]])g();  // (5)
+\end{lstlisting}
+
+(1) discards the last element of the return value and converts the second element to type double.
+
+(2) discards the second component of the second element of the return value of ©g© (if ©g© is free of side effects, this is equivalent to ©[(int)(g().0), (int)(g().1.0), (int)(g().2)]©).
+
+(3) discards the first and third return values (equivalent to ©[(int)(g().1.0), (int)(g().1.1)]©).
+
+(4) is invalid because the cast target type contains 4 components, while the source type contains only 3.
+
+(5) is invalid because the cast ©([int, int, int])(g().1)© is invalid (i.e. it is invalid to cast ©[int, int]© to ©[int, int, int]©)
+
+
+\section{Tuples for Variadic Functions}
+Functions with tuple parameters can be used to provide type-safe variadic functions.
+It appears that it would be possible to leverage tuples to get similar power to what \CC vardiadic templates provide, but with the ability to separately compile them.
+
+\subsection{Option 1: Allow type parameters to match whole tuples, rather than just their components}
+This option could be implemented with two phases of argument matching when a function contains type parameters and the argument list contains tuple arguments.
+If flattening and structuring fail to produce a match, a second attempt at matching the function and argument combination is made where tuple arguments are not expanded and structure must match exactly, modulo implicit conversions. \footnote{It may be desirable to skip the exact matching rule if flattening and structuring produce a match that fails when inferring assertion parameters, at least in the current resolver since our assertion inference appears to be very inefficient.}
+
+For example:
+\begin{lstlisting}
+  forall(otype T, otype U | { T g(U); })
+  void f(T, U);
+
+  [int, int] g([int, int, int, int]);
+
+  f([1, 2], [3, 4, 5, 6]);
+\end{lstlisting}
+With flattening and structuring, the call is first transformed into ©f(1, 2, 3, 4, 5, 6)©.
+Since the first argument of type ©T© does not have a tuple type, unification decides that ©T=int© and ©1© is matched as the first parameter.
+Likewise, ©U© does not have a tuple type, so ©U=int© and ©2© is accepted as the second parameter.
+There are now no remaining formal parameters, there are remaining arguments, and the function is not variadic, so the match fails.
+
+With exact matching, ©T=[int,int]© and ©U=[int,int,int,int]© and so the arguments type check.
+When inferring assertion ©g©, a match is found.
+\footnote{This type of interaction between tuple arguments and type parameters is desirable for perfect forwarding, but it's not obvious to me exactly how this should interact with assertion inference. Ideally, the same rules should apply for assertion satisfaction as apply to argument matching (i.e. flattening \& structuring should be attempted, followed by an exact match attempt on failure), but this may be more complicated than it sounds for assertion satisfaction. Aaron, I'm especially interested to hear your thoughts on this with respect to efficiency in the resolver redesign.
+
+For example, should we allow this to match?
+\begin{lstlisting}
+  forall(otype T, otype U | { T g(U); })
+  void f(T, U);
+
+  [int, int] g(int, ®[int, int]®, int);
+
+  f([1, 2], [3, 4, 5, 6]);
+\end{lstlisting}
+To only have an exact matching rule here feels too strict. At the very least, it would be nice to accept ©[int, int] g(int, int, int, int)©, since that would allow for argument lists to be packaged and sent off to polymorphic functions and then directly forwarded to other functions.}.
+
+The addition of an exact matching rule only affects the outcome for polymorphic type binding when tuples are involved.
+For non-tuple arguments, exact matching and flattening \& structuring are equivalent. For tuple arguments to a function without polymorphic formal parameters, flattening and structuring work whenever an exact match would have worked (the tuple is flattened and implicitly restructured to its original structure).
+Thus there is nothing to be gained from permitting the exact matching rule to take effect when a function does not contain polymorphism and none of the arguments are tuples.
+
+\subsection{Option 2: Add another type parameter kind}
+Perhaps a simpler alternative would be to add another kind of type parameter (e.g., ©ttype©).
+There should be at most one ©ttype© parameter which must occur last in a parameter list.
+Matching against a ©ttype© parameter would consume/package all remaining argument components into a tuple, and would also match no arguments.
+These semantics more closely match normal variadic semantics, while being type-safe. C variadic syntax and ©ttype© polymorphism probably should not be mixed, since it is not clear where to draw the line to decide which arguments belong where.\footnote{In fact, if we go with this proposal, it might be desirable to disallow polymorphic functions to use C variadic syntax to encourage a Cforall style. Aside from maybe calling C variadic functions, it's not obvious to me there would be anything you can do with C variadics that couldn't also be done with ©ttype© parameters. }
+
+Example 1: taken from Wikipedia, demonstrates variadic templates done in a Cforall style
+\begin{lstlisting}
+  void func(void) {}                           // termination version (1)
+  forall(otype T, ttype Params | { void process(const T &); void func(const Params &); })
+  void func(const T& arg1, const Params & p) { // (2)
+    process(arg1);
+    func(p);
+  }
+  void process(int);                           // (3)
+  void process(double);                        // (4)
+  func(1, 2.0, 3.5, 4);
+\end{lstlisting}
+In the call to ©func©, the value ©1© is taken as the first parameter, so ©T© unifies with ©int©, and the arguments ©2.0©, ©3.5©, and ©4© are consumed to form a tuple argument of type ©[double, double, int]©.
+To satisfy the assertions to ©func©, the functions (3) and (2) are implicitly selected to satisfy the requirements of ©void process(const T &)© and ©void func(const Params &)© respectively.
+Since (2) requires assertion parameters, the process repeats selecting (4) and (2).
+The matching process continues recursively until reaching the base case where (3) and (1) are selected.
+The end result is semantically equivalent to ©process(1), process(2.0), process(3.5), process(4)©.
+
+Since (2) is not an exact match for the expected assertion parameter, a thunk is generated that wraps a call to ©func© that accepts an argument of type ©[double, double, int]©.
+This conversion already occurs in the Cforall translator, but may require some modification to handle all of the cases present here.
+
+Example 2: new (i.e. type-safe malloc + constructors)
+\begin{lstlisting}
+  forall(dtype T, ttype Params | sized(T) | { void ?{}(T *, Params); })
+  T * new(Params p) {
+    return malloc(){ p };
+  }
+  array(int) * x = new(1, 2, 3, 4);
+\end{lstlisting}
+In the call to ©new©, ©array(int)© is selected to match ©T©, and ©Params© is expanded ot match ©[int, int, int, int]©. To satisfy the assertions, a constructor with an interface compatible with ©void ?{}(array(int) *, int, int, int, int)© must exist in the current scope.
+
+Assertion inference can also be special cased to match functions that take tuples of any structure only for ttype parameters, if desired.
+
+
+\subsection{Conclusions}
+With either option, we can generate a thunk to perform the conversion from the actual argument's structure to the structure expected by the assertion parameter and that function would be passed as the assertion argument, in a manner similar to the other thunks that are already generated.
+
+I prefer option 2, because it is simpler and I think the semantics are clearer.
+I wouldn't be surprised if it was also noticeably more efficient, because of the lack of backtracking.
+
+As a side note, option 1 also requires calls to be written explicitly, e.g. ©array(int) * x = new([1, 2, 3, 4]);©, which isn't particularly appealing.
+It shifts the burden from the compiler to the programmer, which is almost always wrong, and doesn't match with the way our tuples can be used elsewhere.
+The more I think about it, the more I'm convinced option 1 is the wrong approach, but I'm putting it out anyway in case someone has a good thought on how to make it work correctly.
+
+\addcontentsline{toc}{section}{\refname}
+\bibliographystyle{plain}
+\bibliography{cfa}
+
+%\addcontentsline{toc}{section}{\indexname} % add index name to table of contents
+%\begin{theindex}
+%Italic page numbers give the location of the main entry for the referenced term.
+%Plain page numbers denote uses of the indexed term.
+%Entries for grammar non-terminals are italicized.
+%A typewriter font is used for grammar terminals and program identifiers.
+%\indexspace
+%\input{comp_II.ind}
+%\end{theindex}
+
+\end{document}
