Auniversally quantifiedorpolymorphictype has the formforall v1 v2 vn. t,wheretis a type. The typetmay involve the variablesv1throughvn.
The symbol∀is an alias forforall.
A type likeforall x. F xcan be written simply asF x(theforall xis implied) as long asxis free inF x(it is not bound by an outer scope; seeScoped type variablesbelow).
A polymorphic type may beinstantiatedat any given type. For example, the empty list[]has typeforall x. [x].So it's a type-polymorphic value. Its type can be instantiated atInt,for example, which bindsxtoIntresulting 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 allchoices of element typee,hence the typeforall x. [x].
Likewise the identity function(x -> x),which simply returns its argument, has a polymorphic typeforall t. t -> t.It has typet -> tfor all choices oft.