A universally quantified or "polymorphic" type has the form `forall v1 v2 vn. t`

, where `t`

is a type. The type `t`

may involve the variables `v1`

through `vn`

.

The symbol `ā`

is an alias for `forall`

.

A type like `forall x. F x`

can be written simply as `F x`

(the `forall x`

is implied) as long as `x`

is free in `F x`

(it is not bound by an outer scope; see Scoped type variables below).

A polymorphic type may be instantiated at any given type. For example, the empty list `[]`

has type `forall x. [x]`

. So it's a type-polymorphic value. Its type can be instantiated at `Int`

, for example, which binds `x`

to `Int`

resulting in `[Int]`

which is also a valid type for the empty list. In fact, we can say that the empty list `[]`

is a value of type `[x]`

for all choices of element type `e`

, hence the type `forall x. [x]`

.

Likewise the identity function `(x -> x)`

, which simply returns its argument, has a polymorphic type `forall t. t -> t`

. It has type `t -> t`

for all choices of `t`

.