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/21 16:16] – [P2 - Variables fluidas (1.0pt)] 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 50: Line 50:
 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''. 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)'':+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 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: 
 + 
 +<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. 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.
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 ===
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>