PDF de programación - Apuntes de Programación y estructuras de datos. Tipos de datos

Apuntes de Programación y estructuras de

datos. Tipos de datos

Nikos Mylonakis, Fernando Orejas y Ana Cristina Zoltan

[email protected]

Dept. Llenguatges i Sistemes Informátics Universitat Politécnica de Catalunya

Barcelona

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.1/36

Introducción a la comprobación de
tipos

• Un tipo se puede definir como una propiedad de

un conjunto de valores

• Ejemplos: booleanos, enteros, entero_par,

entero_impar, tablas, tuplas, etc

• Los tipos también se pueden asociar a todas las

construcciones del lenguaje, por ejemplo las
operaciones, las instrucciones y los subprogramas
• Los tipos se introducen en los LPs por motivos de

seguridad.

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.2/36

• Los tipos determinan cómo se pueden utilizar las

entidades del LP

• Ejemplo 1: Si x es entero lo podemos sumar a un

entero pero no lo podemos utilizar en una
operación lógica o como una acción

• Ejemplo 2: Si A:tabla [1..100] de entero la expresión

A[50] es correcta pero A[120] no

• Para detectar los errores de uso de las diferentes

entidades de un LP los LP realizan una
comprobación de tipos

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.3/36

• Ejemplo 1: Para que x + y sea correcta x e y han

de ser bien enteros bien reales

• Ejemplo 2: Para que A[50] sea correcta A ha de

ser de tipo tabla y 50 ha de estar entre el subrango
de la tabla.

• La comprobación de tipos puede ser estática (en
tiempo de compilación) o dinámica (en tiempo de
ejecución)

• Hay comprobaciones de tipos que sólo se pueden

realizar en tiempo de ejecución.

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.4/36

• La comprobación de tipos dinámica hace que los

programas se ejecuten más lentamente

• En algunos LP las comprobaciones dinámicas son

opcionales. Java las realiza siempre

• Las ventajas de la comprobación de tipos son

fiabilidad (si hay errores se detectan lo más pronto
posible) y eficiencia (la memoria asignada a las
variables se puede gestionar con una pila si no se
utilizan punteros)

• Las desventajas son que a veces se imponen

restricciones innecesarias y que es pesado tener
que declarar todo

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.5/36

Clases de sistemas de tipos

• Los sistemas de tipos en los LP pueden ser

monomórficos (toda entidad sólo tiene un único
tipo) o polimórficos ( una entidad puede tener más
de un tipo).

• La notación algorítmica que utilizamos es

monomórfica aunque puede haber sobrecarga de
operadores y Java es polímorfico (por la relación
clase-subclase)

• Hay dos clases de polimorfismo: polimorfismo de

subclase y polimormismo parámetrico

• Ejemplo de polimorfismo parámetrico: listas de

cualquier tipo ([α]) en Haskell donde α denota
cualquier tipo

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.6/36

• Otra decisión de diseño de los sistemas de tipo LP

es la equivalencia de tipos

• Ejemplo : x:=y requiere la comprobación de que

ambos tipos son equivalentes

• Hay dos clases de equivalencia: por nombre y por

estructura

• La equivalencia por nombre requiere que los dos

tipos tengan el mismo nombre

• La equivalencia por estructura requieren que los

dos tipos tengan la misma estructura

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.7/36

Ejemplo:

tipo
T = tabla [1..100] de entero
T ′ = tabla [1..100] de entero
ftipo

var
t1, t2 : T ;
t3 : T ′;
t4 : tabla [1..100] de entero
fvar

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.8/36

• Si hay equivalencia por nombre t1 := t2 es correcto

pero t1 := t3 y t1 := t4 no.

• Si hay equivalencia estructural t1 := t2, t1 := t3 y

t1 := t4 son correctas

• En Java la equivalencia de tipos es por nombre
• La equivalencia estructural varía según el LP

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.9/36

• Otro tema relacionado con la equivalencia de tipos

son las coerciones

• Las coerciones son conversiones ímplicitas de

tipos

• Ejemplo: En C se realiza una coerción al realizar

x = y si x es real y y entero

• En Java no existen coerciones
• Siempre se permite realizar conversiones

explícitas

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.10/36

Concepto de subclase

• Se dice que existe una relación de subclase entre

SC y C (SC es subclase de C) si siempre que
podemos utilizar elementos de la clase C también
podemos utilizar elementos de la subclase SC
• La relación de subclase no es lo mismo que la
relación de subconjunto en teoría de conjuntos

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.11/36

tipo
t = tupla

A : entero;
B : booleano;
ftupla

st = tupla

A : entero;
B : booleano;
C : caracter;
ftupla

ftipo

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.12/36

• Los valores de st no están incluidos en t pero en

cambio sí que puede existir una relación de
subclase

• El motivo es porque las operación de acceso a un

campo de las tuplas hace que siempre que se
utilice un elemento de t se puede utilizar un
elemento de st pues los campos de t están
incluidos en st.

• En algunos LP como en Java para que puede

existir relación de subclase se tiene que declarar
explícitamente

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.13/36

Reglas de inferencia en sistema de
tipos

• Si los tipos son propiedades de conjuntos de

