質問

私は ツイート 今日、こんなことを言った。

Javaユーザーが、Javaが間違っていたことをすべて無視して、唯一正しかった型消去について文句を言うのはおかしい。

したがって、私の質問は

Javaの型消去から利点がありますか？後方互換性と実行時のパフォーマンスのためのJVM実装の好み以外に、それが提供する（かもしれない）技術的またはプログラミングスタイルの利点は何でしょうか？

どのように解決するのですか？

タイプ・イレーザーは良い

事実に忠実であろう

ここまでの回答の多くは、Twitterユーザーに過度に配慮したものです。 メッセンジャーではなく、メッセージに焦点を当て続けることは有用です。 これまでに挙げられた抜粋だけでも、かなり一貫したメッセージがあります。

Java ユーザーが、Java が間違っていたすべてのことを無視して、Java が正しかった唯一のことである型消去について文句を言うのはおかしな話です。

巨大なメリット（パラメトリック性など）を得て、コストはゼロ（コストと言われるのは想像力の限界）。

new Tは壊れたプログラムである。それは "all propositions are true." という主張と同型であり、私はこれに大きな意味を持ちません。

目標：合理的なプログラム

これらのツイートは、機械に以下のことをさせることができるかどうかには興味がない、という視点を反映しています。 何か をさせることができるかどうかではなく、マシンが私たちが実際に望むことをすることを推論できるかどうかに関心がある視点を反映しています。 良い推論とは証明である。 証明は形式的な記法で指定することもできますし、より形式的でないもので指定することもできます。 仕様言語に関係なく、証明は明確で厳密でなければなりません。 非公式な仕様は、正しく構成することは不可能ではありませんが、実用的なプログラミングではしばしば欠陥が生じます。 結局、自動テストや探索的テストのような改善策で、非公式な推論で抱える問題を補うことになるのです。 これは、テストが本質的に悪い考えであると言うわけではありませんが、引用したTwitterユーザーは、もっと良い方法があることを示唆しています。

ですから、私たちの目標は、マシンが実際にどのようにプログラムを実行するかに対応する方法で、明確かつ厳密に推論できる正しいプログラムを持つことなのです。 しかし、これだけが目標ではありません。 論理にはある程度の表現力も必要です。 例えば、命題論理で表現できることは限られている。 一階論理のようなものから普遍量化（∀）や存在量化（∃）ができるのはいいことです。

推論のための型システムの使用

これらの目標は、型システムによって非常にうまく対処することができます。 このことは、特に カレー・ハワード対応 . この対応関係はしばしば次のようなアナロジーで表現されます：型はプログラムにとって定理であり、証明にとって定理である。

この対応はやや奥が深い。 論理式は、型への対応を通じて変換することができます。 そして、同じ型署名でコンパイルできるプログラムがあれば、その論理式が普遍的に真であることを証明したことになります（トートロジー）。 これは、対応が双方向であるためである。 型/プログラムと定理/証明の世界の変換は機械的であり、多くの場合自動化することができます。

Curry-Howardは、私たちがプログラムの仕様で行いたいことにうまく対応します。

Javaで型システムは有用か？

Curry-Howardを理解していても、型システムの価値を簡単に否定してしまう人がいますが、その場合は

1. で作業するのが非常に困難である
2. は、（Curry-Howard を通して）表現力が制限された論理に対応する。
3. が壊れている (これは "weak" または "strong" としてのシステムの特徴づけになる)。

最初のポイントについて、おそらくIDEはJavaの型システムを十分に作業しやすくしています（これは非常に主観的です）。

2点目について、Javaは偶然にも <項目 ほとんど は一階論理に相当する。 ジェネリックスは普遍量化（universal quantification）に相当する型システム を与える。 残念ながら、ワイルドカードは実存的数量化のごく一部を与えるに過ぎない。 しかし、普遍的な数量化というのは、かなり良いスタートである。 例えば List<A> に対して普遍的に働くと言えるのは素晴らしいことです。 すべての可能な のリストに対して普遍的に動作します。これは、Aが完全に無制約であるためです。 これは、Twitterユーザーが言っている「パラメトリック性」に関してです。

パラメトリック性に関してよく引用される論文に、Philip Wadlerの Theorems for free! . この論文の面白いところは、型署名だけで、いくつかの非常に興味深い不変量を証明できることです。 もし、これらの不変量に対して自動テストを書くとしたら、非常に時間を無駄にすることになる。 例えば List<A> に対して、型シグネチャだけから flatten

<A> List<A> flatten(List<List<A>> nestedLists);

flatten(nestedList.map(l -> l.map(any_function)))
    ≡ flatten(nestList).map(any_function)

<T> T broken { return new T(); }