Changes in / [a5e2786f:28c2c9d5]

File:

• doc/theses/fangren_yu_MMath/intro.tex (modified) (10 diffs)

doc/theses/fangren_yu_MMath/intro.tex

@@ -1 +1 @@
 \chapter{Introduction}
 
-This thesis is exploratory work I did to understand, fix, and extend the \CFA type-system, specifically, the \newterm{type-resolver} used to satisfy call-site assertions among overloaded variable and function names to allow polymorphic routine calls.
-Assertions are the operations a function uses within its body to perform its computation.
-For example, a polymorphic function summing an array needs a size, zero, assignment, and plus for the array element-type, and a subscript operation for the array type.
-\begin{cfa}
-T sum( T a[$\,$], size_t size ) {
-        @T@ total = { @0@ };  // size, 0 for type T
-        for ( size_t i = 0; i < size; i += 1 )
-                total @+=@ a@[@i@]@; // + and subscript for T
-        return total;
-}
-\end{cfa}
-In certain cases, if the resolver fails to find an exact assertion match, it attempts to find a \emph{best} match using reasonable type conversions.
-Hence, \CFA follows the current trend of replacing nominal inheritance with traits composed of assertions for type matching.
-The over-arching goal is to push the boundary on localized assertion matching, with advanced overloading resolution and type conversions that match programmer expectations in the C programming language.
-Together, the resulting \CFA type-system has a number of unique features making it different from other programming languages with expressive, static, type-systems.
-
-
-\section{Types}
-
-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 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.
-Expressibility, generalization, and safety are all bound up in a language's type system, and hence, directly affect the capability, build time, and correctness of program development.
-
-
-\section{Overloading}
-
+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.
 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}
@@ -39 +10 @@
 Depending on the language, any ambiguous cases are resolved using some form of qualification and/or casting.
 
-
-\subsection{Operator Overloading}
+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 other programming languages with expressive, static type-systems.
+
+
+\section{Types}
+
+\begin{quote}
+Some are born great, some achieve greatness, and some have greatness thrust upon them. Twelfth Night, Act II Scene 5, William Shakespeare
+\end{quote}
+
+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 the ones provided by the underlying hardware.
+These language types are \emph{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.
+Expressibility, generalization, and safety are all bound up in a language's type system, and hence, directly affect the capability, build time, and correctness of program development.
+
+
+\section{Operator Overloading}
 
 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 maps operators to named functions and allows these operators to be overloaded with user-defined types.
+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 left and right unary operators: @?++@ and @++?@, and binary operators @?+?@ and @?<=?@.
 Here, a user-defined type is extended with an addition operation with the same syntax as builtin types.
@@ -60 +50 @@
 
 
-\subsection{Function Overloading}
+\section{Function Overloading}
 
 Both \CFA and \CC allow function names to be overloaded, as long as their prototypes differ in the number and type of parameters and returns.
@@ -93 +83 @@
 
 
-\subsection{Variable Overloading}
+\section{Variable Overloading}
 
 Unlike most programming languages, \CFA has variable overloading within a scope, along with shadow overloading in nested scopes.
@@ -135 +125 @@
 
 
-\subsection{Constant Overloading}
-
-\CFA is unique in providing restricted constant overloading for the values @0@ and @1@, which have special status in C.
-For example, the value @0@ is both an integer and a pointer literal, so its meaning depends on context.
+\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@.
-For example, @if@ and iteration statements in C compare the condition with @0@, and the increment and decrement operators are semantically equivalent to adding or subtracting the value @1@.
+For example, 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.
 \begin{cfa}
 if ( x ) ++x;        =>    if ( x @!= 0@ ) x @+= 1@;
@@ -149 +138 @@
 \begin{cfa}
 struct S { int i, j; };
-void ?{}( S & s, zero_t ) { s.[i,j] = 0; } $\C{// constant constructors}$
+void ?{}( S & s, zero_t ) { s.[i,j] = 0; } $\C{// constructors}$
 void ?{}( S & s, one_t ) { s.[i,j] = 1; }
-S ?=?( S & dst, zero_t ) { dst.[i,j] = 0; return dst; } $\C{// constant assignments}$
+S ?=?( S & dst, zero_t ) { dst.[i,j] = 0; return dst; } $\C{// assignment}$
 S ?=?( S & dst, one_t ) { dst.[i,j] = 1; return dst; }
 S ?+=?( S & s, one_t ) { s.[i,j] += 1; return s; } $\C{// increment/decrement each field}$
 S ?-=?( S & s, one_t ) { s.[i,j] -= 1; return s; }
-int ?!=?( S s, zero_t ) { return s.i != 0 && s.j != 0; } $\C{// constant comparison}$
+int ?!=?( S s, zero_t ) { return s.i != 0 && s.j != 0; } $\C{// comparison}$
 S s = @0@;                      $\C{// initialization}$
 s = @0@;                        $\C{// assignments}$
 s = @1@;
-if ( @s@ ) @++s@;       $\C{// unary ++/-\,- come implicitly from +=/-=}$
+if ( @s@ ) @++s@;       $\C{// special, unary ++/-\,- come implicitly from +=/-=}$
 \end{cfa}
 Here, type @S@ is first-class with respect to the basic types, working with all existing implicit C mechanisms.
@@ -180 +169 @@
 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.
-Discovering a variable or function type is complex and has limitations.
-The following covers these issues, and why some schemes are not amenable with the \CFA type system.
 
 One of the first and powerful type-inferencing system is Hindley--Milner~\cite{Damas82}.
@@ -261 +248 @@
 
 
-\subsection{Type-Inferencing Issues}
+\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.
@@ -324 +311 @@
 \end{cfa}
 This @identity@ function can be applied to an \newterm{object type}, \ie a type with a known size and alignment, which is sufficient to stack allocate, default or copy initialize, assign, and delete.
-The \CFA implementation passes the size and alignment for each type parameter, as well as auto-generated default and copy constructors, assignment operator, and destructor.
+The \CFA implementation passes the size and alignment for each type parameter, as well as any implicit/explicit constructor, copy constructor, assignment operator, and destructor.
 For an incomplete \newterm{data type}, \eg pointer/reference types, this information is not needed.
 \begin{cfa}
@@ -433 +420 @@
 \end{cfa}
 The implicit routines are used by the @sumable@ operator @?+=?@ for the right side of @?+=?@ and return.
-
-If the array type is not a builtin type, an extra type parameter and assertions are required, like subscripting.
-This case is generalized in polymorphic container-types, such as a list with @insert@ and @remove@ operations, and an element type with copy and assignment.