Clases y herencia

1 Estudio de let con inicialización

Dado este código

let x: T0 <- e0 in e1

Tenemos que deducir el tipo del objeto:

2 Subtipos

Un orden parcial en una jerarquía de tipos es una relación binaria \(\le\) tal que cumple:

• \(X\le X\)
• \(X\le Y\) si \(X\) es un subtipo de \(Y\)
• Si \(X\le Y\) y \(Y\le Z\) entonces \(X\le Z\)

3 Subtipos

4 Subtipos

5 Subtipos

6 Un ejemplo más complicado

if e0 then e1 else e2 fi

Si \(e1\) tiene tipo \(T1\) y \(e2\) tiene tipo \(T2\), ¿qué tipo tiene que devolver esta expresión?

7 Mínimo común ancestro

El mínimo común ancestro (least common ancestor) de dos clases \(X,Y\) es la única clase \(Z\) que cumple \(X\le Z\) y \(Y\le Z\) y si otra clase \(W\) cumple \(X\le W\), \(Y\le W\) entonces \(Z\le W\).

8 Mínimo común ancestro

9 Tipos y evaluación de métodos

Cuando tenemos un método, ¿qué tipo tenemos que inferir?

10 Notas sobre cool

• Métodos y objetos pueden tener el mismo identificado
  • Hay dos ámbitos, uno para metodos y otro para objetos.
  • Para los métodos, lo llamaremos \(M\) y para objetos \(O\)
• \(M(C,f)=(T_1,\ldots,T_{n+1})\) da información de los argumentos y el retorno

11 Reglas

12 Pregunta

Demostrar que, con el siguiente árbol:

si \(O(x) = c3, O(y) = c1\) y \(M(f,c1)= (c1,c1)\), el tipo de \(x.f(y.f(x))\) es \(c1\).

13 Implementación de inferencia de tipos

Se traduce a código a:

typecheck(Environment,e1+e2){
T1 = typecheck(Environment, e1);
T2 = typecheck(Environment, e1);
Check T1 == T2 == Int;
return Int;
}

14 Implementación de inferencia de tipos

Se traduce a código a:

typecheck(Environment, let x:T <- e0 in e1 ){
T1 = typecheck(Environment, e0);
T2 = typecheck(Environment.add(x:T), e1);
Check(T0,T1);
return T1;
}