Index: doc/theses/jiada_liang_MMath/intro.tex
===================================================================
--- doc/theses/jiada_liang_MMath/intro.tex	(revision aa14aafea1bae6cc4de02b4744e9d067c47d6d05)
+++ doc/theses/jiada_liang_MMath/intro.tex	(revision a35e34220bcc3a0cc1bb85804bab226c7523800f)
@@ -235,14 +235,27 @@
 % 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. 
-% \begin{cfa}
-% void foo( void );
-% struct unit {} u;	$\C[1.5in]{// empty type}$
-% unit bar( unit );
-% foo( @foo()@ );		$\C{// void argument does not match with void parameter}$
-% bar( bar( u ) );	$\C{// unit argument does match with unit parameter}\CRT$
-% \end{cfa}
-
-For example, in the Haskell ADT:
+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:
+\begin{cfa}
+void foo( void );
+foo( @foo()@ );		$\C{// void argument does not match with void parameter}$
+\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.
+
+In the Haskell ADT:
 \begin{haskell}
 data Week = Mon | Tue | Wed | Thu | Fri | Sat | Sun deriving(Enum, Eq, Show)