Index: doc/theses/fangren_yu_MMath/performance.tex
===================================================================
--- doc/theses/fangren_yu_MMath/performance.tex	(revision d9878815c295edc9ce535193cb04fcb36ab3c8b3)
+++ doc/theses/fangren_yu_MMath/performance.tex	(revision 4002956bc9d688ce37f113888b160a6ed5aca4d6)
@@ -1,3 +1,59 @@
-\chapter{Performance}
+\chapter{Future Work}
 
-If there are any performance experiments.
+These are some feature requests related to type system enhancement that come up during the development of \CFA language and library, but have not been implemented yet. A lot of the current implementations have to work around the limits of the language features and sometimes lead to inefficiency. 
+
+\section{Closed trait types}
+
+\CFA as it currently is does not have any closed types, as new functions can be added at any time. It is also possible to locally declare a function\footnote{Local functions are not a standard feature in C but supported by mainstream C compilers such as gcc, and allowed in \CFA too.} or a function pointer to make a type satisfy a certain trait temporarily and be used as such in this limited scope. However, the lack of closed types in such a "duck typing" scheme proposes two problems. For library implementors, it is common to not want the defined set of operations to be overwritten and cause the behavior of polymorphic invocations to change. For the compiler, it means caching and reusing the result of resolution is not reliable as newly introduced declarations can participate in assertion resolution, making a previously invalid expression valid, or the other way around by introducing ambiguity in assertions. Sometimes those interfaces are fairly complicated, for example the I/O library traits \textbf{istream} and \textbf{ostream} each has over 20 operations. Without the ability to store and reuse assertion resolution results, each time the compiler encounters an I/O operation in the source code (mainly the pipe operator \textbf{?|?} used to represent stream operations in \CFA) it has to resolve the same set of assertions again, causing a lot of repetitive work. Previous experiments have shown that the I/O assertions often account for over half of the number of assertions resolved in a \CFA translation unit. Introducing a way to eliminate the need of doing such repetitive assertion resolutions that are very unlikely to change by new overloads can therefore provide significant improvement to the performance of the compiler.
+
+\section{Associated Types}
+
+The analysis presented in section 4.3 shows that if we mandate that all type parameters have to be bound before assertion resolution, the complexity of resolving assertions become much lower as every assertion parameter can be resolved independently. By fully utilizing information from higher up the expression tree for return value overloading, most of the type bindings can be resolved. However there are certain scenarios where we would like to have some intermediate types to be involved in certain operations, that are neither input nor output types.
+
+\CFA standard library provides a few polymorphic container types similar to those found in \CC standard template library. Naturally, we would like to have a harmonized iterator interface for different container types. The feature is still under development and has not been finalized, but for the purpose of this discussion, we will be using a similar approach to the \CC standard iterator contract. The equivalent type signatures can be given in \CFA trait as:
+
+\begin{cfa}
+    forall (Container, Iter, Elem) trait iterable {
+        Iter begin(Container);
+        Iter end(Container);
+        Elem& *?(Iter);
+        Iter ++?(Iter);
+        bool ?==?(Iter,Iter);
+    }
+\end{cfa}
+
+These are the exact operators required in \CC for the for-loop comprehension
+@for (Elem & e: container)@. The problem with this trait declaration is that the iterator type @Iter@ has to be explicitly given in the trait parameter list, but is intended to be deduced from the @begin@ and @end@ operations on the container type; and the same can be said for the element type. The iterable trait is meant to describe a property for the container type but involves two additional types, one for the iterator type and one for the element type. If we were to disallow unbound type parameters in assertions without adding any features to the type system, we will not be able to describe this iterable property in \CFA. 
+
+To solve this problem, I propose adding associate type declarations in addition to the existing (free) @forall@ type parameters. In the body of a trait declaration, new types can be introduced as the return type of an expression involving the type parameters. Following the above example, the iterator contract could be rewritten to
+\begin{cfa}
+    forall (Container) trait iterable {
+        type Iter = begin(Container);
+        type Elem& = *?(Iter);
+        Iter end(Container);
+        Iter ++?(Iter);
+        bool ?==?(Iter,Iter);
+    }
+\end{cfa}
+
+This matches conceptually better that the iterable trait is about one type (the container) rather than about three types. The iterator type and element type can be viewed as properties of the container types, not independent type parameters.
+
+There remains one design decision to be made, that is whether the expressions that define associated types need to be uniquely resolved. If the associated type does not appear in parameter or return types, having such requirement seems to be reasonable, because the expression cost does not consider any conversions that occur in assertion parameter matching, which essentially means having multiple ways to resolve an associated type always results in ambiguity. A more interesting case would be that the associated type also appears in the return type, where both resolving the return type overload based on context and resolving the assertion that defines the associate type can help, and for the whole expression to resolve, they must agree on a common result. Moss gave the following example to illustrate \CFA assertion system's expressiveness that could be viewed as having an associated type as return, and can potentially vary based on the context:
+
+\begin{cfa}
+    forall(Ptr, Elem) trait pointer_like {
+        Elem& *?(Ptr); // Ptr can be dereferenced to Elem
+    };
+    struct list {
+        int value;
+        list* next; // may omit struct on type names
+    };
+    typedef list* list_iterator;
+    int& *?(list_iterator it) {
+        return it->value;
+    }
+\end{cfa}
+
+Note that the type @list*@ satisfies both @pointer_like(list*, int)@ and @pointer_like(list*, list)@ (the latter by the built-in pointer dereference operator) and the expression @*it@ could be either a @struct list@ or an @int@. Requiring associated types to be unique would make the @pointer_like@ trait inapplicable to @list*@ here, which is not desirable. I have not attempted to implement associated types in \CFA compiler, but based on the above discussions, one option could be to make associated type resolution and return type overloading coexist: when the associated type appears in the returns, we deduce it from the context and then verify the trait with ordinary assertion resolution; when it does not appear in the returns, we instead require the type to be uniquely determined by the expression that defines the associated type.
+
+\section{User-defined conversions}
