1
2 Principal Type Sepcialization of Dynamic Sum-Types Tesina de Licenciatura en Cs. de la Computación Fac. Cs. Exactas, Ingeniería y Agrimensura Universidad Nacional de Rosario IX Jornadas de Informática e Investigación Operativa Facultad de Informática Alejandro C. Russo [email protected] http://www.fceia.unr.edu.ar/~russo/
3 Introducción Program Specialization (Partial Evaluation) Source Code Residual Codes
4 Type Specialization ➔ Es una forma general de “type inference” para lograr program specialization ➔ Refinar el sistema de tipos del lenguaje residual
5 Residual Type System Residual Program Source Program Source Type System ➔ Resumiendo... Información Estática Información Dinámica
6 ➔ Introducción de un juicio (judgement) responsable de la especialización de programas Source Program Source Type Residual Program Residual Type Specialization Assignment (Free Variables) ➔ Se especifica el proceso de especialización mediante un conjunto de reglas formales
7 Source Program Residual Program
8 Source Program Residual Program
9 Source Program Residual Program
10 Source Program Residual Program Source TypeResidual Type
11 Source Program Residual Program Source TypeResidual Type
12 Source Program Residual Program Source TypeResidual Type
13 ➔ Ejemplos...
14 ¿ en qué influye esta decisión?
15 ➔ Si una expresión es polivariante, entonces puede especializarse en más de una forma ➔ Marcamos en el source program qué expresiones son polivariantes y dónde se utilizan ( poly / spec ) La expresión dentro de poly se especializó dos veces ➔ Para armar la tupla tengo que conocer todos los spec Otra especialización válida
16 ➔ ¿ Conocer todos los specs ? Hay infinitas especializaciones posibles (no relacionadas) Para especializar la función debo esperar a conocer su argumento ( ¿ especialización modular?) Problema: falta de principalidad (lack of principality)
17 Principal Type Specialization Queremos especializar en forma modular En ausencia de información ¿ Qué hacemos? Haskell
18 ➔ Queremos especializar pero, si nos falta información, diferiremos las decisiones ➔ Las decisiones afectan al código generado por la especialización ➔ Necesidad de principalidad Especialización
19 ➔ Queremos especializar pero, si nos falta información, diferiremos las decisiones ➔ Las decisiones afectan al código generado por la especialización ➔ Necesidad de principalidad Especialización
20 ➔ Queremos especializar pero, si nos falta información, diferiremos las decisiones ➔ Las decisiones afectan al código generado por la especializacion ➔ Necesidad de principalidad Especialización Evidencia de predicados ¿P ara qué nos sirve? ➔ Teoría de “Qualified Types” de Mark Jones (Ph.D. Thesis, Cambridge, 1991) ➔ Pablo E. Martínez López adaptó esta teoría para usarla en el proceso de especialización
21 Source Program Source Type Specialization Assignment (Free Variables) Conjunto de Predicados
22 ➔ El sistema P captura todas las posibles especializaciones de un source program (inclusive la principal) ➔ Si escribiera un algoritmo, ¿ qué especialización debería obtener? ➔ Especialización Principal +Mecanismo de Instanciación Automatizable = Obtengo la especialización que necesito en el momento necesario Unificar y calcular evidencia de predicados
23 ➔ Las reglas... Entailment
24 ➔ Las reglas (continuación)...
25 ➔ Ejemplos... ➔ ¿ Conocer todos los specs?
26 Principal Type Specialization of Dynamic Sum-Types ➔ Introducir la capacidad de especializar dynamic sum-types ➔ ¿ Qué queremos?
27 Desapareció una rama ¿?¿? ➔ ¿ Principalidad?
28 ➔ Este trabajo... ➔ Se extendieron los sitemas de reglas formales para poder manipular dynamic sum-types ➔ Se eliminan aquellas ramas de los cases que no son necesarias(menos código muerto) ➔ No se generan declaraciones de constructores que no se utilizan(menos código muerto) ➔ Libertad para combinar constructores y cases dinamicos con las construcciones poly y spec ➔ Se extendieron las demostraciones de la tesis de doctorado de Pablo E. Martínez López para demostrar que el sistema sigue manteniendo la noción de principalidad
29 ➔ Este trabajo (continuación II)... ➔ Se extendio el prototipo ya existente (Mónadas, Clases, etc.) ➔ Se detectaron y arreglaron algunos bugs ➔ Se implemento constraint solving (no se formalizo)
30 ¿Preguntas?