Polymorphism

Here, by ``polymorphism,'' we mean ML-polymorphism (i.e., $2$nd-order universal)--with a few differences that will be explained along the way--in other words, types presented with a grammar such as:

that ensures that universal type quantifiers occur only at the outset of a polymorphic type.^4.1