Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 37336432e480af0a98b3e9b190180eb083f90f82)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision dcfcf368f79594eb9cffea05e52b6e6ca5967954)
@@ -71,4 +71,6 @@
 char * s = label( O_TRUNC );			$\C{// "O\_TRUNC"}$
 int open = posn( O_WRONLY );			$\C{// 1}$
+s = label( mode );						$\C{// "O\_RDONLY"}$
+int open = posn( mode );				$\C{// 0}$
 \end{cfa}
 Equality and relational operations are available.
@@ -131,40 +133,33 @@
 calling constructors happens at runtime (dynamic).
 
+
 \section{Implementation}
-\CFA-cc is is a transpiler that translates \CFA code into C, which can later be compiled by a C compiler.
-
-During the transpilation, \CFA-cc breaks a \CFA enumeration definition into a definition of a C enumeration with the same name and auxiliary arrays: a label array and a value array for a typed enumeration.
+
+\CFA-cc is is a transpiler translating \CFA code into C, which is compiled by a C compiler.
+During transpilation, \CFA-cc breaks a \CFA enumeration definition into a definition of a C enumeration with the same name and auxiliary arrays: a label and value array for a typed enumeration.
 For example:
 \begin{cfa}
-// CFA (source):
-enum(T) E { E1=t1, E2=t2, E3=t3 };
+enum( T ) E { E1 = t1, E2 = t2, E3 = t3 };
 \end{cfa}
 is compiled into:
 \begin{cfa}
-// C (transpiled by cfa-cc):
 enum E { E1, E2, E3 };
-const char * E_labels[3] = { "E1", "E2", "E3" };
-const T E_values [3] = { t1, t2, t3 };
-\end{cfa}
-The generated C enumeration will have enumerator values resemble \CFA enumerator positions thanks to C's auto-initialization scheme.
-A \CFA enumeration variable definition is same in \CFA and C, before or after the transpilation.
-For example:
+static const char * E_labels[3] = { "E1", "E2", "E3" };
+static const T E_values[3] = { t1, t2, t3 };
+\end{cfa}
+The generated C enumeration has enumerator values that match \CFA enumerator positions because of C's auto-initialization.
+A \CFA enumeration variable definition is the same in \CFA as C, \eg:
 \begin{cfa}
 enum E e = E1;
-e;
-\end{cfa}
-These two expressions will not change by \CFA-cc. A \CFA enumeration variable will always have the same underlying representation as its generated 
-C enumeration. This implies \CFA enumeration variable does not take up extra memory and \CFA enumeration use @posn@ as its underlying representation.
-
-Notice that value and label arrays are dynamically allocated data structures that take up 
-memory. If an enumeration is globally defined, the arrays are allocated in the @.data@ section and will be initialized before the program execution.
-Otherwise, if an enumeration has its definition in a local scope, these arrays will be allocated on the stack and be initialized when the program counter 
-reaches the code location of the enumeration definition.
-
-% This bring a considerable overhead to the program, in terms of both execution time and storage. 
-% An opaque enumeration has no overhead 
-% for values, and it has been suggested as a future work to leave as an option to not generate the label array.
-
-Alongs with the enumeration defintion, \CFA-cc adds defintions of attribute functions: @posn@, @label@ and @value@: 
+e = E2;
+\end{cfa}
+so these expressions remain unchanged by \CFA-cc.
+Therefore, a \CFA enumeration variable has the same underlying representation as its generated C enumeration.
+This semantics implies a \CFA enumeration variable does not use memory, that @posn@ can use its underlying representation, and the label and value arrays take little storage.
+It should be possible to eliminated the two arrays if unused, either by \CFA if local to a translation unit and unused, or by the linker if global but unreferenced.
+Also, the label and value arrays are declared @static@ and initialized with constants, so the arrays are allocated in the @.data@ section and initialized before program execution.
+Hence, there is no addition execution cost unless new enumeration features are use, and storage usage is minimal as the number of enumerations in a program is small as is the number of enumerators in an enumeration.
+
+Along with the enumeration definition, \CFA-cc generates definitions of the attribute functions, @posn@, @label@ and @value@, for each enumeration:
 \begin{cfa}
 inline int posn( E e ) { return (int) e; }
@@ -172,14 +167,10 @@
 inline const * E_value( E e ) { return E_values[ (int) e ]; }
 \end{cfa}
-These functions are not implemented in \CFA code: they are Abstract Syntax Tree (AST) nodes appends to the Abstract Syntax Tree (AST).
-Notably, the AST subnode for the "cast to @int@" expression inside the functions is annotated as reinterpreted casts.
-In order words, the effect of a case is only to change the type of an expression, and it stops further reduction on the expression \see{\VRef{s:ValueConversion}}.
-
-Consequently, \CFA enumeration comes with space and runtime overhead, both for enumeration definition and function call to attribute functions. \CFA made efforts to reduce the runtime 
-overhead on function calls by aggressively reducing @label()@ and @value()@ function calls on an enumeration constant to a constant expression. The interpreted casts are extraneous 
-after type checking and removed in later steps. A @label()@ and @value()@ call on an enumeration variable is a lookup of an element of an array of constant values, and it is up to the 
-C compiler to optimize its runtime. While OpaqueEnum is effectively an "opt-out" of the value overhead, it has been suggested that an option to "opt-out" from labels be added as well.
-A @label()@ function definition is still necessary to accomplish enumeration traits. But it will return an empty string for an enumeration label when "opt-out" or the enumerator name 
-when it is called on an enumeration constant. It will allow a user not to pay the overhead for labels when the enumerator names of a particular enumerated type are not helpful.
+where the function calls are normally inlined by the backend C compiler into a few instructions.
+These functions simplify the job of getting the enumerations types through the type system in the same way as normal functions and calls.
+Note, the cast to @int@ is actually an internal reinterpreted cast added before type resolution to stop further reduction on the expression by the type resolver \see{\VRef{s:ValueConversion}} and removed in code generation.
+Finally, to further mitigate \CFA enumeration costs, calls to @label@ and @value@ with an enumeration constant are unrolled into the appropriate constant expression, although this could be left to the backend C compiler.
+Hence, in space and time costs, \CFA enumerations follow the C philosophy of only paying for what is used, modulo some future work to convince the linker to remove unaccessed @label@ and @value@ arrays, possibly with @weak@ attributes.
+
 
 \section{Value Conversion}
@@ -214,5 +205,5 @@
 % \begin{cfa}
 % forall(T | @CfaEnum(T)@) void bar(T);
-% 
+%
 % bar(a);					$\C{// (3), with cost (0, 0, 1, 0, 0, 0, 0, 0)}$
 % \end{cfa}
@@ -236,7 +227,7 @@
 \end{cfa}
 
-The restriction on C's enumeration initializers being constant expression is relaxed on \CFA enumeration. 
-Therefore, an enumerator initializer allows function calls like @?+?( S & s, one_t )@ and @?{}( S & s, zero_t )@. 
-It is because the values of \CFA enumerators are not stored in the compiled enumeration body but in the @value@ array, which 
+The restriction on C's enumeration initializers being constant expression is relaxed on \CFA enumeration.
+Therefore, an enumerator initializer allows function calls like @?+?( S & s, one_t )@ and @?{}( S & s, zero_t )@.
+It is because the values of \CFA enumerators are not stored in the compiled enumeration body but in the @value@ array, which
 allows dynamic initialization.
 
@@ -249,5 +240,5 @@
 \end{cfa}
 Enumeration @Greek@ may have more or less enumerators than @Letter@, but its enumerator values \emph{must} be from @Letter@.
-Therefore, the set of @Greek@ enumerator values in a subset of the @Letter@ enumerator values. 
+Therefore, the set of @Greek@ enumerator values in a subset of the @Letter@ enumerator values.
 @Letter@ is type compatible with enumeration @Letter@ because value conversions are inserted whenever @Letter@ is used in place of @Greek@.
 \begin{cfa}
@@ -291,5 +282,5 @@
 However, the position of the underlying representation is the order of the enumerator in the new enumeration.
 \begin{cfa}
-enum() E1 { B };									$\C{// B}$						
+enum() E1 { B };									$\C{// B}$
 enum() E2 { C, D };						$\C{// C D}$
 enum() E3 { inline E1, inline E2, E };	$\C{// {\color{red}[\(_{E1}\)} B {\color{red}]} {\color{red}[\(_{E2}\)} C D {\color{red}]} E}$
@@ -298,7 +289,7 @@
 In the example, @B@ is at position 0 in @E1@ and @E3@, but position 1 in @E4@ as @A@ takes position 0 in @E4@.
 @C@ is at position 0 in @E2@, 1 in @E3@, and 2 in @E4@.
-@D@ is at position 1 in @E2@, 2 in @E3@, and 3 in @E4@. 
-
-A subtype enumeration can be casted, or implicitly converted into its supertype, with a @safe@ cost, called \newterm{enumeration conversion}. 
+@D@ is at position 1 in @E2@, 2 in @E3@, and 3 in @E4@.
+
+A subtype enumeration can be casted, or implicitly converted into its supertype, with a @safe@ cost, called \newterm{enumeration conversion}.
 \begin{cfa}
 enum E2 e2 = C;
Index: doc/theses/jiada_liang_MMath/Cenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/Cenum.tex	(revision 37336432e480af0a98b3e9b190180eb083f90f82)
+++ doc/theses/jiada_liang_MMath/Cenum.tex	(revision dcfcf368f79594eb9cffea05e52b6e6ca5967954)
@@ -22,7 +22,4 @@
 \VRef[Figure]{f:EnumeratorVisibility} shows how resolution, qualification, and casting are used to disambiguate situations for enumerations @E1@ and @E2@.
 
-Aside, name shadowing in \CFA only happens when a name has been redefined with the exact same type. Because an enumeration define its type and enumerators in one definition,
-and enumeration cannot be changed afterward, shadowing an enumerator is not possible (it is impossible to have another @First@ with same type @E1@.).
-
 \begin{figure}
 \begin{cfa}
@@ -43,4 +40,7 @@
 \label{f:EnumeratorVisibility}
 \end{figure}
+
+Aside, name shadowing in \CFA only happens when a name has been redefined with the \emph{exact} same type.
+Because an enumeration define its type and enumerators in one definition, shadowing an enumerator is not possible, \ie it is impossible to have another @First@ with same type @E1@.
 
 
@@ -68,4 +68,5 @@
 \end{cfa}
 As in Section~\ref{s:CVisibility}, opening multiple scoped enumerations in a @with@ can result in duplicate enumeration names, but \CFA implicit type resolution and explicit qualification/casting handle this localized scenario.
+
 
 \section{Type Safety}
Index: doc/theses/jiada_liang_MMath/background.tex
===================================================================
--- doc/theses/jiada_liang_MMath/background.tex	(revision 37336432e480af0a98b3e9b190180eb083f90f82)
+++ doc/theses/jiada_liang_MMath/background.tex	(revision dcfcf368f79594eb9cffea05e52b6e6ca5967954)
@@ -15,5 +15,5 @@
 \item
 For @#define@, the programmer must explicitly manage the constant name and value.
-Furthermore, these C preprocessor macro names are outside the C type system and can unintentionally change semantics of a program.
+Furthermore, these C preprocessor macro names are outside the C type system and can unintentionally change program text.
 \item
 The same explicit management is true for the @const@ declaration, and the @const@ variable cannot appear in constant-expression locations, like @case@ labels, array dimensions,\footnote{
@@ -136,9 +136,26 @@
 A ``plain'' @int@ object has the natural size suggested by the architecture of the execution environment (large enough to contain any value in the range @INT_MIN@ to @INT_MAX@ as defined in the header @<limits.h>@).~\cite[\S~6.2.5(5)]{C11}
 \end{quote}
-However, @int@ means 4 bytes on both 32/64-bit architectures, which does not seem like the ``natural'' size for a 64-bit architecture.
-% Whereas @long int@ means 4 bytes on a 32-bit and 8 bytes on 64-bit architectures, and @long long int@ means 8 bytes on both 32/64-bit architectures, where 64-bit operations are simulated on 32-bit architectures.
+\VRef[Table]{t:IntegerStorageSizes} shows integer storage sizes.
+On UNIX systems (LP64), @int@ means 4 bytes on both 32/64-bit architectures, which does not seem like the ``natural'' size for a 64-bit architecture.
+Whereas @long int@ means 4 bytes on a 32-bit and 8 bytes on 64-bit architectures, and @long long int@ means 8 bytes on both 32/64-bit architectures, where 64-bit operations are simulated on 32-bit architectures.
+On Windows systems (LLP64), @int@ and @long@ mean 4 bytes on both 32/64-bit architectures, which also does not seem like the ``natural'' size for a 64-bit architecture.
 \VRef[Figure]{f:gccEnumerationStorageSize} shows both @gcc@ and @clang@ partially ignore this specification and type the integral size of an enumerator based on its initialization.
 Hence, initialization in the range @INT_MIN@..@INT_MAX@ results in a 4-byte enumerator, and outside this range, the enumerator is 8 bytes.
 Note that @sizeof( typeof( IMin ) ) != sizeof( E )@, making the size of an enumerator different than its containing enumeration type, which seems inconsistent.
+
+\begin{table}
+\centering
+\caption{Integer Storage Sizes (bytes)}
+\label{t:IntegerStorageSizes}
+\begin{tabular}{@{}rcc@{}}
+Type				& LP64	& LLP64	\\
+@char@				& 1		& 1		\\
+@short@ @int@		& 2		& 2		\\
+@int@				& 4		& 4		\\
+@long@ @int@		& 8		& 4		\\
+@long@ @long@ @int@	& 8		& 8		\\
+pointer				& 8		& 8
+\end{tabular}
+\end{table}
 
 \begin{figure}
@@ -483,6 +500,6 @@
 More type assertions mean more constraints on argument types, making the function less generic.
 
-\CFA defines two special cost values: @zero@ and @infinite@.
-A conversion cost is @zero@ when the argument and parameter have an exact match, and a conversion cost is @infinite@ when there is no defined conversion between the two types.
+\CFA defines two special cost values: 0 and @infinite@.
+A conversion cost is 0 when the argument and parameter have an exact match, and a conversion cost is @infinite@ when there is no defined conversion between the two types.
 For example, the conversion cost from @int@ to a @struct S@ is @infinite@.
 
Index: doc/theses/jiada_liang_MMath/intro.tex
===================================================================
--- doc/theses/jiada_liang_MMath/intro.tex	(revision 37336432e480af0a98b3e9b190180eb083f90f82)
+++ doc/theses/jiada_liang_MMath/intro.tex	(revision dcfcf368f79594eb9cffea05e52b6e6ca5967954)
@@ -39,8 +39,8 @@
 For example, the week, the weekdays, the weekend, and every second day of the week.
 \begin{cfa}[morekeywords={in}]
-for ( cursor in Mon, Tue, Wed, Thu, Fri, Sat, Sun } ... $\C[3.75in]{// week}$
-for ( cursor in Mon, Tue, Wed, Thu, Fri } ...	$\C{// weekday}$
-for ( cursor in Sat, Sun } ...					$\C{// weekend}$
-for ( cursor in Mon, Wed, Fri, Sun } ...		$\C{// every second day of week}\CRT$
+for ( cursor in Mon, Tue, Wed, Thu, Fri, Sat, Sun ) ... $\C[3.75in]{// week}$
+for ( cursor in Mon, Tue, Wed, Thu, Fri ) ...	$\C{// weekday}$
+for ( cursor in Sat, Sun ) ...					$\C{// weekend}$
+for ( cursor in Mon, Wed, Fri, Sun ) ...		$\C{// every second day of week}\CRT$
 \end{cfa}
 A set can have a partial or total ordering, making it possible to compare set elements, \eg Monday is before Tuesday and Tuesday is after.
@@ -73,5 +73,5 @@
 
 The term \newterm{enumeration} defines a type with a set of new constants, and the term \newterm{enumerator} represents an arbitrary alias name \see{\VRef{s:CEnumeration} for the name derivations}.
-An enumerated type can have three fundamental properties, \newterm{label} (name), \newterm{order} (position), and \newterm{value} (payload).
+An enumerated type can have the following properties: \newterm{label} (name), \newterm{order} (position), and \newterm{value} (payload).
 \begin{cquote}
 \sf\setlength{\tabcolsep}{3pt}
@@ -234,11 +234,24 @@
 % The association between ADT and enumeration occurs if all the constructors have a unit (empty) type, \eg @struct unit {}@.
 % Note, the unit type is not the same as \lstinline{void}.
-In terms of functional programming linguistics, enumerations often refers to a @unit type@ ADT, where @unit type@ is a type 
-that carry no information. The unit type is different than @void@ in C, because @void@ is type has no value, i.e., it is a empty set.
-In constract, unit type has exactly one value, often called a @nil@ value. 
-Because of this distinction, it is not possbile to have a variable to have type @void@ or to be assigned with a value @void@. 
-In practice, @void@ in C is more like an annotation that nothing is expected in this place. A function takes @void@ as parameter 
-is essentially a function that expects no parameter. A function that return @void@ cannot be used as a parameter of a function that expects no 
-parameter. Therefore, the following code is illegal in C:
+In terms of functional programming linguistics, enumerations often refer to a @unit type@ ADT, which is a set with the @nil@ value carrying no information.
+The unit type is different from type @void@ in C, because @void@ has no value, which is an empty set.
+Hence, @void@ is a C annotation that nothing is expected in this place.
+For example, a function that takes a @void@ parameter and returns a @void@ is a function that expects no parameters and returns nothing.
+\begin{cfa}
+void foo( void );
+foo(); $\C{// no arguments and no result}$
+\end{cfa}
+Because of this distinction, it is impossible to have a variable of type @void@, to assign a @void@ value, or have a function taking and returning multiple @void@s.
+\begin{cfa}
+void v; 		$\C{// disallowed}$
+v = void;
+[ void, void ] bar( void, void );
+\end{cfa}
+Programming languages often use an empty parameter list to imply no value and no return type for empty return.
+\begin{cfa}
+[] bar(); $\C{// \CFA empty/empty prototype}$
+\end{cfa}
+However, C is saddled with an empty parameter list meaning a list of unknown type parameters, \ie @var_arg@, which is changed to @void@ in \CC/\CFA.
+As a result, a function that returns @void@ cannot be used as a parameter of a function that expects no parameter.
 \begin{cfa}
 void foo( void );
@@ -246,14 +259,13 @@
 \end{cfa}
 
-This is a more notably issue when to use @variant@ to simulate @ADT@: @void@ cannot be used as an empty variant. To solve this problem, 
-\CC introduced @monstate@, a type that can be instantiated as a value, but holds no information. There is no standard representation of 
-@unit@ in C, and it is often approximated by a user-defined type that has no field, for example:
-\begin{cfa}
-struct Empty {} e;		$\C{// empty type}$
-Empty bar( Empty );
-bar(@bar(e)@);
-\end{cfa}
-@Empty@ is a close approximation to @unit@ if and only if @Empty@ is the only representation of @unit@ in the program. If a program has 
-a second type, say @Nothing@, that also tries to resemble @unit@, then @unit@ concepts falls apart.
+This issue arose when simulating an ADT using a \CC @variant@: @void@ cannot be used as an empty variant.
+To solve this problem, \CC introduced @std::monstate@~\cite{C++monstate}, a type that can be instantiated as a value but holds no information.
+A similar approximation in C is to define a @struct@ type with no fields.
+\begin{cfa}
+struct Unit {} e;		$\C{// empty type}$
+Unit bar( Unit );
+bar( @bar( e )@ );
+\end{cfa}
+Because @std::monostate@ and @Unit@ are user-defined types versus part of the type system, they are only an approximation to @unit@ because other @unit@ types can be defined.
 
 In the Haskell ADT:
Index: doc/theses/jiada_liang_MMath/relatedwork.tex
===================================================================
--- doc/theses/jiada_liang_MMath/relatedwork.tex	(revision 37336432e480af0a98b3e9b190180eb083f90f82)
+++ doc/theses/jiada_liang_MMath/relatedwork.tex	(revision dcfcf368f79594eb9cffea05e52b6e6ca5967954)
@@ -336,4 +336,5 @@
 \end{c++}
 whereas C @const@ declarations without @static@ are marked @R@.
+This difference results from linking concerns that come from templates.
 
 The following \CC non-backward compatible change is made, plus the safe-assignment change shown in~\VRef{s:TypeSafety}.
@@ -417,5 +418,5 @@
 A common workaround is to iterate over enumerator as integral values, but it only works if 
 enumerators resemble a sequence of natural, i.e., enumerators are auto-initialized.
-Otherwises, the iteration would have integers that are not enumeration values.
+Otherwise, the iteration would have integers that are not enumeration values.
 \begin{c++}
 enum Week { Mon, Tue, Wed, Thu = 10, Fri, Sat, Sun };
@@ -497,8 +498,9 @@
 To indirectly enumerate, \Csharp's Enum library provides @Enum.GetValues@, 
 % a pseudo-method that retrieves an array of the enumeration constants for looping over an enumeration type or variable (expensive operation).
-a static memeber of abstract Enum type that return a reference to an array of all enumeration constants.
-Internally, a Enum type has a static member called @fieldInfoHash@, a @Hashtable@ that stores enumerators information. The field is populated on-demand: 
-it only contains information if a @reflection@ like @GetValues@ is called. But the information will be cached, so the cost of reflection is paid only 
-once throughout the lifetime of a program. @GetValues@ then converts a @Hashtable@ to an @Array@, which supports enumerating.
+a static member of abstract Enum type that return a reference to an array of all enumeration constants.
+Internally, a Enum type has a static member called @fieldInfoHash@ -- a @Hashtable@ that stores enumerators information.
+The field is populated on-demand: it only contains information if a @reflection@ like @GetValues@ is called.
+As an optimization, this information is cached, so the cost of reflection is paid once throughout the lifetime of a program.
+@GetValues@ then converts a @Hashtable@ to an @Array@, which supports enumerating.
 \begin{csharp}
 foreach ( Week d in @Enum.GetValues@( typeof(Week) ) ) {
@@ -507,5 +509,5 @@
 Mon 0, Tue 1, Wed 2, Thu 10, Fri 11, Sat 12, Sun 13,
 \end{csharp}
-Hence, enumerating is not supplied directly by the enumeration, but indirectly through the enumerable array type.
+Hence, enumerating is not supplied directly by the enumeration, but indirectly through the expensive $O(N)$ creation of an enumerable array type, and recreating this array for each enumerating, versus direct arithmetic.
 
 An enumeration type cannot declare an array dimension but an enumerator can be used as a subscript.
@@ -529,5 +531,5 @@
 Go has @const@ aliasing declarations, similar to \CC \see{\VRef{s:C++RelatedWork}}, for basic types with type inferencing and static initialization (constant expression).
 The most basic form of constant definition is a @const@ keyword, followed by the name of constant, an optional type declaration of the constant, and a mandatory initialize.
-For exmaple:
+For example:
 \begin{Go}
 const R @int@ = 0;  const G @uint@ = 1;  const B = 2; $\C{// explicit typing and type inferencing}$
@@ -541,5 +543,5 @@
 
 % Go provides an enumeration-like feature to group together @const@ declaration into a block and introduces a form of auto-initialization.
-These named constants can be grouped together in one @const@ declaration block and introduces a form of auto-initialization.
+These named constants can be grouped together in one @const@ declaration block to introduce a form of auto-initialization.
 \begin{Go}
 const ( R = 0; G; B )					$\C{// implicit initialization: 0 0 0}$
@@ -550,71 +552,52 @@
 subsequent identifiers can be implicitly or explicitly initialized.
 Implicit initialization always uses the \emph{previous} (predecessor) constant expression initializer.
-
-% Each @const@ declaration provides an implicit integer counter starting at zero, called \lstinline[language=Go]{iota}.
-Each const declaration is often paired with a const expression \lstinline[language=Go]{iota} to re-define its 
-implicit initialization. \lstinline[language=Go]{iota} represents an sequence of natural number starting from zero.
-Every implicit or explicit \lstinline[language=Go]{iota} increments the value of the expression by one.
-Using \lstinline[language=Go]{iota} outside of a @const@ block always sets the identifier to zero.
+A constant block can still use explicit declarations, and following constants inherit that type.
 \begin{Go}
-const R = iota;							$\C{// 0}$
+type BigInt int64
+const ( R @BigInt@ = 0; G; B )
+const ( Fred @string@ = "Fred"; Mary = "Mary"; Jane = "Jane" )
+const ( S @int@ = 0; T; USA @string@ = "USA"; U; V @float32@ = 3.1; W )
 \end{Go}
+Typing the first constant and implicit initializing is still not a enumeration because there is no unique type for the constant block;
+nothing stops other constant blocks from having the same type. 
+
+Each @const@ declaration provides an implicit \emph{compile-time} integer counter starting at @0@, called \lstinline[language=Go]{iota}, which is post-incremented after each constant declaration.
+% Each @const@ declaration is often paired with a const expression \lstinline[language=Go]{iota} to re-define its implicit initialization.
+% \lstinline[language=Go]{iota} represents a sequence of natural numbers starting from zero.
+% Using \lstinline[language=Go]{iota} outside of a @const@ block always sets the identifier to zero.
+% \begin{Go}
+% const R = iota;							$\C{// 0}$
+% \end{Go}
 % Inside a @const@ block, \lstinline[language=Go]{iota} is implicitly incremented for each \lstinline[language=golang]{const} identifier and used to initialize the next uninitialized identifier.
-Inside a @const@ block, if a constant has \lstinline[language=Go]{iota} initializer, its successor will also use \lstinline[language=Go]{iota} initializer.
-\lstinline[language=Go]{iota} is no different than other constant expression when it is used in implicit initialization, but 
-thanks to the increment natural of \lstinline[language=Go]{iota}, the successor will have a value equal to its predecessor plus 1.
+% Inside a @const@ block, if a constant has \lstinline[language=Go]{iota} initializer, its successor will also use \lstinline[language=Go]{iota} initializer.
+% Inside a @const@ block, if a constant has \lstinline[language=Go]{iota} initializer, its successor will also use \lstinline[language=Go]{iota} initializer.
+% \lstinline[language=Go]{iota} is no different than other constant expression when it is used in implicit initialization, but thanks to the increment natural of \lstinline[language=Go]{iota}, the successor will have a value equal to its predecessor plus 1.
 \begin{Go}
-const ( R = @iota@; G; B )				$\C{// implicit: 0 1 2}$
-% const ( C = @iota + B + 1@; G; Y )		$\C{// implicit: 3 4 5}$
+const ( R = @iota@; G; B )					$\C{// implicit: 0 1 2}$
+const ( C = @iota + B + 1@; G; Y )			$\C{// implicit: 3 4 5}$
 \end{Go}
-The constant blocks from the previous example is equivalanet to:
+which are equivalent to:
 \begin{Go}
-const ( R = @iota@; G=@iota@; B=@iota@ )				$\C{// implicit: 0 1 2}$
+const ( R = @iota@; G = @iota@; B = @iota@ ) $\C{// implicit: 0 1 2}$
+const ( C = @iota + B + 1@; G = @iota + B + 1@; Y = @iota + B + 1@ ) $\C{// implicit: 3 4 5}$
 \end{Go}
-R, G, B have values 0, 1, 2, respectively, because \lstinline[language=Go]{iota} is an increasing.
-
-Similarly, 
+An underscore \lstinline[language=golang]{const} identifier advances \lstinline[language=Go]{iota}.
 \begin{Go}
-const ( C = @iota + B + 1@; G; Y )		$\C{// implicit: 3 4 5}$
+const ( O1 = iota + 1; @_@; O3; @_@; O5 )	$\C{// 1, 3, 5}$
 \end{Go}
-can be rewritten as:
+Auto-initialization reverts from \lstinline[language=Go]{iota} to the previous value after an explicit initialization, but auto-incrementing of \lstinline[language=Go]{iota} continues.
 \begin{Go}
-const ( C = @iota + B + 1@; G = @iota + B + 1@; Y = @iota + B + 1@ )		$\C{// implicit: 3 4 5}$
+const ( Mon = iota; Tue; Wed;				$\C{// 0, 1, 2}$
+		 @Thu = 10@; Fri; Sat; @Sun = iota@ ) $\C{// 10, 10, 10, {\color{red}6}}$
 \end{Go}
-Go's grouped constants do not define a new type, and constants in the same block can have heterogeneous types. 
-These two characteristics differs a grouped constant from an enumeration, but also gives a direction on approximating enumeration in Go:
-first to define a new type externally, and make sure all constants in the same group will have the new type.
+Auto-initialization from \lstinline[language=Go]{iota} is restarted and \lstinline[language=Go]{iota} reinitialized with an expression containing at most \emph{one} \lstinline[language=Go]{iota}.
 \begin{Go}
-type Language int64
-const (
-	C Language = iota
-	CPP
-	CSharp
-	CFA
-	Go
-)
+const ( V1 = iota; V2; @V3 = 7;@ V4 = @iota@ + 1; V5 ) // 0 1 7 4 5
+const ( Mon = iota; Tue; Wed; // 0, 1, 2
+		@Thu = 10;@ Fri = @iota@ - Wed + Thu - 1; Sat; Sun ) // 10, 11, 12, 13
 \end{Go}
-By typing the first constant as @Language@ and assigning initializer with \lstinline[language=Go]{iota}, all other constants will have the same type 
-and the same initialzer. It is a close approximation, but it is not a real enumeration. The definition of the "enumerated type" is separate from 
-the "enumerator definition", and nothing stop outside constants to have the type @Language@. 
-
-% An underscore \lstinline[language=golang]{const} identifier advances \lstinline[language=Go]{iota}.
-% \begin{Go}
-% const ( O1 = iota + 1; @_@; O3; @_@; O5 ) // 1, 3, 5 
-% \end{Go}
-% Auto-initialization reverts from \lstinline[language=Go]{iota} to the previous value after an explicit initialization, but auto-incrementing of \lstinline[language=Go]{iota} continues.
-% \begin{Go}
-% const ( Mon = iota; Tue; Wed; // 0, 1, 2
-% 		@Thu = 10@; Fri; Sat; @Sun = itoa@ ) $\C{// 10, 10, 10, {\color{red}6}}$
-% \end{Go}
-% Auto-initialization from \lstinline[language=Go]{iota} is restarted and \lstinline[language=Go]{iota} reinitialized with an expression containing at most \emph{one} \lstinline[language=Go]{iota}.
-% \begin{Go}
-% const ( V1 = iota; V2; @V3 = 7;@ V4 = @iota@ + 1; V5 ) // 0 1 7 4 5
-% const ( Mon = iota; Tue; Wed; // 0, 1, 2
-% 		@Thu = 10;@ Fri = @iota@ - Wed + Thu - 1; Sat; Sun ) // 10, 11, 12, 13
-% \end{Go}
-% Here, @V4@ and @Fri@ restart auto-incrementing from \lstinline[language=Go]{iota} and reset \lstinline[language=Go]{iota} to 4 and 11, respectively, because of the initialization expressions containing \lstinline[language=Go]{iota}.
-% Note, because \lstinline[language=Go]{iota} is incremented for an explicitly initialized identifier or @_@,
-% at @Fri@ \lstinline[language=Go]{iota} is 4 requiring the minus one to compute the value for @Fri@.
-
+Here, @V4@ and @Fri@ restart auto-incrementing from \lstinline[language=Go]{iota} and reset \lstinline[language=Go]{iota} to 4 and 11, respectively, because of the initialization expressions containing \lstinline[language=Go]{iota}.
+Note, because \lstinline[language=Go]{iota} is incremented for an explicitly initialized identifier or @_@,
+at @Fri@ \lstinline[language=Go]{iota} is 4 requiring the minus one to compute the value for @Fri@.
 
 Basic switch and looping are possible.
@@ -660,5 +643,5 @@
 Week day = Week.Sat;
 \end{Java}
-The enumerator's members are scoped and requires qualification.
+The enumerator's members are scoped requiring qualification.
 The value of an enumeration instance is restricted to its enumerators.
 
@@ -724,6 +707,7 @@
 
 There are no arithmetic operations on enumerations, so there is no arithmetic way to iterate through an enumeration without making the implementation type \lstinline[language=Java]{public}.
-Like \Csharp, looping over an enumeration is done using static method @values@, which returns an array of enumerator values.
-Unfortunately, @values@ is an expensive @O(n)@ operation because it creates a new array every time it is called. 
+Like \Csharp, enumerating is supplied indirectly through another enumerable type, not via the enumeration.
+Specifically, Java supplies a static method @values@, which returns an array of enumerator values.
+Unfortunately, @values@ is an expensive @O(n)@ operation, which is recreated each time it is called. 
 \begin{Java}
 for ( Week d : Week.values() ) {
@@ -732,16 +716,15 @@
 0 1 Mon,  1 2 Tue,  2 3 Wed,  3 4 Thu,  4 5 Fri,  5 6 Sat,  6 7 Sun,  
 \end{Java}
-Like \Csharp, enumerating is supplied indirectly through another enumerable type, not via the enumeration.
 
 % Java provides an @EnumSet@ where the underlying type is an efficient set of bits, one per enumeration \see{\Csharp \lstinline{Flags}, \VRef{s:Csharp}}, providing (logical) operations on groups of enumerators.
 % There is also a specialized version of @HashMap@ with enumerator keys, which has performance benefits.
-Java provides @EnumSet@, an auxiliary data structure that takes an enum @class@ as parameter (Week.class) for its construction, and it contains members only with the supplied 
-enum type. @EnumSet@ is enumerable because it extends @AbstractSet@ interfaces and thus supports direct enumerating via @forEach@. It also has subset operation 
-@range@ and it is possible to add to and remove from members of the set. 
+Java provides @EnumSet@, an auxiliary data structure that takes an enum @class@ as parameter (Week.class) for its construction, and it contains members only with the supplied enum type.
+@EnumSet@ is enumerable because it extends @AbstractSet@ interfaces and thus supports direct enumerating via @forEach@.
+It also has subset operation @range@ and it is possible to add to and remove from members of the set. 
 @EnumSet@ supports more enumeration features, but it is not an enumeration type: it is a set of enumerators from a pre-define enum. 
-
 
 An enumeration type cannot declare an array dimension nor can an enumerator be used as a subscript.
 Enumeration inheritence is disallowed because an enumeration is \lstinline[language=Java]{final}.
+
 
 \section{Rust}
@@ -857,6 +840,6 @@
 \end{cquote}
 % However, there is no mechanism to iterate through an enumeration without casting to integral and positions versus values is not handled.
-Like C/\CC, there is no mechanism to iterate through an enumeration. It can only be approximated 
-by a loop over a range of enumerator and will not work if enumerator values is a sequence of natural numbers.
+Like C/\CC, there is no mechanism to iterate through an enumeration.
+It can only be approximated by a loop over a range of enumerator and only works if the enumerator values are a sequence of natural numbers.
 \begin{c++}
 for d in Week::Mon as isize ..= Week::Sun as isize {
@@ -866,6 +849,6 @@
 \end{c++}
 % An enumeration type cannot declare an array dimension nor as a subscript.
-There is no direct way to harmonize an enumeration and another data structure. For example, 
-there is no mapping from an enumerated type to an array type.
+There is no direct way to harmonize an enumeration and another data structure.
+For example, there is no mapping from an enumerated type to an array type.
 In terms of extensibility, there is no mechanism to subset or inherit from an enumeration.
 
@@ -874,5 +857,5 @@
 \label{s:Swift}
 % https://www.programiz.com/swift/online-compiler
-Despite being named as enumeration, A Swift @enum@ is in fact a ADT: cases (enumerators) of an @enum@ can have heterogeneous types and be recursive.
+Despite being named as enumeration, a Swift @enum@ is in fact a ADT: cases (enumerators) of an @enum@ can have heterogeneous types and be recursive.
 % Like Rust, Swift @enum@ provides two largely independent mechanisms from a single language feature: an ADT and an enumeration.
 When @enum@ is an ADT, pattern matching is used to discriminate among the variant types.
@@ -917,10 +900,10 @@
 \end{tabular}
 \end{cquote}
-% Note, after an @adt@'s type is know, the enumerator is inferred without qualification, \eg @.I(3)@.
-Normally an enumeration case needs a type qualification. But in the example when pattern matching @adt@, which 
-has a type @ADT@, the context provides that the cases refer to @ADT@'s cases and no explicit type qualification is required. 
+Note, after an @adt@'s type is known, the enumerator is inferred without qualification, \eg @.I(3)@.
+% Normally an enumeration case needs a type qualification.
+%However, when pattern matching @adt@ of type @ADT@, the @case@ context provides the type @ADT@ so no explicit type qualification is required. 
 
 % An enumeration is created when \emph{all} the enumerators are unit-type, which is like a scoped, opaque enumeration.
-Without type declaration for enumeration cases, a Swift enum syntax defined a unit-type enumeration, which is like a scoped, opaque enumeration.
+Without type declaration for enumeration cases, the enumerators have unit-type, which is like a scoped, opaque enumeration.
 \begin{swift}
 enum Week { case Mon, Tue, Wed, Thu, Fri, Sat, Sun }; // unit-type
@@ -929,7 +912,7 @@
 % As well, it is possible to type \emph{all} the enumerators with a common type, and set different values for each enumerator;
 % for integral types, there is auto-incrementing.
-As well, it is possible to type associated values of enumeration cases with a common types. 
+As well, it is possible to type associated values of enumeration cases with a common type. 
 When enumeration cases are typed with a common integral type, Swift auto-initialize enumeration cases following the same initialization scheme as C language.
-If enumeration is typed with @string@, its cases are auto-initialized to case names (labels).
+If an enumeration is typed with @string@, its cases are auto-initialized to case names (labels).
 \begin{cquote}
 \setlength{\tabcolsep}{15pt}
@@ -981,6 +964,5 @@
 \end{tabular}
 \end{cquote}
-Enumerating is accomplished by inheriting from @CaseIterable@ protocol, which has a static 
-@enum.allCases@ property that returns a collection of all the cases for looping over an enumeration type or variable.
+Enumerating is accomplished by inheriting from @CaseIterable@ protocol, which has a static @enum.@ @allCases@ property that returns a collection of all the cases for looping over an enumeration type or variable.
 Like \CFA, Swift's default enumerator output is the case name (label). An enumerator of a typed enumeration has attribute 
 @rawValue@ that return its case value.
@@ -1032,6 +1014,7 @@
 \end{swift}
 % Conversion from @rawValue@ to enumerator may fail (bad lookup), so the result is an optional value.
-In the previous exmaple, the initialization of @opt@ fails when there is no enumeration cases has value equals 0, resulting in a 
-@nil@ value. Initialization from a raw value is considered a expensive operation because it requires a value lookup.
+In the previous example, the initialization of @opt@ fails if there is no enumeration value equal to 0, resulting in a @nil@ value.
+Initialization from a raw value is considered a expensive operation because it requires a value lookup.
+
 
 \section{Python 3.13}
@@ -1329,4 +1312,13 @@
 However, as stated in the documentation, @enumerate@ PPX does not guarantee the order of the list.
 PPX is beyond the scope of OCaml native language and it is a preprocessor directly modifying a parsed AST. In conclusion, there is no enumerating mechanism within the scope of OCaml language.
+
+\PAB{Why was this removed?}
+Enumeration subsetting is allowed but inheritance is restricted to classes not types.
+\begin{ocaml}
+type weekday = Mon | Tue | Wed | Thu | Fri
+type weekend = Sat | Sun
+type week = Weekday of weekday | Weekend of weekend
+let day : week = Weekend Sun
+\end{ocaml}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Index: doc/theses/jiada_liang_MMath/test.go
===================================================================
--- doc/theses/jiada_liang_MMath/test.go	(revision 37336432e480af0a98b3e9b190180eb083f90f82)
+++ doc/theses/jiada_liang_MMath/test.go	(revision dcfcf368f79594eb9cffea05e52b6e6ca5967954)
@@ -20,6 +20,6 @@
 
 
-const ( R = 0; G = 3; B = 3; TT = 3 ) // implicit: 0 3 3
-const ( Fred = "Fred"; Mary = "Mary"; Jane = "Jane" ) // Fred Mary Jane
+const ( R int = 0; G = 3; B = 3; TT = 3 ) // implicit: 0 3 3
+const ( Fred string = "Fred"; Mary = "Mary"; Jane = "Jane" ) // Fred Mary Jane
 const ( H = 0; Jack = "Jack"; J; K = 0; I ) // type change, implicit: 0 Jack Jack
 const ( C = iota + G; M = iota; Y )
@@ -31,9 +31,11 @@
 const ( D = 1.5; E );
 
-
+const ( AA int = 3; KK; BB float32 = 3.5; CC = 3.9 );
+type BigInt int64
 
 func main() {
 	fmt.Println( "Go:")
 	if 3 == R {};
+	fmt.Println( AA, KK, BB, CC )
 	fmt.Println( R, G, B )
 	fmt.Println( Fred, Mary, Jane )
Index: doc/theses/jiada_liang_MMath/trait.tex
===================================================================
--- doc/theses/jiada_liang_MMath/trait.tex	(revision 37336432e480af0a98b3e9b190180eb083f90f82)
+++ doc/theses/jiada_liang_MMath/trait.tex	(revision dcfcf368f79594eb9cffea05e52b6e6ca5967954)
@@ -120,5 +120,5 @@
 Hence, the \CFA enumeration traits never connected with the specific @enum@ kind.
 Instead, anything that can look like the @enum@ kind is considered an enumeration (static structural typing).
-However, Scala, Go, and Rust traits are nominative: a type explicitly declares a named traits to be of its type, while in \CFA, any type implementing all requirements declared in a trait implicitly satisfy its restrictions.
+However, Scala, Go, and Rust traits are nominative: a type explicitly declares a named trait to be of its type, while in \CFA, any type implementing all requirements declared in a trait implicitly satisfy its restrictions.
 
 One of the key differences between concepts and traits, which is leveraged heavily by \CFA, is the ability to apply new \CFA features to C legacy code.
Index: doc/theses/jiada_liang_MMath/uw-ethesis.bib
===================================================================
--- doc/theses/jiada_liang_MMath/uw-ethesis.bib	(revision 37336432e480af0a98b3e9b190180eb083f90f82)
+++ doc/theses/jiada_liang_MMath/uw-ethesis.bib	(revision dcfcf368f79594eb9cffea05e52b6e6ca5967954)
@@ -12,2 +12,13 @@
     year	= 2023,
 }
+
+@misc{C++monstate,
+    keywords	= {unit type},
+    key		= {monstate},
+    title	= {{\sf std::monostate3}},
+    author	= {cppreference.com},
+    howpublished= {\url{https://en.cppreference.com/w/cpp/utility/variant/monostate}},
+    month	= sep,
+    year	= 2024,
+}
+
