Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
teaching:cc4101:tareas:2015-1:tarea2 [2015/04/20 23:14] – [P1 - Lenguaje base (0.5pt)] flarenasteaching:cc4101:tareas:2015-1:tarea2 [2015/05/11 14:08] (current) – [P2 - Variables fluidas (1.0pt)] flarenas
Line 20: Line 20:
 <code haskell> <code haskell>
 > run "((fun (x) (+ x 1)) 3)" > run "((fun (x) (+ x 1)) 3)"
-4+NumV 4
 </code> </code>
  
Line 38: Line 38:
            (flet (x 10)            (flet (x 10)
              (f 1))))")              (f 1))))")
-11+NumV 11
 </code> </code>
  
Line 46: Line 46:
 En esta parte, vamos a equipar el lenguaje de la Parte 1 con un sistema de //inferencia de tipos//. Esto significa que, al igual que en Haskell, vamos a checkear que un programa este bien tipado, //sin requerir anotaciones de tipos en el código fuente//. En esta parte, vamos a equipar el lenguaje de la Parte 1 con un sistema de //inferencia de tipos//. Esto significa que, al igual que en Haskell, vamos a checkear que un programa este bien tipado, //sin requerir anotaciones de tipos en el código fuente//.
  
-El capítulo 30 del PLAI explica en detalles como funciona un inferenciador monomórfico (si mira el PLAI, empiece leyendo desde el 30.1.1, dado que el caso polimórfico no nos interesa en esta tarea). +El capítulo 30 del PLAI explica en detalles como funciona un inferenciador monomórfico (Si estudia desde el libro PLAI, empiece leyendo desde el 30.1.1, dado que el caso polimórfico no nos interesa en esta tarea). 
  
-Un inferenciador de tipos funciona de manera distinta a un verificador de tipos "tradicional" como los que ya vimos en clase. En particular, el sistema de tipos usa //variables de tipos// para denotar cada tipo desconocido, y genera, al analizar un programa, una lista de constraints sobre estas variables. +Un inferenciador de tipos funciona de manera distinta a un verificador de tipos "tradicional" como los que ya vimos en clase. En particular, el sistema de tipos usa //variables de tipos// para denotar cada tipo desconocido y genera, al analizar un programa, una lista de constraints sobre estas variables. 
  
