Index: doc/theses/fangren_yu_MMath/intro.tex
===================================================================
--- doc/theses/fangren_yu_MMath/intro.tex	(revision c82dad4e91592787d98be7b164b82f68e16bb70d)
+++ doc/theses/fangren_yu_MMath/intro.tex	(revision b4c6e10548edd581adb979906d0129330e8320ff)
@@ -2,6 +2,4 @@
 
 This thesis is exploratory work I did to understand, fix, and extend the \CFA type-system, specifically, the type resolver used to select polymorphic types among overloaded names.
-The \CFA type-system has a number of unique features making it different from all other programming languages.
-
 Overloading allows programmers to use the most meaningful names without fear of name clashes within a program or from external sources, like include files.
 \begin{quote}
@@ -10,7 +8,9 @@
 Experience from \CC and \CFA developers is that the type system implicitly and correctly disambiguates the majority of overloaded names, \ie it is rare to get an incorrect selection or ambiguity, even among hundreds of overloaded (variables and) functions.
 In many cases, a programmer has no idea there are name clashes, as they are silently resolved, simplifying the development process.
-Depending on the language, ambiguous cases are resolved using some form of qualification and/or casting.
-
-One of the key goals in \CFA is to push the boundary on overloading, and hence, overload resolution.
+Depending on the language, any ambiguous cases are resolved using some form of qualification and/or casting.
+
+Therefore, one of the key goals in \CFA is to push the boundary on overloading, and hence, overload resolution.
+As well, \CFA follows the current trend of replacing nominal inheritance with traits.
+Together, the resulting \CFA type-system has a number of unique features making it different from all other programming languages.
 
 
@@ -22,7 +22,7 @@
 
 All computers have multiple types because computer architects optimize the hardware around a few basic types with well defined (mathematical) operations: boolean, integral, floating-point, and occasionally strings.
-A programming language and its compiler present ways to declare types that ultimately map into those provided by the underlying hardware.
-These language types are thrust upon programmers, with their syntactic and semantic rules, and resulting restrictions.
-A language type-system defines these rules and uses them to understand how an expression is to be evaluated by the hardware.
+A programming language and its compiler present ways to declare types that ultimately map into the ones provided by the underlying hardware.
+These language types are thrust upon programmers, with their syntactic and semantic rules and restrictions.
+These rules are used to transform a language expression to a hardware expression.
 Modern programming-languages allow user-defined types and generalize across multiple types using polymorphism.
 Type systems can be static, where each variable has a fixed type during execution and an expression's type is determined once at compile time, or dynamic, where each variable can change type during execution and so an expression's type is reconstructed on each evaluation.
@@ -34,5 +34,5 @@
 Virtually all programming languages overload the arithmetic operators across the basic computational types using the number and type of parameters and returns.
 Like \CC, \CFA also allows these operators to be overloaded with user-defined types.
-The syntax for operator names uses the @'?'@ character to denote a parameter, \eg unary operators: @?++@, @++?@, binary operator @?+?@.
+The syntax for operator names uses the @'?'@ character to denote a parameter, \eg unary left and right operators: @?++@ and @++?@, and binary operators @?+?@ and @?<=?@.
 Here, a user-defined type is extended with an addition operation with the same syntax as builtin types.
 \begin{cfa}
