段階的なタイピング

段階的型付けは、静的型付けと動的型付けの中間に位置する型システムです。一部の変数と式には型が指定され、コンパイル時に型の正確さがチェックされます(静的型付け)。また、一部の式は型付けされず、実行時に最終的な型エラーが報告されます(動的型付け)。

段階的型付けにより、ソフトウェア開発者は単一の言語内から、必要に応じていずれかの型パラダイムを選択できます。^[1]多くの場合、段階的型付けは既存の動的言語に追加され、^[2]静的型付けの使用を許可するが必須ではない派生言語が作成されます。場合によっては、言語が最初から段階的型付けを使用します。

この用語は、2006年にワリド・タハとともに段階的型付けを開発したジェレミー・シークによって造られました。^{[1] [非一次資料が必要]}

段階的型付けでは、静的に未知の型を表すために、 dynamicという特別な型が使用されます。型の等価性の概念は、 dynamic型を他のすべての型に関連付ける一貫性と呼ばれる新しい関係に置き換えられます。一貫性関係は反射的で対称的ですが、推移的ではありません。^[3]

静的型付けと動的型付けを統合する以前の試みでは、動的型をサブタイプ階層の最上位と最下位の両方にしようとした。しかし、サブタイプ化は推移的であるため、すべての型が他のすべての型と関連し、サブタイプ化によって静的型エラーを排除できなくなる。型システムに妥当性チェックの第2段階を追加しても、この問題は完全には解決されなかった。^{[4] [5]}

段階的型付けは、サブタイプ化に関して暗黙的なアップキャストを可能にするためにサブサンプションルールをすでに使用しているオブジェクト指向言語の型システムに簡単に統合できます。 主なアイデアは、一貫性とサブタイプ化はうまく組み合わさる直交するアイデアであるということです。 段階的型付け言語にサブタイプ化を追加するには、サブサンプションルールを追加し、サブタイプ化は反射的であるはずなので、動的型をそれ自身のサブタイプにするサブタイプ化ルールを追加するだけです。 (ただし、サブタイプ化順序のトップを動的にしないでください!) ^[6]

既存の動的型付け言語から派生した段階的に型付けされる言語の例には、Closure Compiler、TypeScript（ともにJavaScript用^[7]）、^[8] Hack（PHP用）、PHP（7.0以降^[9]）、Typed Racket（Racket用^{[10] [11]}）、Typed Clojure（Clojure用^[12] Cython（Pythonコンパイラ）、mypy （ Python用静的型チェッカー）、^[13] pyre（Python用代替静的型チェッカー）、^[14]またはcperl（型付けされたPerl 5）などがあります。ActionScriptは段階的に型付けされる言語^{[15]であり、現在は}ECMAScriptの実装となっていますが、もともとは兄弟として別々に登場し、ともにAppleのHyperTalkの影響を受けています。

Jプログラミング言語用のシステムが開発され、^[16]型システムの通常の検証プロパティに強制、エラー伝播、フィルタリングが追加され、関数定義の外部に型関数が適用され、型定義の柔軟性が向上しました。

逆に、C#は静的型付け言語として始まりましたが、バージョン4.0からは段階的に型付けされ、型を使用して変数を明示的に動的としてマークできるようになりましたdynamic。^[17] 動的型付け言語から派生していない段階的に型付けされた言語には、Dart、Dylan、Rakuなどがあります。

Raku (旧称 Perl6) には、最初から段階的な型付けが実装されています。型チェックは、値が代入またはバインドされるすべての場所で行われます。「型指定されていない」変数またはパラメータは と型指定されAny、(ほぼ)すべての値と一致します。コンパイラは、コンパイル時に型チェックの競合が決して成功しないと判断できる場合、コンパイル時にその競合にフラグを立てます。

Objective-C では、メソッド呼び出しに関して、オブジェクト ポインターの段階的な型付けが行われます。静的型付けは、変数が特定のオブジェクト クラスへのポインターとして型付けされている場合に使用されます。変数に対してメソッド呼び出しが行われると、コンパイラーはクラスがそのようなメソッドをサポートするように宣言されているかどうかを静的にチェックし、そうでない場合は警告またはエラーを生成します。ただし、その型の変数idが使用されている場合、コンパイラーはその変数に対して任意のメソッドを呼び出すことを許可します。

2011年にリリースされたJS ++プログラミング言語は、 ECMAScriptやDOM APIの特殊なケースに適した段階的な型システムを備えたJavaScript （動的型付け）のスーパーセットです。^[18]

• ジーク、ジェレミー G.ヴィトセク、マイケル M.チミニ、マッテオ。ボーイランド、ジョン・タン (2015)。ボール、トーマス。ボディク、ラスチスラフ。クリシュナムルティ、シュリラム。ラーナー、ベンジャミン S.モリセット、グレッグ (編)。段階的な入力のための洗練された基準。情報学におけるライプニッツ国際論文集。 Vol. 32. ダグシュトゥール、ドイツ: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik。 274–293ページ。土井：10.4230/lipics.snapl.2015.274。ISBN 9783939897804.S2CID 15383644  。