Hispanopedia WikiLa distinción de fases es una propiedad de los lenguajes de programación que observan una división estricta entre tipos y términos . Luca Cardelli propuso una regla concisa para determinar si la distinción de fases se conserva en un lenguaje o no : 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 de tipado estático se ajustan al principio de distinción de fases. Sin embargo, algunos lenguajes con sistemas de tipos especialmente flexibles y expresivos (en particular, los lenguajes de programación con tipado dependiente ) permiten manipular los tipos del mismo modo que los términos regulares. Estos pueden pasarse a funciones o devolverse como resultados.
Un lenguaje con distinción de fases puede tener espacios de nombres separados para tipos y variables de tiempo de ejecución. En un compilador optimizador , la distinción de fases marca el límite entre las expresiones que se pueden borrar de forma segura .
Teoría
La distinción de fases se utiliza junto con la verificación estática. [ 2 ] Al utilizar un sistema basado en cálculo, la distinción de fases elimina la necesidad de imponer una lógica lineal entre diferentes tipos y términos de programación. [ 3 ]
Introducción
La distinción de fases diferencia entre el procesamiento que se realiza en tiempo de compilación y el procesamiento que se realiza en tiempo de ejecución.
Consideremos un lenguaje simple, [ 3 ] con términos:
t ::= verdadero | falso | x | λx : T . t | tt | si t entonces t sino t
y tipos:
T ::= Booleano | T -> T
Nótese la diferencia entre tipos y términos. En tiempo de compilación , los tipos se utilizan para verificar la validez de los términos. Sin embargo, en tiempo de ejecución, los tipos no desempeñan ningún papel.
Referencias
- ↑ Cardelli, Luca (3 de enero de 1988). "Distinciones de fase en la teoría de tipos" (PDF) . Digital Equipment Corporation .
- ↑ Cardelli, Luca (3 de enero de 1988). "Distinciones de fase en la teoría de tipos" (PDF) . Digital Equipment Corporation .
- 1 2 "CMSC 336: Sistemas de tipos para lenguajes de programación; Lección 7: Isomorfismo de Curry-Howard y formas derivadas" (PDF) . 31 de enero de 2008.
- Programación informática