Polymorphism

ad-hoc

This means syntactic level tricks, no support at type-level.

Operator overloading

Syntactic sugar, as if a function is generic (desugars into specialized mono-typed by a compiler)
Parameterized templates or macros (syntactic level)

Implicit coercions

coercion syscalls inserted by a compiler (a kludge)

Universal

A polymorphic type-system (such as the Hidley-Milner).

Parametric

Parameterized type-constructors (type-level application)

Sharing the same structure (a structured value)
The same code for all types (like length)

Sub-typing

An actual type-hierarchy from general to specific (specialization)

Sharing the same interface (nesting)
The same code for all types, unless shadowed (overridden)

Type-classes

An extension of a Hindley-Milner sytem - partitioning by an interface (a set of type-signatures)

Sub-class relationship (has to implement)
Passing a dictionary of functions

forall

It turns out that one cannot just say $\forall x$ - this would imply everything what is in the whole Universe and lead to the Russel paradox.

An universal quantifier requires an $\in$ or a “such that” ($\vert$) - a particular selection (or a predicate), and this is the “natural” notion of typing (which arises “naturally” in this world).

The $\forall x \in S\vert P(x)$ quantifier implies that the relation, which it binds, is a projection (forms a Subset).

Just like $λ x.$ binds a variable, $∀ x.$ binds a type-variable. (and so does $∃ x.$). The bound variable has to appear in the following scope being thus introduced.

At a type-level quantifiers introduce a generic (parameterized by a type) expression, which binds a type-variable and thus selects a Subset of (from) the Set of All Types.

In modern languages one could write an explicit forall a

id :: forall a. a -> a
id x = x

Here the type-variable a ranges over the set of all possible types, and in this particular context (and the special case of an identity function) it produces no paradoxes.

There is an explicit type-constraint on a - the type has to be “already” an instance of the Eq type-class.

instance forall a. Eq a => Eq [a] where
  ...

We can explicitly declare a type-variable (Ocaml does not have type-classes)

type showable = Show: 'a. 'a * ('a -> string) -> showable

exists

The $\exists$ quantifier corresponds to the notion that there is a most general type (a super-type) like Object.