| Both sides previous revisionPrevious revisionNext revision | Previous revision |
| people:etanter:tipos [2013/05/02 17:51] – etanter | people:etanter:tipos [2013/06/04 13:12] (current) – etanter |
|---|
| //draft de artículo para la revista BITs de Ciencias - Last updated May 1st, 2013// | //draft de artículo para la revista BITs de Ciencias - Last updated May 17, 2013// |
| |
| ====== Tipos: Garantías a Medida ====== | ====== Tipos: Garantías a Medida ====== |
| 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. | 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?"). | 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. |
| | |
| | ------- |
| | **FIGURA 1: Verificación estática**\\ |
| | [[http://pleiad.cl/_media/people/etanter/verificacion.png|{{people:etanter:verificacion.png?900}}]] |
| | ------- |
| | |
| | El campo de la verificación de programas es por ende un pozo sin fin, un eterno compromiso entre la expresividad requerida para lo que se quiere verificar, y la amenaza de la indecidibilidad. En la práctica, muchas veces uno quiere la garantía absoluta que todos los programas malos son rechazados. Esto significa que los sistemas de verificación son conservadores: sólo reportan que un programa cumple una cierta propiedad cuando lo pudieron demostrar, pero inevitablemente van a rechazar algunos programas que sí cumplen la propiedad (Figura 1c). |
| |
| El campo de la verificación de programas es por ende un pozo sin fin, un eterno compromiso entre la expresividad requerida para lo que se quiere verificar, y la amenaza de la indecidibilidad. Lo que se traduce en la práctica en sistemas de verificación conservadores, que se dedican a la semi-decidabilidad. Es decir, sistemas que sólo reportan que un programa cumple una cierta propiedad cuando lo pudieron demostrar, pero que rechazan programas donde no se puede demostrar dicha propiedad, a pesar de que posiblemente el programa la cumpla. | |
| Mientras que las técnicas más avanzadas de verificación de software, como el análisis formal y la verificación de modelos, no han tenido mucha aceptación en la industria de software--excepto en áreas críticas donde la correctitud absoluta es una necesidad vital (automóviles, cohetes, etc.)--existe una forma liviana de métodos formales que cada programador usa día a día, muchas veces sin preguntarse mucho de qué se trata: los sistemas de tipos. | Mientras que las técnicas más avanzadas de verificación de software, como el análisis formal y la verificación de modelos, no han tenido mucha aceptación en la industria de software--excepto en áreas críticas donde la correctitud absoluta es una necesidad vital (automóviles, cohetes, etc.)--existe una forma liviana de métodos formales que cada programador usa día a día, muchas veces sin preguntarse mucho de qué se trata: los sistemas de tipos. |
| |
| **¿Sistemas de tipos?** | **¿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. | 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. |
| **¡Coherencia, por favor!** | **¡Coherencia, por favor!** |
| |
| Una propiedad fundamental que se espera de un sistema de tipos, es que las predicciones de tipos sean coherentes con la ejecución del programa. Por ejemplo, si el sistema de tipos dice que un programa es válido y de tipo numérico, entonces ejecutarlo debería producir un valor de tipo numérico. Por más sorprendente que parezca, ciertos lenguajes carecen de esta propiedad. Por ejemplo, en C, el sistema de tipos no es coherente con la ejecución de los programas, lo que lleva a un estado extraño en el cual el sistema de tipos no asegura nada. Esto es porque el modelo de ejecución de C, de muy bajo nivel, no garantiza que se respeten las abstracciones establecidas al nivel del código fuente, y verificadas por el sistema de tipos. La consecuencia de esto son los famosos "errores de segmentación" y otras joyas del "comportamiento no-definido" que todo programador C ha llegado a apreciar en su justo valor. | Una propiedad fundamental que se espera de un sistema de tipos, es que las predicciones de tipos sean coherentes con la ejecución del programa. Por ejemplo, si el sistema de tipos dice que un programa es válido y de tipo numérico, entonces ejecutarlo debería producir un valor de tipo numérico. Por más sorprendente que parezca, ciertos lenguajes carecen de esta propiedad. Por ejemplo, en C, el sistema de tipos no es coherente con la ejecución de los programas, lo que lleva a un estado extraño en el cual el sistema de tipos no asegura nada. Esto es porque el modelo de ejecución de C, de muy bajo nivel, no garantiza que se respeten las abstracciones establecidas al nivel del código fuente, y verificadas por el sistema de tipos. La consecuencia de esto son los famosos "errores de segmentación" y otras joyas del "comportamiento no-definido" que todo programador C ha llegado a apreciar en su justo valor. Para volver a la Figura 1, el verificador de tipos de C corresponde al caso 1e: incompleto, e incorrecto. |
| |
| Volviendo a lenguajes civilizados, un sistema de tipos puede ser visto como un sistema de demostración formal de que ciertos errores no ocurrirán en tiempo de ejecución. El costo a pagar por esta firme garantía es que el programador debe convencer al sistema de tipos que su programa cumple con las exigencias establecidas. Surgen nuevamente los monstruos de la indecidibilidad, y el necesario conservadurismo de la verificación de tipos. La consecuencia práctica es que en algunos casos, un programa válido será rechazado por el sistema de tipos. Frente a este problema, hay dos puertas para avanzar. | Volviendo a lenguajes civilizados, un sistema de tipos puede ser visto como un sistema de demostración formal de que ciertos errores no ocurrirán en tiempo de ejecución. El costo a pagar por esta firme garantía es que el programador debe convencer al sistema de tipos que su programa cumple con las exigencias establecidas. Surgen nuevamente los monstruos de la indecidibilidad, y el necesario conservadurismo de la verificación de tipos. La consecuencia práctica es que en algunos casos, un programa válido será rechazado por el sistema de tipos (Figura 1c). Frente a este problema, hay dos puertas para avanzar. |
| |
| **Promesas de tipos** | **Promesas de tipos** |
| **Mejores tipos** | **Mejores tipos** |
| |
| La segunda puerta es mejorar el sistema de tipos, haciéndolo más expresivo. Un ejemplo clásico de esta vía es la introducción en Java 1.5 de los "generics", es decir, del polimorfismo paramétrico, tal como se encuentra en los lenguajes ML y Haskell. Anteriormente, el sistema de tipos de Java sólo razonaba en base a polimorfismo de subtipos, es decir, el hecho de que un objeto es aceptable en un lugar donde se espera que tenga algún tipo A si entiende un conjunto de mensajes más amplio que el especificado por A. Dicho sistema de tipos era sin embargo muy limitado al momento de usar colecciones de objetos, dado que no permite especificar el tipo de los elementos contenidos dentro de una colección. Esto obligaba los programadores a hacer uso de casts de manera muy frecuente, lo que a su vez, disminuyó mucho la relevancia misma del sistema de tipos, al dejar la puerta abierta a muchos errores en tiempo de ejecución. La introducción de los generics en Java resolvió este problema, permitiendo al programador especificar el tipo de los elementos contenidos en una colección. Pero esta mejora aumentó considerablemente la complejidad del sistema de tipos, dado que la interacción entre el polimorfismo de subtipos y el polimorfismo paramétrico no es trivial. | La segunda puerta es mejorar el sistema de tipos, haciéndolo más expresivo, y así reducir el monto de programas válidos que son rechazados. Un ejemplo clásico de esta vía es la introducción en Java 1.5 de los "generics", es decir, del polimorfismo paramétrico, tal como se encuentra en los lenguajes ML y Haskell. Anteriormente, el sistema de tipos de Java sólo razonaba en base a polimorfismo de subtipos, es decir, el hecho de que un objeto es aceptable en un lugar donde se espera que tenga algún tipo A si entiende un conjunto de mensajes más amplio que el especificado por A. Dicho sistema de tipos era sin embargo muy limitado al momento de usar colecciones de objetos, dado que no permite especificar el tipo de los elementos contenidos dentro de una colección. Esto obligaba los programadores a hacer uso de casts de manera muy frecuente, lo que a su vez, disminuyó mucho la relevancia misma del sistema de tipos, al dejar la puerta abierta a muchos errores en tiempo de ejecución. La introducción de los generics en Java resolvió este problema, permitiendo al programador especificar el tipo de los elementos contenidos en una colección. Pero esta mejora aumentó considerablemente la complejidad del sistema de tipos, dado que la interacción entre el polimorfismo de subtipos y el polimorfismo paramétrico no es trivial. |
| |
| **Tipos dinámicos** | **Tipos dinámicos** |
| **¿Qué tan útiles son estos tipos?** | **¿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. | 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. |
| La verificación basada en tipos tiene un alto potencial de ser adoptada en la industria, por múltiples razones. Primero, no apunta a la verificación de propiedades globales de un sistema completo. Aún con tipos dependientes, nunca es necesario establecer un teorema sobre el sistema en su globalidad. Solamente se expresan propiedades locales. La conexión lógica entre estas propiedades locales y las propiedades globales que se desean no se verifica. La experiencia con otras técnicas de verificación formal muestra que apuntar a verificar dicho razonamiento global es un tremendo esfuerzo, fuera del alcance para la mayoría de la industria del software. Segundo, los programadores ya están acostumbrados a desarrollar en lenguajes con tipos estáticos. Si bien los sistemas de tipos que se exploraron aquí son semánticamente bastante más ricos que los tipos tradicionales, la metodología de programación es muy cercana. No es necesario aprender un nuevo lenguaje de modelamiento o una nueva herramienta de análisis. La integración fuerte entre programar, especificar, y verificar es un factor de adopción importante. Podemos prever un escenario de adopción progresiva de estas técnicas de verificación, con sistemas de tipos con una semántica paulatinamente más rica. De hecho, este escenario ya se hizo realidad cuando Java adoptó el polimorfismo paramétrico en su versión 1.5, y ahora con el lenguaje Scala--cuyo sistema de tipos es mucho más avanzado que el de Java--que está progresivamente reemplazando a Java en muchas aplicaciones (p.ej. Twitter y LinkedIn). Además, es posible diseñar sistemas de tipos muy expresivos que sean graduales, con tal de que no sea necesario demostrar todas las propiedades a la vez, sino que se puedan dejar varias a cargo de una verificación dinámica, e ir elaborando la verificación estática paso a paso. | La verificación basada en tipos tiene un alto potencial de ser adoptada en la industria, por múltiples razones. Primero, no apunta a la verificación de propiedades globales de un sistema completo. Aún con tipos dependientes, nunca es necesario establecer un teorema sobre el sistema en su globalidad. Solamente se expresan propiedades locales. La conexión lógica entre estas propiedades locales y las propiedades globales que se desean no se verifica. La experiencia con otras técnicas de verificación formal muestra que apuntar a verificar dicho razonamiento global es un tremendo esfuerzo, fuera del alcance para la mayoría de la industria del software. Segundo, los programadores ya están acostumbrados a desarrollar en lenguajes con tipos estáticos. Si bien los sistemas de tipos que se exploraron aquí son semánticamente bastante más ricos que los tipos tradicionales, la metodología de programación es muy cercana. No es necesario aprender un nuevo lenguaje de modelamiento o una nueva herramienta de análisis. La integración fuerte entre programar, especificar, y verificar es un factor de adopción importante. Podemos prever un escenario de adopción progresiva de estas técnicas de verificación, con sistemas de tipos con una semántica paulatinamente más rica. De hecho, este escenario ya se hizo realidad cuando Java adoptó el polimorfismo paramétrico en su versión 1.5, y ahora con el lenguaje Scala--cuyo sistema de tipos es mucho más avanzado que el de Java--que está progresivamente reemplazando a Java en muchas aplicaciones (p.ej. Twitter y LinkedIn). Además, es posible diseñar sistemas de tipos muy expresivos que sean graduales, con tal de que no sea necesario demostrar todas las propiedades a la vez, sino que se puedan dejar varias a cargo de una verificación dinámica, e ir elaborando la verificación estática paso a paso. |
| |
| Encontrar un sabio equilibrio entre la complejidad de la programación verificada y sus beneficios en términos de correctitud es un desafiante problema de ingeniería de software, que merece ser estudiado en profundidad. Dada la enorme dependencia de nuestra sociedad en los sistemas de software, es de esperar que la programación verificada se volverá una práctica común, contribuyendo ampliamente a la correctitud del software que usamos día a día. | Encontrar un sabio equilibrio entre la complejidad de la programación verificada y sus beneficios en términos de correctitud es un desafiante problema de ingeniería de software, que merece ser estudiado en profundidad. Dada la enorme dependencia de nuestra sociedad en los sistemas de software, es de esperar que la programación verificada se vuelva una práctica común, contribuyendo ampliamente a la correctitud del software que usamos día a día. |
| |
| |
| |
| -------- | -------- |
| **FIGURA 1: La Correspondencia de Curry-Howard** | **FIGURA 2: La Correspondencia de Curry-Howard** |
| |
| La correspondencia de Curry-Howard establece un puente entre tipos y proposiciones lógicas, y programas y demostraciones de dichas proposiciones. Fue descubierta y refinada por los matemáticos Haskell Curry y William A. Howard. | La correspondencia de Curry-Howard establece un puente entre tipos y proposiciones lógicas, y programas y demostraciones de dichas proposiciones. Fue descubierta y refinada por los matemáticos Haskell Curry y William A. Howard. |
