Index: doc/theses/jiada_liang_MMath/relatedwork.tex
===================================================================
--- doc/theses/jiada_liang_MMath/relatedwork.tex	(revision 9a32903fc141b4db3380f2b4e3d945f14c51303a)
+++ doc/theses/jiada_liang_MMath/relatedwork.tex	(revision 423c0cd0894a0a7babef2a37f4f5c2ec522aa094)
@@ -2502,5 +2502,5 @@
 \end{ocaml}
 
-A variant type can have a recursively definition.
+A variant type can have a recursive definition.
 \begin{ocaml}
 type stringList = Empty | Pair of string * stringList
@@ -2509,10 +2509,13 @@
 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 =
-	match l with
+let rec len_of_string_list( list : stringList ): int =
+	match list with
 		Empty -> 0 |
-		Pair(_ , r) -> 1 + len_of_string_list r
+		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.
+Here, the head of the recursive type is removed and the remainder is processed until the type is empty.
+Each recursion is counted to obtain the number of elements in the type.
+
+Note, the compiler statically guarantees that only the correct kind of type can be used in the \lstinline[language=ML]{match} statement.
+However, the tag is dynamically set on binding (and possible reset on assignment), so the \lstinline[language=ML]{match} statement is effectively doing RTTI to select the matching case clause.
+Hence, a tagged variant has no notion of enumerabilty, and therefore is not a real enumeration, except for the simple pure (untyped) case.