Index: doc/theses/jiada_liang_MMath/intro.tex
===================================================================
--- doc/theses/jiada_liang_MMath/intro.tex	(revision a35e34220bcc3a0cc1bb85804bab226c7523800f)
+++ 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:
