Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revisionBoth sides next revision
people:etanter:tipos [2013/05/17 21:47] – etanterpeople:etanter:tipos [2013/05/17 21:49] – etanter
Line 26: Line 26:
 **¡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 (Figura 1c). 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.