位相の区別

フェーズの区別は、型と項を厳密に区別するプログラミング言語の特性です。言語でフェーズの区別が保持されるかどうかを判断するための簡潔なルールが、Luca Cardelliによって提案されました。Aがコンパイル時の項であり、B が A のサブ項である場合、B もコンパイル時の項である必要があります。 ^[1]

静的に型付けされた言語のほとんどは、フェーズの区別の原則に従います。ただし、特に柔軟で表現力豊かな型システムを持つ言語 (特に依存型プログラミング言語) では、型を通常の項と同じ方法で操作できます。型は関数に渡されたり、結果として返されたりします。

フェーズの区別がある言語では、型と実行時変数に別々の名前空間がある場合があります。最適化コンパイラでは、フェーズの区別によって、安全に消去できる式間の境界が示されます。

フェーズの区別は静的チェックと組み合わせて使用​​されます。^[2]計算ベースのシステムを使用することで、フェーズの区別はプログラミングの異なるタイプと用語の間で線形ロジックを強制する必要がなくなります。^[3]

フェーズの区別は、コンパイル時に実行される処理と実行時に実行される処理を区別します。

次のような用語を含む単純な言語^[3]を考えてみましょう。

   t ::= true | false | x | λx : T . t | tt | t ならば t、そうでなければ t

種類:

   T ::= ブール | T -> T 

型と用語がどのように異なるかに注意してください。コンパイル時に、型は用語の有効性を検証するために使用されます。ただし、実行時には型は役割を果たしません。