タイプチェックアルゴリズム

Question

私はタイプチェックアルゴリズムに関する個人的な参考文献研究を始めており、いくつかのヒントが必要です。最も一般的に使用されるタイプチェックアルゴリズム、戦略、一般的な手法は何ですか？

特に、C ++、Java 5+、Scalaなど、広く知られている強力な静的な型言語で実装された複雑なタイプチェックアルゴリズムに興味があります。 IE、基礎となる言語の非常に単純なタイピング（Java 1.4以降など）のためにそれほど単純ではないタイプチェックアルゴリズム。

私は特定の言語X、Y、Zに興味がありません。ターゲットとする言語に関係なく、タイプチェックアルゴリズムに興味があります。どちらが強く入力されていて、タイピングが複雑であるかについて聞いたことがない言語lのような回答を提供する場合、アルゴリズムzを使用してxとyをチェックすることにより、a、b、cを実行するタイプチェックアルゴリズムがあります」、または「 SCALAに使用される戦略XとYおよびC＃に使用されるAのバリアントZは、そのように機能するR、S、Tの機能のためにクールです。

Answer 1

ほとんどの研究では、完全に吹き飛ばされたプログラミング言語のタイプチェックアルゴリズムを実際に公開していません。あなたは、によって行われた作業など、完全なプログラミング言語のタイプシステムの大部分のいくつかの形式を見つけるでしょう JavaのDrossopoulouとEisenbach また Nipkov et alのC ++に関する研究. 。ただし、多くの場合、言語のコア部分（フェザー級Javaが一例です）の型システムを見つけることができます。 SCALAのローカルタイプの推論アプローチ.

POPLやICFPなどの会議では、特定の種類のタイプシステムの多くのタイプチェックアルゴリズム、およびなどの新しいアプローチがあります。 双方向 と 三方向 タイプチェック。

より一般的には、あなたはおそらく Damas-Milnerアルゴリズム, 、ローカルタイプの推論、双方向および三方向タイプのチェック、およびそこから拡大し、論文で参照をフォローし、Google Scholarを使用してこれらを引用し、説明されているアプローチに基づいて構築する論文を見つけます。また、上記のように、POPL、ICPF、ESOP、さらにはEcoopやOopslaなどの会議には、クエストに関連する論文があります。

Answer 2

基本的なツールはです 属性グラマー. 。あなたは彼らと一緒に想像できるすべての邪悪なことをすることができないかもしれませんが、それらは良い出発点です。

基本的に、プログラムの抽象的な構文ツリーのトップダウンおよび/またはボトムアップを歩き、情報を渡すことができます。したがって、たとえば、グローバルスコープタイプ情報（クラスやそのメンバーなど）を下向きに渡し、式のタイプを再帰的に決定し、つまり、結果のタイプを上に渡すことができます。

スライドにいくつかの説明と例を見つけてください ここ （第5章）。