In the discipline of computer science, modern type systems are regarded as a formal mechanism originated from Alonzo Church's \(\lambda \)  calculus proposed in 1940 [1]}. One possible definition of a type system is “a tractable syntactic framework for classifying phrases according to the kinds of values they compute" [2]}. By associating types with each computed value, a compiler can detect meaningless or invalid code written in a given programming language. For instance, the expression “mix = 29 + “Tan"" cannot get through type checking since a string cannot be added to a number.
