Index: doc/bibliography/pl.bib
===================================================================
--- doc/bibliography/pl.bib	(revision 75d789c11cb725d1bc4d528dbee9dd7ca666a2e4)
+++ doc/bibliography/pl.bib	(revision 9a32903fc141b4db3380f2b4e3d945f14c51303a)
@@ -5985,4 +5985,15 @@
 }
 
+@manual{Ocaml,
+    keywords	= {OCaml programming language},
+    contributer	= {pabuhr@plg},
+    key		= {OCaml},
+    title	= {The {OC}aml system, release 5.1},
+    optaddress	= {Rust Project Developers},
+    year	= 2023,
+    note	= {\url{https://v2.ocaml.org/manual/}},
+}
+
+
 @book{Galletly96,
     keywords	= {occam},
Index: doc/theses/jiada_liang_MMath/relatedwork.tex
===================================================================
--- doc/theses/jiada_liang_MMath/relatedwork.tex	(revision 75d789c11cb725d1bc4d528dbee9dd7ca666a2e4)
+++ doc/theses/jiada_liang_MMath/relatedwork.tex	(revision 9a32903fc141b4db3380f2b4e3d945f14c51303a)
@@ -2463,25 +2463,42 @@
 
 \section{OCaml}
-\lstnewenvironment{ocaml}[1][]{\lstset{language=ML,escapechar=\$,moredelim=**[is][\color{red}]{@}{@},}\lstset{#1}}{}
-
-An enumerated data types is a list of named values.
+\lstnewenvironment{ocaml}[1][]{\lstset{language=ML,escapechar=\$,morekeywords={match},moredelim=**[is][\color{red}]{@}{@},}\lstset{#1}}{}
+
+OCaml~\cite{Ocaml} provides a tagged variant (union) type, where multiple heterogeneously-typed objects share the same storage.
+The simplest form of the variant type is a list of untyped tags, which is like an unscoped, pure enumeration.
 \begin{ocaml}
 type weekday = Mon | Tue | Wed | Thu | Fri | Sat | Sun
+let day : weekday = Mon					$\C{(* bind *)}$
+let take_class( d : weekday ) =
+	match d with						$\C{(* matching *)}$
+		Mon | Wed -> Printf.printf "CS442\n" |
+		Tue | Thu -> Printf.printf "CS343\n" |
+		Fri -> Printf.printf "Tutorial\n" |
+		_ -> Printf.printf "Take a break\n"
+let _ = take_class( Mon );
+@CS442@
 \end{ocaml}
-Enumerated data types are the simplest subset of variants types.
-Because @weekday@ is a summantion of values @Mon@ to @Sun@, enumerated data types are often call a sum type in turns of functional programming paradigm. 
-
-The values defined in an enumerated type are called data constructors.
-The data constructors of an enumerated data type takes no value as parameter.
-They are known as 0-arity constructor.
-
-A more generic variant type has n-ary constructors. 
+The only operations are binding a tag and pattern matching (equality).
+Here, function @take_class@ has a @weekday@ parameter, and returns @"CS442"@, if the weekday value is @Mon@ or @Wed@, @"CS343"@, if the value is @Tue@ or @Thu@, and @"Tutorial"@ for @Fri@.
+The ``@_@'' is a wildcard matching any @weekday@ value, so the function returns @"Take a break"@ for values @Sat@ or @Sun@, which are not matched by the previous cases.
+Since the tag has no type, it has a \Newterm{0-arity constructor}, \ie no parameters.
+Because @weekday@ is a summation of values @Mon@ to @Sun@, it is a \Newterm{sum type} in turns of the functional-programming paradigm. 
+
+Each tag can have an associated heterogeneous type, with an n-ary constructor for creating a corresponding value.
 \begin{ocaml}
 type colour = Red | Green of string | Blue of int * float
 \end{ocaml}
-The @colour@ type can be constructed as a combination of a value from an @int@ and a @blue@, using the @Blue@ data constructor.
-Mathematically, a @Blue@ value is a Cartesian product of the @int@ type and the @bool@. 
-@Colour@ type is a summation of a nullary type, a unary product type, and a cross product of @int@ and @bool@.
-The OCaml variant type can be create as a sum of product of different types.
+@colour@ is a summation of a nullary type, a unary product type of @string@, and a cross product of @int@ and @bool@.
+(Mathematically, a @Blue@ value is a Cartesian product of the @int@ type and the @bool@.)
+Hence, a variant type creates a sum of product of different types.
+\begin{ocaml}
+let c : colour = Red					$\C{(* 0-ary constructor *)}$
+let _ = match c with Red -> Printf.printf "Red, "
+let c : colour = Green( "abc" )			$\C{(* 1-ary constructor *)}$
+let _ = match c with Green g -> Printf.printf "%s, " g
+let c : colour = Blue( 1, 1.5 )			$\C{(* 2-ary constructor *)}$
+let _ = match c with Blue( i, f ) -> Printf.printf "%d %g\n" i f
+@Red, abc, 1 1.5@
+\end{ocaml}
 
 A variant type can have a recursively definition.
@@ -2489,25 +2506,6 @@
 type stringList = Empty | Pair of string * stringList
 \end{ocaml}
-OCaml's variant types are recusrive sum of product of types, which are known as Algebraic Data Types.
-Programming languages follows the functional programming paradigm often supports algebraic data types, and supports pattern matching against algebraic data type.
-\begin{ocaml}
-let take_class = function
-	Mon | Wed -> "CS442" |
-	Tue | Thu -> "CS343" |
-	Fri -> "Tutorial" |
-	_ -> "Take a break"
-\end{ocaml}
-The function has a @weekday@ as parameter, and returns @"CS442"@, if the weekday value is @Mon@ or @Wed@, @"CS343"@, if the value is @Tue@ or @Thu@, and @"Tutorial"@ for @Fri@.
-The @_@ is a wildcard matching any @weekday@ value, so the function returns @"Take a break"@ for values @Sat@ or @Sun@, which are not matched by the previous cases.
-
-Values of a product type can be named.
-\begin{ocaml}
-let check_colour (c: colour): string =
-	 match c with
-		Red -> "Red" |
-		Green g -> g |
-		Blue(i, f) -> string_of_int i ^ string_of_float f
-\end{ocaml}
-A recurisve function is often used to pattern match against a recurisve variant type.
+which is a recursive sum of product of types, called an \Newterm{algebraic data-type}.
+A recursive function is often used to pattern match against a recursive variant type.
 \begin{ocaml}
 let rec len_of_string_list(l: stringList): int =
@@ -2516,2 +2514,5 @@
 		Pair(_ , r) -> 1 + len_of_string_list r
 \end{ocaml}
+
+Note, matching is logically a dynamic type-check.
+Hence, a tagged variant has no notion of enumerabilty, and therefore is not an enumeration, except for the simple pure (untyped) case.
