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 ?


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...
| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.