Differences

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

--- people:etanter:tipos [2013/06/04 13:02] – etanter
+++ people:etanter:tipos [2013/06/04 13:09] – etanter
@@ Line 50: / Line 50: @@
 **¿Qué tan útiles son estos tipos?**
-Una gran crítica a los sistemas de tipos tradicionales es que solamente verifican propiedades simples, y que por lo tanto, "no valen la pena". Es cierto que saber que nunca se van a sumar peras con manzanas es útil, pero más útil aún es saber que el resultado final es correcto, no solamente algún valor del tipo esperado. En los ojos de un sistema de tipos tradicional, 1 y 1000 son lo mismo (elementos de un tipo numérico), pero claramente al usuario final no le da lo mismo tener 1 o 1000 dólares en su cuenta. De manera similar, un programa que computa el resultado deseado no es muy atractivo si es que para lograrlo, hace un uso indebido de recursos o compromete la integridad del sistema. Mucho trabajo ha sido desarrollado en el área de tipos expresivos--o verificación basada en tipos, o programación certificada--donde los tipos se usan para especificar propiedades mucho más relevantes que la simple pertenencia a un conjunto de valores. En lo que queda de este artículo, quisiera mencionar brevemente tres enfoques para análisis precisos con tipos: sistemas de tipos sub-estructurales, sistemas de efectos, y tipos dependientes.
+Una gran crítica a los sistemas de tipos tradicionales es que solamente verifican propiedades simples, y que por lo tanto, "no valen la pena". Es cierto que es útil saber que nunca se van a sumar peras con manzanas, pero más útil aún es saber que el resultado final es correcto, no solamente algún valor del tipo esperado. En los ojos de un sistema de tipos tradicional, 1 y 1000 son lo mismo (elementos de un tipo numérico), pero claramente al usuario final no le da lo mismo tener 1 o 1000 dólares en su cuenta. De manera similar, un programa que computa el resultado deseado no es muy atractivo si es que para lograrlo, hace un uso indebido de recursos o compromete la integridad del sistema. Mucho trabajo ha sido desarrollado en el área de tipos expresivos--o verificación basada en tipos, o programación certificada--donde los tipos se usan para especificar propiedades mucho más relevantes que la simple pertenencia a un conjunto de valores. En lo que queda de este artículo, quisiera mencionar brevemente tres enfoques para análisis precisos con tipos: sistemas de tipos sub-estructurales, sistemas de efectos, y tipos dependientes.
-**Tipos avanzados I: sistemas sub-estructurales**
+**Tipos avanzados I: sistemas subestructurales**
 En los sistemas de tipos tradicionales, la información de tipos que utiliza el sistema para analizar un pedazo de código goza de varias características llamadas "estructurales". Por ejemplo, si se sabe que la variable a es de tipo Num y que la variable b es de tipo Bool, no importa el orden de estas premisas. Tampoco interfiere con ellas el hecho de conocer más premisas, por ejemplo que otra variable c también está definida. Además, se puede usar el conocimiento de que a es de tipo Num tantas veces que se requiera (por ejemplo para poder tipar la expresión a + a, se usa el conocimiento relativo a la variable a dos veces). Los sistemas de tipos llamados sub-estructurales son sistemas en los cuales alguna(s) de estas características no se provee; por ejemplo, donde la información relativa a una variable se tiene que usar exactamente una vez. Estos sistemas permiten verificar propiedades interesantes, fuera del alcance de los sistemas tradicionales. Un ejemplo clásico es restringir las interfaces que proveen acceso a los distintos recursos de un sistema, como archivos, locks, y memoria. Está claro que cada uno de estos recursos pasa por una serie de cambios de estado a lo largo de su vida: los archivos pueden ser abiertos o cerrados; los locks pueden ser tomados o no; y la memoria puede ser asignada o liberada. Los sistemas de tipos sub-estructurales proveen mecanismos para hacer un seguimiento estático coherente de estos cambios de estado, con el fin de prevenir la realización de operaciones en objetos que están en un estado inválido, como lo es leer o escribir en un archivo cerrado. Los sistemas de tipos tradicionales no pueden verificar estas propiedades, y por ende las operaciones asociadas a recursos siempre pueden producir errores en tiempo de ejecución.