-Por ejemplo, si ve ''%%(fun (x) (+ x 1)%%'', genera una nueva variable de tipo ''T1'' para denotar el tipo desconocido de ''x'', y luego, mirando el cuerpo de la función, genera la constraint ''T1=TNum'' para reflejar que esta es la única forma con que la función pueda ser bien tipada. El sistema de tipo produce finalmente que la expresión tiene el tipo ''T1->TNum'' con la constraint de que ''T1=TNum''. Finalmente, aplicando la substitución de ''T1'' por ''TNum'', retorna al usuario que la expresión tiene el tipo ''(num->num)'':+Por ejemplo, si ve ''%%(fun (x) (+ x 1))%%'', genera una nueva variable de tipo ''T1'' para denotar el tipo desconocido de ''x''. Luego, mirando el cuerpo de la función, genera la constraint ''T1=TNum'' para reflejar que esta es la única forma con que la función pueda estar bien tipada. El sistema de tipo produce finalmente que la expresión tiene el tipo ''T1->TNum'' con la constraint ''T1=TNum''. Finalmente, aplicando la substitución de ''T1'' por ''TNum'', retorna al usuario que la expresión tiene el tipo ''(num->num)'':
  
 <code haskell> <code haskell>
-> type-run "(fun (x) (+ x 1))"+> runType "(fun (x) (+ x 1))"
 (num->num) (num->num)
 </code> </code>
Line 59: Line 59:
 Más precisamente, el inferenciador tiene tres etapas: Más precisamente, el inferenciador tiene tres etapas:
  
-  - generar todas las constraints, sin preocuparse de si son consistentes o no (es decir, sin preocuparse de si existe una solución para todas las variables de tipos tal que todas las ecuaciones sean satisfechas). Los únicos errores que se botan en esta etapa son las de identificadores libres. +  - Generar todas las constraints sin preocuparse de si son consistentes o no (es decir, sin preocuparse de si existe una solución para todas las variables de tipos tal que todas las ecuaciones sean satisfechas). Los únicos errores que se botan en esta etapa son los de identificadores libres. 
-  - aplicar un algoritmo de //unificación// para determinar si existe una solución, y cual es. Si no hay solución, entonces es un error de tipo.  +  - Aplicar un algoritmo de //unificación// para determinar si existe una solución, y cual es. Si no hay solución, entonces es un error de tipo.  
-  - si existe una solución, está es utilizada para reportar el tipo del programa.+  - Si existe una solución, ésta es utilizada para reportar el tipo del programa.
  
 === A. Representar tipos y constraints === === A. Representar tipos y constraints ===
Line 72: Line 72:
 </code> </code>
  
-donde ''TVar Symbol'' es una variable de tipo con un ''Symbol'' único. Cada vez que se necesite definir una nueva variable de tipo, se debe ejecutar ''newTVar 0'' para adquirir un nuevo ''Symbol''. La definición de ''newTVar'' está incluida en el archivo adjunto al enunciado de la tarea. **agregar link al archivo desde aquí mismo--esto //es// el enunciado**+donde ''TVar Symbol'' es una variable de tipo con un ''Symbol'' único. Cada vez que se necesite definir una nueva variable de tipo, se debe ejecutar ''newTVar 0'' para adquirir una nueva variable de tipo con un ''Symbol'' único. Para la definición de ''newTVar'' debe considerar las siguientes librerias y definiciones:
  
-Asegúrese de definir una forma adecuada de comparar tipos (''Eq''), así como imprimirlos (''Show''). Vea más abajo para detalles de como se espera que se impriman los tipos.+<code haskell> 
 +import Data.Unique 
 +import System.IO.Unsafe 
 + 
 +type Symbol = Unique 
 + 
 +newTVar _ = TVar (unsafePerformIO newUnique) 
 +</code> 
 + 
 +Asegúrese de definir una forma adecuada de comparar tipos (''Eq'') y también para imprimirlos (''Show''). Vea más abajo para detalles de como se espera que se impriman los tipos.
  
 Finalmente, una constraint ''T1=T2'' se puede representar simplemente como un par de tipos: Finalmente, una constraint ''T1=T2'' se puede representar simplemente como un par de tipos:
Line 85: Line 94:
 Estudie el capitulo 30.2 del PLAI para una explicación detallada de como generar constraints. Estudie el capitulo 30.2 del PLAI para una explicación detallada de como generar constraints.
  
-Defina la función ''%%typeof :: Expr -> TEnv -> [Const] -> (Type, [Const])%%'' que dada una expresión ''Expr'', un ambiente de tipos ''TEnv'' y una lista de constraints ''[Const]'', ''typeof'' retorna el tipo de la expresión con la lista de constraints. La función reporta errores solo en caso de identificadores libres; si la lista de constrains generada no es consistente, no retorna errores.+Defina la función ''%%typeof :: Expr -> TEnv -> (Type, [Const])%%'' que dada una expresión ''Expr'' y un ambiente de tipos ''TEnv'', retorna el tipo de la expresión con la lista de constraints que debe ser solucionable para que el programa sea válido en tipos. La función reporta errores solo en caso de identificadores libres; si la lista de constraints generada no es consistente, no retorna errores.
  
 === C. Unificación === === C. Unificación ===
  
-Si bien el algoritmo de unificación esta descrito en el PLAI, existe una descripción más concisa y simple, proveniente de otro libro (//Types and Programming Languages//, B. Pierce):+Si bien el algoritmo de unificación está descrito en el PLAI, existe una descripción más concisa y simple, proveniente de otro libro (//Types and Programming Languages//, B. Pierce):
  
 {{ :teaching:cc4101:tareas:2015-1:unification.png?nolink |}} {{ :teaching:cc4101:tareas:2015-1:unification.png?nolink |}}
Line 95: Line 104:
 Considere que en esta definición: //C// es el conjunto de constraints (''[Const]''), //S// y //T// son metavariables que son cualquier tipo, //T = X// como condición expresa que //T// es una variable de tipo (''TVar x''), //[X -> T]C// es la substitución de //T// por //X// en //C//, y //X \notin FV(T)// es para checkear que la variable X no ocurre en T (ver la discusión del //occurs check// en PLAI 30.5 o TAPL o wikipedia). Considere que en esta definición: //C// es el conjunto de constraints (''[Const]''), //S// y //T// son metavariables que son cualquier tipo, //T = X// como condición expresa que //T// es una variable de tipo (''TVar x''), //[X -> T]C// es la substitución de //T// por //X// en //C//, y //X \notin FV(T)// es para checkear que la variable X no ocurre en T (ver la discusión del //occurs check// en PLAI 30.5 o TAPL o wikipedia).
  
-Defina la función ''%%unify :: [Const] -> [Const]%%'' que dada una lista de constrains retorna una lista de substitución. Una substitución es una ecuación ''T1=T2'' donde ''T1'' es una variable de tipo. En caso de que la lista posea inconsistencias, arroja un error.+Defina la función ''%%unify :: [Const] -> [Const]%%'' que dada una lista de constraints retorna una lista de substitución. Una substitución es una ecuación ''T1=T2'' donde ''T1'' es una variable de tipo. En caso de que la lista posea inconsistencias, arroja un error.
  
  
Line 104: Line 113:
 Defina la función ''apply :: [Const] -> Type -> Type'' que dado una lista de substituciones y un tipo ''t'' (que típicamente contiene variables de tipos), aplica dicha substitución para obtener una versión legible del tipo. Defina la función ''apply :: [Const] -> Type -> Type'' que dado una lista de substituciones y un tipo ''t'' (que típicamente contiene variables de tipos), aplica dicha substitución para obtener una versión legible del tipo.
  
-Finalmente defina la función ''type-run :: String -> Type'' que dado un programa fuente como string, retorna su tipo (o arroja un error).+Finalmente defina la función ''runType :: String -> Type'' que dado un programa fuente como string, retorna su tipo (o arroja un error).
  
 **Ejemplos**: **Ejemplos**:
  
-Se debe respetar el output **exacto** siguiendo el formato de los ejemplos presentados a continuación, donde ''type-run'' es una función que retorna el tipo de una expresión dada como string:\\+Se debe respetar el output **exacto** siguiendo el formato de los ejemplos presentados a continuación, donde ''runType'' es una función que retorna el tipo de una expresión dada como string:\\
  
 <code haskell> <code haskell>
  
-> trun "(fun (x) (+ x 1))"+> runType "(fun (x) (+ x 1))"
 (num->num) (num->num)
  
-> trun "(fun (x) x)"+> runType "(fun (x) x)"
 (?1->?1) (?1->?1)
  
-> trun "(fun (x) 3)"+> runType "(fun (x) 3)"
 (?1->num) (?1->num)
  
-> trun "x"+> runType "x"
 *** Exception: free identifier x *** Exception: free identifier x
  
-> trun "((fun (x) (+ x 1)) (fun (x) x))"+> runType "((fun (x) (+ x 1)) (fun (x) x))"
 *** Exception: Type error: cannot unify num with (?1->?1) *** Exception: Type error: cannot unify num with (?1->?1)
 </code> </code>