Abstraction type system
Type system is a construction for guarantees safely in a language, though exist many other aplications like metaprogramming... It's means that i can writes a program but with a safe way, sure it's is perfect why it's solve many problems that programmers has after of compilation. The main idea that i can encode and represent a subset of solutions with a safe type system and better maybe the type can help me represent that.
Ok it's mean i have a safe type system and i could represent my types of data..... Ok sure...., but no... limited type system have a weak power of abstraction(no i am not talking about c++ but yes a little part of the language).
The problem of "pair"
Let's go represent a pair: Pair is a tuple of the two values like (P x y), where x and y are values, in this discussion the values x and y can be encode a T type and a Tuple T type.