Differences

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

--- people:etanter:tipos [2013/05/17 21:52] – etanter
+++ people:etanter:tipos [2013/06/04 13:02] – etanter
@@ Line 7: / Line 7: @@
 Desde que aparecieron los ensambladores, hasta hoy, el desarrollo de software se apoya de manera esencial en herramientas computacionales cuyo objetivo es permitir al programador abstraerse de detalles de bajo nivel (como la ubicación exacta de los datos en memoria) para concentrarse en el desarrollo de soluciones expresadas en términos de conceptos inteligibles por humanos y fácilmente comunicables. El alto nivel de abstracción provisto por los lenguajes de programación, que incluye la posibilidad de construir nuevas abstracciones dedicadas (procedimientos, funciones, tipos de datos abstractos, clases, librerías, frameworks), es un habilitador crucial en el desarrollo de los sistemas altamente complejos sobre los cuales nuestra sociedad se construye.
-Idealmente, uno quisiera tener, al mismo tiempo que está programando, la garantía de que el programa así desarrollado es correcto. Correcto, en el sentido de que computa lo que se espera que compute, y que lo haga de la manera que uno espera (por ejemplo respecto del uso de recursos). Sin embargo, hay una mala noticia: la gran mayoría de las propiedades interesantes que uno quiere asegurar son indecidibles (partiendo con la propiedad aparentemente muy simple "¿este programa termina?"). La Figura 1 ilustra esta problemática, y las distintas posibilidades a considerar.
+Idealmente, uno quisiera tener, al mismo tiempo que está programando, la garantía de que el programa desarrollado es correcto. Correcto, en el sentido de que computa lo que se espera que compute, y que lo haga de la manera que uno espera (por ejemplo respecto del uso de recursos). Sin embargo, hay una mala noticia: la gran mayoría de las propiedades interesantes que uno quiere asegurar son indecidibles (partiendo con la propiedad aparentemente muy simple "¿este programa termina?"). La Figura 1 ilustra esta problemática, y las distintas posibilidades a considerar.
 -------
@@ Line 20: / Line 20: @@
 **¿Sistemas de tipos?**
-El objetivo de un sistema de tipos es asegurar estáticamente--es decir antes de la ejecución del programa--que ciertos errores nunca ocurren en tiempo de ejecución. ¿Cuáles son estos errores? Típicamente, se trata de errores "simples" como el aplicar una operación primitiva a valores inadecuados, como lo es multiplicar dos valores que no son numéricos. Para operar, un sistema de tipos clasifica las expresiones de un programa según el tipo de valores que pueden producir. Luego, verifica que solamente se usan expresiones de tipos adecuados en lugares adecuados. Por ejemplo, si e1 y e2 son expresiones, la expresión e1 + e2 es válida en tipos solamente si e1 y e2 son expresiones válidas de tipo numérico; de ser así, la expresión e1 + e2 misma es válida, y tiene un tipo numérico. Esta clasificación de tipos se puede basar en anotaciones de tipo que el programador escribe explícitamente en el programa (como en C y Java), o pueden ser inferidas por el mismo sistema de tipos (como en ML y Haskell).
+El objetivo de un sistema de tipos es asegurar estáticamente--es decir antes de la ejecución del programa--que ciertos errores nunca ocurren en tiempo de ejecución. ¿Cuáles son estos errores? Típicamente, se trata de errores "simples" como aplicar una operación primitiva a valores inadecuados, como lo es multiplicar dos valores que no son numéricos. Para operar, un sistema de tipos clasifica las expresiones de un programa según el tipo de valores que pueden producir. Luego, verifica que solamente se usan expresiones de tipos adecuados en lugares adecuados. Por ejemplo, si e1 y e2 son expresiones, la expresión e1 + e2 es válida en tipos solamente si e1 y e2 son expresiones válidas de tipo numérico; de ser así, la expresión e1 + e2 misma es válida, y tiene un tipo numérico. Esta clasificación de tipos se puede basar en anotaciones de tipo que el programador escribe explícitamente en el programa (como en C y Java), o pueden ser inferidas por el mismo sistema de tipos (como en ML y Haskell).
 Una característica muy importante de los sistemas de tipos, y una razón decisiva de su amplia adopción en la industria, es la componibilidad: para poder verificar un componente solamente se necesita conocer los tipos de los componentes con los cuales interactúa, y no sus definiciones exactas. Esto diferencia los sistemas de tipos de los análisis estáticos que requieren poder analizar todo el código fuente de un sistema a la vez. Por ejemplo, considerando una función, basta conocer el tipo de sus argumentos, y los tipos de las funciones que llama, para determinar si tiene un tipo de retorno bien definido, y cuál es. Además, si el programador especificó el tipo de retorno esperado, se puede corroborar que la definición de la función cumple esta expectativa. En resumen, los tipos sirven como contratos que rigen las interacciones entre los componentes de un sistema, permitiendo el desarrollo independiente de los componentes y validando su integración.