valores, la lógica es una buena herramienta para
tratarlas

• Un sistema de tipos quedará definido por un

conjunto de reglas para inferir si una cierta
construcción del LP tiene su tipo correcto
• Las reglas de inferencia tendrán la forma

premisa1

. . .

premisaN

conclusion

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.14/36

• Ejemplo de reglas lógicas

A B
A ∧ B

A ⇒ B A

B

• Las premisas y conclusiones de las reglas de un

sistema de tipos para determinar el tipo de una
expresión podrían ser de la forma Expr : T (Expr
tiene el tipo T )

• Ejemplo de estas reglas serían

E1 : entero E2 : entero

E1 : entero E2 : entero

E1 + E2 : entero

E1 ≤ E2 : booleno

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.15/36

• El problema está en que la comprobación de tipos

requiere un conjunto de declaraciones de
constantes y variables ademas de la aridad de las
operaciones predefinidas

• Por tanto las reglas requieren de entorno Γ que
contiene una lista con todas las declaraciones
definidas y predefinidas

• Nosotros no veremos las reglas de generación del
entorno pero si veremos el formato general de las
reglas para comprobar el tipo de las expresiones

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.16/36

Γ ∪ {x : T } ⊢ x : T

Γ ∪ {f : T 1 × . . . × T N → T } ⊢ f : T 1 × . . . × T N → T

Γ ⊢ f : T 1 × . . . × T N → T Γ ⊢ E1 : T 1
Γ ⊢ f (E1, . . . , EN ) : T

. . . Γ ⊢ EN : T N

• Los operadores unarios y binarios tendrían reglas

específicas por su posición infija y prefija

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.17/36

Las reglas para las instrucciones serían:

Γ ⊢ x : T Γ ⊢ E : T
Γ ⊢ x := E : Instr

Γ ⊢ I1 : Instr Γ ⊢ I2 : Instr

Γ ⊢ I1; I2 : Instr

Γ ⊢ E : booleano Γ ⊢ I1 : Instr Γ ⊢ I2 : Instr

Γ ⊢ Si E entonces I1 sinoI2 : Instr

Γ ⊢ E : booleano Γ ⊢ I : Instr

Γ ⊢ mientras E hacer I fmientras : Instr

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.18/36

• La comprobación de tipos de los subprogramas

requeriría un nuevo tipo (por ejemplo Subpr)

• El entorno se tendría que actualizar con la lista de

parámetros y variables locales

• A continuación se pasaría a comprobar que el tipo

del cuerpo del subrprograma es una instrucción

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.19/36

• Finalizada la comprobación el entorno se tiene

que actualizar con el nombre del subprograma y el
tipo de sus parámetros para comprobar que las
llamadas a los subprogramas son correctas

• Debido a que pueden haber llamadas recursivas

esta actualización se ha de hacer antes de
comprobar el tipo del cuerpo del subprograma

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.20/36

Ejercicio: Comprobar el tipo de la siguiente función

funcion f (x, y : entero) retorna b : booleano

x := x + 1;
y ::= y + 2;
b := x ≤ y
retorna b

ffuncion

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.21/36

Algoritmos de comprobación de
tipos

• Los compiladores de los LP no implementan

sistemas deductivos de comprobación de tipos por
ser ineficientes

• Los compiladores utilizan una tabla de símbolos
para guardar la información que tenemos en el
entorno de las reglas

• La representación del programa es mediante un

árbol sintáctico

• La comprobación de tipos requiere realizar un

recorrido recursivo del árbol sintáctico desde las
hojas hasta la raíz asociando un tipo a cada nodo

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.22/36

Reglas de inferencia con subtipo

• Recordemos que un tipo st es subtipo de un tipo t
si cualquier elemento de st puede ser utilizado en
un contexto en el que se utiliza t

• Las reglas de inferencia con subtipos tienen reglas

adicionales como la reflexividad y la transitividad
de la relación de subtipos y la regla de
subsumción.

• La regla para subsumir nos dice que cuando un
elemento es de un tipo st, ese elemento también
tiene los tipos de los supertipos de st, esto es, de
todos los tipos t de los cuales st es subtipo

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.23/36

La formalización de las reglas es la siguiente

Γ ⊢ T < T

Γ ⊢ T 1 < T 2 Γ ⊢ T 2 < T 3

Γ ⊢ T 1 < T 3

Γ ∪ {ST < T } ⊢ ST < T

Γ ⊢ expr : ST Γ ⊢ ST < T

Γ ⊢ expr : T

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.24/36

• Veamos cómo se implementa la comprobación de

tipos con subtipos

• El funcionamiento general es el mismo teniendo

una tabla de símbolos y un árbol sintáctico al que
hay que comprobar su tipo

• La tabla de símbolos contiene el menor subtipo

asociado a las variables, constantes y parámetros
de las operaciones y las relaciones de subtipos
entre los tipos

• El proceso recursivo es el mismo de las hojas a la

raíz pero con comprobaciones adicionales

Nikos Mylonakis, UPC (Spain)

March 4, 2010 – p.25/36

• Si tenemos que f : T 1 × . . . × T N → y al re