¿Alguna vez te preguntaste como se realiza la implementación de un sistema de tipos?
Pues, tuve esa pregunta hace algun tiempo y realizar una implementación sencilla me ayudo a entender varias cosas.
Trabajamos sobre un interprete que evalua expresiones aritméticas y expresiones sencillas como expresiones IF y LET, ver la descripción de la gramática.
Solo que este interprete no controla los tipos, por ejemplo si evaluas una expresion como:
2 + TRUE el resultado es 3.0
Si revisas la gramática, la expresión es correcta sintacticamente, pues la estructura de suma es de la forma: Expresion :+: Expresion, donde 2 y TRUE son expresiones.
Pero de acuerdo a lo que nos enseñaron a programar, debería haber una llamada de atención indicando que la función suma esta recibiendo tipos diferentes y por tanto no se puede evaluar.
A eso se llama un Sistema de tipos, es decir, tener un conjunto de modulos que controlen y determinen los tipos de los términos, funciones y estructuras que manejes.
En el caso de este interprete empezamos siguiendo la receta del buen Benjamin Pierce, analizando nuestros términos y definiendo un sistema de reglas, el cual nos ayudo en la implementación del sistema de tipos.
Bueno el caso es que definimos una estructura de datos que representaria los tipos como:
data Tipo = TBool | TDouble | TAbst [Ids] Expresion | TApl [Tipo]
TBool y TDouble, son los tipos que devuelve el interprete ej:
2 + 2 -> 4.0 es de tipo TDouble en el caso de este interprete.
TRUE && FALSE -> 0.0 es de tipo TBool. (0.0 representa el False y 1.0 representa el True)
Los otros 2 constructores son para controlar y deducir tipos de expresiones un poco mas complejas como abstracciones y aplicaciones.
Despues de definir la estructura de datos se implementa las reglas de tipificación que en este caso de reflejan en los modulos Tipo y TypeOf donde las funciones del mismo nombre respectivamente controlan que las expresiones pertenezcan a un contexto de evaluación, es decir ahora cuando pongamos expresiones como:
2 + TRUE , sale el mensaje: $>*** Exception: La funcion suma solo admite valores enteros y doubles debe ser el tipo TDouble -> TDouble -> TDouble
Lo bonito de esto es que puedes definir los tipos que quieras y tener el control sobre un lenguaje, como el caso de TBool cuyos valores son 0.0 y 1.0 en vez de True y False. Pues esto solo ha sido una experiencia de aprendizaje, pero tambien se puede definir subtipos, por ejemplo en vez de haber definido un tipo TDouble, quetal si definiamos un tipo TNum que tenga los tipos TDouble y TEntero.
Je je, pero no todo es color rosa, pues al implementar estas cosas uno puede toparse con los temibles ciclos infinitos, sip, esos malos stack overflow, que tanto dolor de cabeza dan, pues en una expresion recursiva como:
LET f = \n -> IF n==0 THEN 1 ELSE n*f(n-1) IN f(4) ; -> 24.0 (funcion factorial)
es muy facil toparse con algo asi, entonces cual es el tipo de esta función?
typeOf LET f = \n -> IF n==0 THEN 1 ELSE n*f(n-1) IN f(4)
sabemos que f recibe un TDouble, entonces f :TDouble -> T
y que devuelve? si tenemos un Entorno donde [(n,TDouble),(f, TAbst ["n"] IF n==0.....)]
si busco en mi entorno, claramente sera una respuesta infinita de que f es de tipo TAbst y cuando evalue la expresion IF de esa estructura volvere a preguntar por el tipo de f.
Bueno, la solución que se nos ocurrio fué buscar si en el tipo de f se llama a la misma funcion, en caso de ser asi, claramente es una función recursiva y toda funcion recursiva tiene su caso base, donde está el tipo que devuelve esa función, esto se refleja en la función recursiveFunction del modulo TypeOf , nose si es la mejor solución pero cuando nos topamos con este problema me causo mucha curiosidad pensar en varias alternativas, otra solución que pense fue modificar la estructura del data Tipo, pero no se me ocurrio como.
Este tipo de experiencias te hacen pensar en como realmente estan diseñados los lenguajes de programación (todos en general) y en el caso de los lenguajes funcionales, tienen una representación formal bastante decente (el poder de la matemática y su formalización)
Je je , espero no haberlos cansado, creo que lo hice un poco largo :P
Palabras clave: sistema de tipos
Comentarios
Hola Tatiana, queria preguntarte porque tienes una expresion dentro del tipo de la abstraccion lambda. Supongo que es necesario para tu algoritmo saber cual era el cuerpo?
Abajo una solucion para funciones recursivas, pero no la leas! Te quitara la diversion de descubrirla por ti misma :).
Para la funcion recursiva puedes resolverlo de la sig. manera: f inicialmente tiene un tipo A (A es una variable), luego descubres que le pasas un numero asi que f es funcion, por lo tanto: B->C (B y C son variables y cambiar B->C en vez de A en todo lado), luego sabes que B es un double ya que f recibe un double. Luego, como la multiplicacion recibe un numero, f tiene que devolver uno, por lo tanto C es double.
#1 Hola Alexey, pues si, los tipos TAbst generalmente aparecen en una aplicación dentro de en expresion LET, es decir algo asi:
LET x=1, y = TRUE, f = / a -> a + 2 IN f x
La aplicación f x tendrá que buscar en el cuerpo de LET y encuentra que f es una Abstracción en el Entorno se registra como [(x,TDouble),(y,TBool),(f, TAbst ["a"] (\ a ->a+2) ) ], entonces es necesario guardar la Expresion (\a -> a+2) de la Abstracción para encontrar su tipo y de esa forma determinar el tipo de la funcion f, pues si buscariamos directamente el tipo de la Expresion a+2, nos encontramos con que la variable a no se encuentra en el entorno, y usamos el truco de reemplazar los argumentos de la funcion de aplicación (en este caso x de la funcion f x) por los parametros de la abstracción (en este caso a), asi el entorno se actualiza a [(a,TDouble), (x,TDouble).....] . Esa es la razón por la que hay una expresión dentro del tipo TAbst
Bueno es una de las formas que se nos ocurrio resolver el problema, ¿Conocen otras?, ¿Se puede lograr sin tener que usar una Expresion en nuestras Estructuras de Datos?
OK Alexey, no he leido el último parrafo, pero tengo mucha tentación :) :) :)
Hay una cosa que no he entendido de la explicación y es si el sistema pretende ser solamente un (1) verificador de tipos o un (2) inferenciador de tipos. De acuerdo a lo que querramos el problema se puede resolver de una u otra forma. Si es (1) un verificador de tipos, entonces se trata de un lenguaje con tipado explícito, por tanto el tipo de f deberia estar explícito en la sintaxis, entonces no hay necesidad de guardar la expresión en el entorno que le llamas (yo le llamo ambiente). Por la sintaxis que tienes parece que hay que hacer (2) inferencia de tipos. Las reglas de inferencia debieran guiarte en la actualización de los entornos cuando actualizas los tipos de los nombres. No encuentro en tus reglas de tipo (que yo llamo reglas de inferencia) una regla para el let ... ups no sé buscar o no existe? Con esas reglas debiera poder construir el tipo de las expresiones del ejemplo que pones.