@@ -43,5 +43,5 @@
 s1 = @?+?@( s1, s2 );	$\C{// direct call}\CRT$
 \end{cfa}
-The type system examines each call size and selects the best matching overloaded function based on the number and types of arguments.
+The type system examines each call site and selects the best matching overloaded function based on the number and types of arguments.
 If there are mixed-mode operands, @2 + 3.5@, the type system, like in C/\CC, attempts (safe) conversions, converting the argument type(s) to the parameter type(s).
 Conversions are necessary because the hardware rarely supports mix-mode operations, so both operands must be the same type.
@@ -71,5 +71,5 @@
 double d = f( 3 );		$\C{// select (2)}\CRT$
 \end{cfa}
-However, if the type system looks at the return type, there is an exact match for each call, which matches with programmer intuition and expectation.
+Alternatively, if the type system looks at the return type, there is an exact match for each call, which matches with programmer intuition and expectation.
 This capability can be taken to the extreme, where there are no function parameters.
 \begin{cfa}
@@ -98,15 +98,48 @@
 }
 \end{cfa}
-It is interesting that shadow overloading is considered a normal programming-language feature with only slight software-engineering problems, but variable overloading within a scope is often considered extremely dangerous.
+It is interesting that shadow overloading is considered a normal programming-language feature with only slight software-engineering problems.
+However, variable overloading within a scope is considered extremely dangerous, without any evidence to corroborate this claim.
+Similarly, function overloading occurs silently within the global scope in \CC from @#include@ files all the time without problems.
 
 In \CFA, the type system simply treats overloaded variables as an overloaded function returning a value with no parameters.
-Hence, no significant effort is required to support this feature.
-Leveraging the return type to disambiguate is essential because variables have no parameters.
+Hence, no significant effort is required to support this feature by leveraging the return type to disambiguate as variables have no parameters.
 \begin{cfa}
 int MAX = 2147483647;	$\C[2in]{// (1); overloaded on return type}$
-double MAX = ...;		$\C{// (2); overloaded on return type}$
+long int MAX = ...;		$\C{// (2); overloaded on return type}$
+double MAX = ...;		$\C{// (3); overloaded on return type}$
 int i = MAX;			$\C{// select (1)}$
-double d = MAX;			$\C{// select (2)}\CRT$
-\end{cfa}
+long int i = MAX;		$\C{// select (2)}$
+double d = MAX;			$\C{// select (3)}\CRT$
+\end{cfa}
+Hence, the name @MAX@ can replace all the C type-specific names, \eg @INT_MAX@, @LONG_MAX@, @DBL_MAX@, \etc.
+The result is a significant reduction in names to access typed constants.
+% Paraphrasing Shakespeare, ``The \emph{name} is the thing.''.
+
+
+\section{Constant Overloading}
+
+\CFA is unique in providing restricted constant overloading for the values @0@ and @1@, which have special status in C, \eg the value @0@ is both an integer and a pointer literal, so its meaning depends on context.
+In addition, several operations are defined in terms of values @0@ and @1@, \eg:
+\begin{cfa}
+if (x) x++									$\C{// if (x != 0) x += 1;}$
+\end{cfa}
+Every @if@ and iteration statement in C compares the condition with @0@, and every increment and decrement operator is semantically equivalent to adding or subtracting the value @1@ and storing the result.
+These two constants are given types @zero_t@ and @one_t@ in \CFA, which allows overloading various operations for new types that seamlessly connect to all special @0@ and @1@ contexts.
+The types @zero_t@ and @one_t@ have special builtin implicit conversions to the various integral types, and a conversion to pointer types for @0@, which allows standard C code involving @0@ and @1@ to work.
+\begin{cfa}
+struct S { int i, j; };
+void ?{}( S & s, zero_t ) { s.[i,j] = 0; }
+void ?{}( S & s, one_t ) { s.[i,j] = 1; }
+int ?!=?( S s, zero_t ) { return s.i != 0 && s.j != 0; }
+S ?+=?( S & s, one_t ) { s.i++; s.j++; return s; }
+S ?-=?( S & s, one_t ) { s.i--; s.j--; return s; }
+S ?=?( S & dst, one_t ) { return dst.[i,j] = 1; }
+void foo() {
+	S s = @0@;
+	s = @1@;
+	if ( @s@ ) @s++@;
+}
+\end{cfa}
+Hence, type @S@ is first-class with respect to the basic types, working with all existing implicit C mechanisms.
 
 
@@ -121,10 +154,10 @@
 z = "abc";				$\C{// assignment}$
 \end{cfa}
+For type-only, the programmer specifies the initial type, which remains fixed for the variable's lifetime in statically typed languages.
 For type-and-initialization, the specified and initialization types may not agree.
-Similarity, for assignment the current variable and expression types may not agree.
-For type-only, the programmer specifies the initial type, which remains fixed for the variable's lifetime in statically typed languages.
-In the other cases, the compiler may select the type by melding programmer and context information.
+For initialization-only, the compiler may select the type by melding programmer and context information.
 When the compiler participates in type selection, it is called \newterm{type inferencing}.
 Note, type inferencing is different from type conversion: type inferencing \emph{discovers} a variable's type before setting its value, whereas conversion has two typed values and performs a (possibly lossy) action to convert one value to the type of the other variable.
+Finally, for assignment, the current variable and expression types may not agree.
 
 One of the first and powerful type-inferencing system is Hindley--Milner~\cite{Damas82}.
@@ -147,11 +180,11 @@
 \end{cfa}
 In both overloads of @f@, the type system works from the constant initializations inwards and/or outwards to determine the types of all variables and functions.
-Note, like template meta-programming, there could be a new function generated for the second @f@ depending on the types of the arguments, assuming these types are meaningful in the body of the @f@.
+Note, like template meta-programming, there could be a new function generated for the second @f@ depending on the types of the arguments, assuming these types are meaningful in the body of @f@.
 Inferring type constraints, by analysing the body of @f@ is possible, and these constraints must be satisfied at each call site by the argument types;
 in this case, parametric polymorphism can allow separate compilation.
 In languages with type inferencing, there is often limited overloading to reduce the search space, which introduces the naming problem.
-Return-type inferencing goes in the opposite direction to Hindley--Milner: knowing the type of the result and flowing back through an expression to help select the best possible overloads, and possibly converting the constants for a best match.
-
-In simpler type inferencing systems, such as C/\CC/\CFA, there are more specific usages.
+Note, return-type inferencing goes in the opposite direction to Hindley--Milner: knowing the type of the result and flowing back through an expression to help select the best possible overloads, and possibly converting the constants for a best match.
+
+In simpler type-inferencing systems, such as C/\CC/\CFA, there are more specific usages.
 \begin{cquote}
 \setlength{\tabcolsep}{10pt}
@@ -190,10 +223,10 @@
 This issue is exaggerated with \CC templates, where type names are 100s of characters long, resulting in unreadable error messages.
 \item
-Ensuring the type of secondary variables, always matches a primary variable.
+Ensuring the type of secondary variables, always match a primary variable.
 \begin{cfa}
 int x; $\C{// primary variable}$
 typeof(x) y, z, w; $\C{// secondary variables match x's type}$
 \end{cfa}
-If the type of @x@ changes, the types of the secondary variables correspondingly update.
+If the type of @x@ changes, the type of the secondary variables correspondingly updates.
 \end{itemize}
 Note, the use of @typeof@ is more restrictive, and possibly safer, than general type-inferencing.
@@ -208,5 +241,5 @@
 \section{Type-Inferencing Issues}
 
-Each kind of type-inferencing system has its own set of issues that flow onto the programmer in the form of convenience, restrictions or confusions.
+Each kind of type-inferencing system has its own set of issues that flow onto the programmer in the form of convenience, restrictions, or confusions.
 
 A convenience is having the compiler use its overarching program knowledge to select the best type for each variable based on some notion of \emph{best}, which simplifies the programming experience.
@@ -227,8 +260,8 @@
 In Haskell, it is common for programmers to brand (type) function parameters.
 
-A confusion is large blocks of code where all declarations are @auto@.
+A confusion is large blocks of code where all declarations are @auto@, as is now common in \CC.
 As a result, understanding and changing the code becomes almost impossible.
 Types provide important clues as to the behaviour of the code, and correspondingly to correctly change or add new code.
-In these cases, a programmer is forced to re-engineer types, which is fragile, or rely on a fancy IDE that can re-engineer types.
+In these cases, a programmer is forced to re-engineer types, which is fragile, or rely on a fancy IDE that can re-engineer types for them.
 For example, given:
 \begin{cfa}
@@ -243,10 +276,11 @@
 In this situation, having the type name or its short alias is essential.
 
-\CFA's type system tries to prevent type-resolution mistakes by relying heavily on the type of the left-hand side of assignment to pinpoint the right types within an expression.
+The \CFA's type system tries to prevent type-resolution mistakes by relying heavily on the type of the left-hand side of assignment to pinpoint the right types within an expression.
 Type inferencing defeats this goal because there is no left-hand type.
 Fundamentally, type inferencing tries to magic away variable types from the programmer.
 However, this results in lazy programming with the potential for poor performance and safety concerns.
 Types are as important as control-flow in writing a good program, and should not be masked, even if it requires the programmer to think!
-A similar issue is garbage collection, where storage management is masked, resulting in poor program design and performance.
+A similar issue is garbage collection, where storage management is magicked away, often resulting in poor program design and performance.\footnote{
+There are full-time Java consultants, who are hired to find memory-management problems in large Java programs.}
 The entire area of Computer-Science data-structures is obsessed with time and space, and that obsession should continue into regular programming.
 Understanding space and time issues are an essential part of the programming craft.
