自分の理解のまとめです。ベースはWikipediaです。（Wikipedia日本語ページの記述は2017/3に英語ページの記述をもとに拡充されています。）論文や書籍を参照・引用してるわけではないので、たぶん突っ込みどころがあるのではないかと思います。うのみにしないように。

多相性

ざっくり3つに分類されています。

アドホック多相
サブタイピング多相
パラメトリック多相

アドホック多相は、型システム上は関連性のない複数の型を引数や戻り値にとることができる関数（メソッドや演算子を含む）の性質です。普通は引数や戻り値の型に応じて異なる実装にディスパッチされます。Javaで言うとオーバーローディングです。Javaのオーバーローディングだと、多相性を保ったまま第一級オブジェクトとして扱うことはできません（オーバーロードされたメソッドの参照を関数インターフェース型の変数に代入しようとすると、その時点でオーバーロードが解決されます）。

サブタイピング多相¹は、ある型を引数や戻り値にとる関数が、その型の部分型（サブタイプ、派生型とも言う）も引数や戻り値に取ることができる性質です。普通は型に応じて異なる実装にディスパッチされます。Javaというか静的型付けOOP²でポリモーフィズムと言えばこれを指すことが多いです。
Javaでは、スーパータイプ（親クラスまたはインターフェース）に定義されたメソッドをサブタイプ（子クラスまたは実装クラス）でオーバーライドしたり実装したりすることで、インスタンスメソッドを呼び出したときに実行時のthisの型に応じて実装が選ばれます。インスタンスメソッドを関数としてとらえ、thisを暗黙の第一引数と考えれば、「ある型を引数や戻り値にとる関数が、その型の部分型を……」に適合していることがわかります。
なお、Javaのように、（クラスの継承やインターフェースの実装など）関係性を明示することでサブタイプが決まる仕組みを、公称的部分型（ノミナルサブタイピング）といいます。一方、OCamlやTypeScriptは、構造的部分型（ストラクチャルサブタイピング）といい、ある型に定義されたメンバーが、別の型に定義されたメンバーと構造的に互換性がある場合、自動的にサブタイプ関係が成立します³。そこに継承はかならずしも必要ありません⁴。

サブタイピングが出てくると必ず一緒に顔を出す厄介な問題が共変性／反変性です。正確な定義にはいろいろ前提知識がいるので、ここでは適当に端折って書きますが、T型の引数を取ったりT型の戻り値を返したりする関数があったとき、型Tに対して互換性がある別の型Uを持ってきたら、「T型の引数を取ったりT型の戻り値を返したりする関数」と「U型の引数を取ったりU型の戻り値を返したりする関数」に互換性があるかどうか、といったことを考える時の話です。
共変性／反変性が問題になるのは、多くの場合、後述するパラメトリック多相とサブタイピングが組み合わさった時です。ですが、サブタイピング多相だけでも共変性／反変性を考えることはあります。一つの例が、Javaにおける「メソッドをオーバーライドしたときの戻り値の型」です。

class AnimalSound {
}
class Animal {
  AnimalSound cry() {
    ...
  }
}

みたいなクラスがあったときに、これらを継承して

class DogSound extends AnimalSound {
}
class Dog extends Animal {
  @Override
  DogSound cry() {
    ...
  }
}

とすることができます。それは、「AnimalSound型とDogSound型の互換性」と「AnimalSound cry()メソッドとDogSound cry()メソッドの互換性（ひいては、それぞれのメソッドを定義しているAnimal型とDog型の互換性）」に共変性があるためです。これをJavaでは「共変戻り値型」と呼びます。

パラメトリック多相は、関数の引数や戻り値の型情報の一部をパラメータ化して外部から与えることができる関数、あるいは、合成型の定義に含まれる型情報の一部をパラメータ化して外部から与えることができる型の性質です。パラメータ化された型を型パラメータや型変数と呼ぶこともあります。普通は型に対して抽象化された一つの実装⁵を持ち、型パラメータとして具体的な型が与えられた時に再利用されます。ジェネリクスと言えば基本的にはこれを指します。

型パラメータは基本的には任意の型をとるのですが、任意の型しかとれないとなると、 "抽象化された一つの実装" の中で、パラメータ化された型の値に対し何か具体性のある処理をしたいときに困ることがあります。なので、型パラメータを限定するために型制約をつけることができる言語もあります。限定といっても一つの型しかとれないようだとパラメトリックな多相性があるとはいえませんから、型制約はほかの多相性（アドホック多相やサブタイプ多相）と関連するのが普通です。たとえばJavaでは<T extends Xxx>のようにサブタイプ関係を指定できます。C++のテンプレートではメソッドや演算子の存在がチェックされます（≒構造的部分型）。Haskellでは型クラスを制約とすることができます。

サブタイピング多相のところにも書きましたが、パラメトリック多相とサブタイピングが組み合わさると、共変性／反変性のバリエーションがぐっと増え、とても複雑になりがちです。
Javaの配列は、ジェネリクスの機構が取り入れられる前からあった唯一のパラメトリック多相とみなせます（Foo型の配列 Foo[] を Array<Foo> と読み替えてみましょう）。Javaの配列にはなぜか共変性があり（細かくは省略します）、メリットもなくはないのですが型安全性の観点ではデメリットが多いため、配列の共変性を利用することは避けられるようになりました。

型を集合と考えた時の部分集合と包含関係にちなんで「インクルージョン（包摂）多相」と呼んだりもします。 ↩
Smalltalkなどの動的型付けOOPにおけるメッセージング機構だとサブタイピングとは言いにくい気がします。 ↩
OCamlの多相ヴァリアントも構造的部分型に分類されるのかどうか、よくわかりませんでした。 ↩
OCamlの場合はメソッドの引数や戻り値を「自分と同一の型」とすることができるので、むしろ継承するとサブタイプ関係が崩れることもあります。 ↩
ソースコード上の話。C++テンプレートの特殊化の話や、具象化（レイフィケーション）と型消去（イレイジャー）の話は、今回は省略しました。 ↩

多相性とジェネリクス

多相性