En la teoría de tipos , una regla de tipos es una regla de inferencia que describe cómo un sistema de tipos asigna un tipo a una construcción sintáctica. Estas reglas pueden ser aplicadas por el sistema de tipos para determinar si un programa está bien escrito y qué tipo de expresiones tienen. Un ejemplo prototípico del uso de reglas de tipos es la definición de inferencia de tipos en el cálculo lambda simplemente tipado , que es el lenguaje interno de las categorías cerradas cartesianas .
Notación
Una expresión de tipo está escrito como . El entorno de escritura se escribe como. La notación para inferencia es la habitual para secuentes y reglas de inferencia , y tiene la siguiente forma general
Los secuentes arriba de la línea son las premisas que se deben cumplir para que se aplique la regla, dando como resultado la conclusión: los secuentes debajo de la línea. Esto se puede leer como: if expresión tiene tipo en el medio ambiente , para todos , luego la expresión tendrá un ambiente y escriba .
Por ejemplo, un lenguaje simple para realizar cálculos aritméticos en números reales puede tener las siguientes reglas
Una regla de tipo puede no tener premisas y, por lo general, la línea se omite en estos casos. Una regla de tipo también puede cambiar un entorno agregando nuevas variables a un entorno anterior; por ejemplo, una declaración puede tener la siguiente regla de tipo, donde una nueva variable, con tipo , se agrega a :
Aquí, la sintaxis de la expresión let es la de ML estándar . Por lo tanto, las reglas de tipos se pueden usar para derivar los tipos de expresiones compuestas, al igual que en la deducción natural .
Ver también
Otras lecturas
- Cardelli, Luca (marzo de 1996). "Type Systems" (PDF) . Encuestas de computación ACM . 28 (1): 263–264. doi : 10.1145 / 234313.234418 .