Phase Distinction es una propiedad de los lenguajes de programación que observan una estricta división entre tipos y términos . Luca Cardelli ha propuesto una regla concisa para determinar si la distinción de fase se conserva o no en un idioma : si A es un término de tiempo de compilación y B es un subtérmino de A, entonces B también debe ser un término de tiempo de compilación. [1]
La mayoría de los lenguajes tipificados estáticamente se ajustan al principio de distinción de fase. Sin embargo, algunos lenguajes con sistemas de tipos especialmente flexibles y expresivos (especialmente los lenguajes de programación tipificados de forma dependiente ) permiten que los tipos se manipulen de la misma manera que los términos regulares. Pueden pasarse a funciones o devolverse como resultados.
Un lenguaje con distinción de fase puede tener espacios de nombres separados para tipos y variables de tiempo de ejecución. En un compilador de optimización , la distinción de fase marca el límite entre las expresiones que son seguras de borrar .
La distinción de fase se utiliza junto con la verificación estática. [2] Mediante el uso de un sistema basado en cálculo, la distinción de fases elimina la necesidad de aplicar una lógica lineal entre diferentes tipos y términos de programación. [3]
Phase Distinction distingue entre el procesamiento que se realiza en tiempo de compilación y el procesamiento realizado en tiempo de ejecución.
Tenga en cuenta cómo los tipos y los términos son distintos. En tiempo de compilación, los tipos se utilizan para verificar la validez de los términos. Sin embargo, los tipos no juegan ningún papel en tiempo de ejecución.