| Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision |
| people:etanter:tipos [2013/05/01 12:03] – etanter | people:etanter:tipos [2013/06/04 13:01] – etanter |
|---|
| //draft de artículo para la revista BITs de Ciencias - Last updated Abril 23, 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. |
| |
| **¡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** |
| **Tipos avanzados II: efectos** | **Tipos avanzados II: efectos** |
| |
| La segunda familia de sistemas de tipos que aumenta considerablemente el rango de problemas controlables estáticamente es la de tipos de efectos. Como hemos visto, un sistema de tipos caracteriza el rango de posibles valores que puede resultar de la evaluación de una expresión, o sea, el "qué" se computa, pero no dice nada del "cómo" se obtiene el resultado. En un sistema de efectos, el tipo de una expresión también refleja los posibles efectos computacionales (acceso y escritura en memoria, entradas y salidas, etc.) que la evaluación de la expresión puede provocar. Un ejemplo seguramente muy familiar para los que han programado en Java, es el de las excepciones verificadas. En Java, el tipo de un método no solamente refleja el tipo de los argumentos y del valor retornado, sino también la posibilidad de que el método lance una excepción, la cual produce una transferencia del flujo de control desde el que lanza la excepción al que la captura. Este es un ejemplo de un efecto de control. El sistema de tipos asegura en este caso que ninguna excepción declarada puede pasar desapercibida. Una área donde se usan mucho los tipos de efectos es para evitar los infames "data races" en programación concurrente. Volviendo a nuestro programa estrella e1 + e2, el conocer estáticamente qué regiones de memoria e1 y e2 pueden leer o escribir (efectos de memoria) permite detectar si la ejecución paralela de ambas expresiones es correcta o no. | La segunda familia de sistemas de tipos que aumenta considerablemente el rango de problemas controlables estáticamente es la de tipos de efectos. Como hemos visto, un sistema de tipos caracteriza el rango de posibles valores que puede resultar de la evaluación de una expresión, o sea, el "qué" se computa, pero no dice nada del "cómo" se obtiene el resultado. En un sistema de efectos, el tipo de una expresión también refleja los posibles efectos computacionales (acceso y escritura en memoria, entradas y salidas, etc.) que la evaluación de la expresión puede provocar. Un ejemplo seguramente muy familiar para los que han programado en Java, es el de las excepciones verificadas. En Java, el tipo de un método no solamente refleja el tipo de los argumentos y del valor retornado, sino también la posibilidad de que el método lance una excepción, la cual produce una transferencia del flujo de control desde el que lanza la excepción al que la captura. Este es un ejemplo de un efecto de control. El sistema de tipos asegura en este caso que ninguna excepción declarada puede pasar desapercibida. Una área donde se usan mucho los tipos de efectos es para evitar los infames "data races" en programación concurrente: volviendo a nuestro programa estrella e1 + e2, el conocer estáticamente que e1 y e2 sólo pueden leer o escribir (efectos de memoria) en regiones de memoria disjuntas, permite garantizar que es correcto ejecutar ambas expresiones en paralelo. |
| |
| En forma relacionada, el saber que una expresión no tiene efectos computacionales (es decir, que es una expresión "pura") permite varias optimizaciones derivadas del razonamiento basado en ecuaciones, que conocemos de nuestros cursos de álgebra. Si una expresión e1 aparece múltiples veces en un programa y es pura, entonces es totalmente correcto reemplazar e1 por su valor v, porque e1 = v. Así evitamos calcular e1 varias veces. Para entender por qué esto no es cierto para cualquier expresión, considere que e1 imprime en pantalla "ok". Claramente no es lo mismo para el usuario ver una vez "ok", o verlo varias veces. Lo mismo si e1 retira 100 dólares de su cuenta. Un caso ejemplar de estas ideas es el lenguaje de programación Haskell. Haskell es un lenguaje funcional puro: todas las expresiones en Haskell son puras. Haskell no incluye ninguna forma nativa de hacer asignaciones, por ejemplo. Como todo lenguaje práctico tiene que permitir de alguna manera tener algún efecto sobre el mundo real, los diseñadores de Haskell tuvieron que ingeniar un mecanismo para soportar efectos dentro de este marco puro. Resulta que la respuesta vino del lado de las mónadas, estructuras componibles que representan computación. Sin entrar en detalles, en Haskell una función de tipo Int → Int es una función pura que, dado un entero, retorna un entero. Y nada más; el compilador puede hacer todas las optimizaciones que quiera cuando ve aplicaciones de dicha función. En cambio, si la función hace uso de entradas y salidas como imprimir en pantalla, esto se ve reflejado en su tipo, que pasa a ser Int → IO Int, donde IO es la mónada de los efectos de entradas y salidas. Existen mónadas para excepciones, continuaciones, estado compartido, no-determinismo, etc. Y obviamente un programador puede definir sus propios efectos, por ejemplo si quiere razonar sobre el flujo de valores en el programa, lo cual tiene aplicaciones en seguridad. Esta disciplina, por más estricta que sea, fomenta un estilo de programación donde se separa el manejo de efectos de las partes más computacionales de un sistema, lo que mejora su modularidad al mismo tiempo que permite más razonamiento estático, incluyendo más optimizaciones. | En forma relacionada, el saber que una expresión no tiene efectos computacionales (es decir, que es una expresión "pura") permite varias optimizaciones derivadas del razonamiento basado en ecuaciones, que conocemos de nuestros cursos de álgebra. Si una expresión e1 aparece múltiples veces en un programa y es pura, entonces es totalmente correcto reemplazar e1 por su valor v, porque e1 = v. Así evitamos calcular e1 varias veces. Para entender por qué esto no es cierto para cualquier expresión, considere que e1 imprime en pantalla "ok". Claramente no es lo mismo para el usuario ver una vez "ok", o verlo varias veces. Lo mismo si e1 retira 100 dólares de su cuenta. Un caso ejemplar de estas ideas es el lenguaje de programación Haskell. Haskell es un lenguaje funcional puro: todas las expresiones en Haskell son puras. Haskell no incluye ninguna forma nativa de hacer asignaciones, por ejemplo. Como todo lenguaje práctico tiene que permitir de alguna manera tener algún efecto sobre el mundo real, los diseñadores de Haskell tuvieron que ingeniar un mecanismo para soportar efectos dentro de este marco puro. Resulta que la respuesta vino del lado de las mónadas, estructuras componibles que representan computación. Sin entrar en detalles, en Haskell una función de tipo Int → Int es una función pura que, dado un entero, retorna un entero. Y nada más; el compilador puede hacer todas las optimizaciones que quiera cuando ve aplicaciones de dicha función. En cambio, si la función hace uso de entradas y salidas como imprimir en pantalla, esto se ve reflejado en su tipo, que pasa a ser Int → IO Int, donde IO es la mónada de los efectos de entradas y salidas. Existen mónadas para excepciones, continuaciones, estado compartido, no-determinismo, etc. Y obviamente un programador puede definir sus propios efectos, por ejemplo si quiere razonar sobre el flujo de valores en el programa, lo cual tiene aplicaciones en seguridad. Esta disciplina, por más estricta que sea, fomenta un estilo de programación donde se separa el manejo de efectos de las partes más computacionales de un sistema, lo que mejora su modularidad al mismo tiempo que permite más razonamiento estático, incluyendo más optimizaciones. |
| |
| -------- | -------- |
| **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. |
