Sistemas de tipado

  1. Que es un tipo?
  2. Tipado simple
  3. Relacion de tipado
  4. Tipado de valores y expresiones
  5. Derivaciones
  6. Algoritmo de validacion: small step y big step
  7. Tipo "funcion"
  8. Ejemplo: Int <=> String
  9. Intervalo
  10. Presentacion Lab2

Para que sirven los tipos?

  • Verificar ciertas propiedades del programa, como la validez
  • Documentacion
  • Como ayuda al compilador

Tipado simple

A cada expresion se le asigna un unico tipo.

Esto es en contraste a otros sistemas donde, por ejemplo, un Perro puede ser tambien un Animal y una funcion que acepte Animal puede recibir a Perro como parametro

Relacion de tipado

La relacion de tipado es ternaria: relaciona un contexto, una variable y un tipo.

El contexto indica el significado de cada variable.

Relacion de tipado

No significa lo mismo x dentro de
fun x -> x * 2
que en
fun x y -> (x && y)
En la primera x es un entero y en la segunda un booleano.

Relacion de tipado

Esta relacion se escribe $\Gamma \vdash t : T$, significando que en el contexto $\Gamma$ la variable $t$ es del tipo $T$

Tipado de valores y expresiones

A los valores (expresiones irreducibles) se les asigna un tipo al cual pertenecen. Por ejemplo 3 es entero. A las expresiones se les obtiene el tipo aplicando una serie de derivaciones (aplicaciones de reglas)

Reglas de tipado

Producen a una relacion de tipado. Por ejemplo: $$\frac{\Gamma \vdash t_1 : Entero, t_2: Entero}{\Gamma \vdash t_1 + t_2: Entero}$$ Esto significa que si sumo cosas, y estas cosas son enteros (premisa), obtengo un entero $$\Gamma \vdash false: Booleano$$ Esto significa que false es un booleano.

Derivaciones

Usando varias reglas de tipado, puedo llegar a la conclusion que cierta expresion es de un tipo. Por ejemplo si tengo las reglas: $$\Gamma \vdash LiteralEntero: Entero$$ $$\frac{\Gamma \vdash t_1 : Entero, t_2: Entero}{\Gamma \vdash t_1 + t_2: Entero}$$ Puedo deducir que (2 + 3) + 4 es de tipo entero.

Como validar tipos simples: small step

Es posible validar tipos de un paso a la vez, empezando por los valores cuyo tipo es conocible sin premisa.
En el caso de (2+3)+4 primero concluyo que 2 es un entero, luego que 3 y que 4.
Despues obtengo que 2+3 es entero porque es suma de enteros. Lo mismo para (2+3)+4 llegando a la conclusion deseada.
Esto es small step.

Como validar tipos simples: big step

Tambien se puede empezar desde la raiz y descender recursivamente.
Tengo (2+3)+4. Miro que hay a la izquierda. 2+3 es una suma por lo que reviso que 2 y 3 sean enteros.
Mira a la derecha, entero. Como los dos son enteros el tipo de todo es entero.

Tipo funcion

El tipo de las funciones se representa como $P \rightarrow R$ donde P es el tipo del parametro y R el del resultado. Al verificarlas, se debe asegurar que su cuerpo consiste de una expresion que, reemplazando el parametro por un valor de tipo P devuelve un valor de tipo R. Al ser llamadas se debe verificar que el tipo del parametro sea el esperado.

Ejemplo: Int <=> String

Tengo un sistema con literales de cadena y entero, suma (comun y concatenacion) y multiplicacion (comun y repeticion). Como en python. 

					2         # 2
					2 * 3     # 6
					2 + 2     # 4
					"a" + "b" # "ab"
					3 * "a"   # "aaa"
					"a" * "b" # invalido
					"a" + 1   # invalido

Ejemplo: Int <=> String

Esto se podria representar con las siguientes reglas: $$LiteralNumerico: Entero$$ $$LiteralCadena: Cadena$$ $$\frac{\Gamma \vdash t_1 : Entero, t_2: Entero}{\Gamma \vdash t_1 + t_2: Entero}$$ $$\frac{\Gamma \vdash t_1 : Cadena, t_2: Cadena}{\Gamma \vdash t_1 + t_2: Cadena}$$ $$\frac{\Gamma \vdash t_1 : Entero, t_2: Entero}{\Gamma \vdash t_1 * t_2: Entero}$$ $$\frac{\Gamma \vdash t_1 : Entero, t_2: Cadena}{\Gamma \vdash t_1 * t_2: Cadena}$$ $$\frac{\Gamma \vdash t_1 : Cadena, t_2: Entero}{\Gamma \vdash t_1 * t_2: Cadena}$$

Ejemplo: Int <=> String


					type lang1 = LiteralCadena | LiteralNumerico | Suma of lang1*lang1 | Multiplicacion lang1*lang1
					type type1 = Cadena | Entero | Invalido
					
					let rec type0f lang1 = match config with
						| LiteralCadena -> Cadena
						| LiteralNumerico -> Entero
						| Suma(lhs, rhs) -> match (typeof lhs, typeof rhs) with
								| (Entero, Entero) -> Entero
								| (Cadena, Cadena) -> Cadena
								| _ -> Invalido
						| Multiplicacion(lhs, rhs) -> match (typeof lhs, typeof rhs) with
								| (Entero, Entero) -> Entero
								| (Entero, Cadena) -> Cadena
								| (Cadena, Entero) -> Cadena
								| _ -> Invalido

Intervalo

Presentacion lab2

El lab2 consiste de tres ejercicios: - El primero, consiste de dos tipos y dos operaciones para convertir entre ellos. - El segundo, es similar al ejemplo visto - El tercero agrega la complejidad de los tipos funcion