Types and Types Systems concepts

Question

Given this definitions about Types and Type systems :

Types are described by means of a language of type expressions:

• Basic or primitive types: Bool, Char, Int, ...

• Type variables: a, b, c, ...

• Type constructors: → (function), × (tuple), [ ] (list), ...

• Rules to build type expressions:

  τ ::= Bool | Char | Int | ··· | t | τ → τ | τ × τ | [ τ ] | ···

• Types whose type expression contains no type variable are called monomorphic types or just monotypes.

• Types whose type expression contains variables are called polytypes or polymorphic types (parametric polymorphism)

• A polymorphic type represents an infinite number of monotypes

I'm trying to understand the last definition but i can't. A polymorphic type represents a infinite number of monoytpes, because in his type expression has a type variable ?

Answer 1

Yes, exactly. Because you can instantiate the polymorphic type with an infinite amount of (mono)types.

For example, the type $a \to a$ (which is a polymrphic type) represents

• Bool $\to$ Bool
• Char $\to$ Char
• (Char $\to$ Int) $\to$ (Char $\to$ Int)
• etc...