¿Existen sistemas de tipo (estático) que intenten formalizar las características de rendimiento de los programas? Parece que no puedo encontrar tales intentos.
Dado que los sistemas tipográficos son (una de) las herramientas más poderosas en el arsenal del programador para hacer declaraciones sobre programas, y dado que hay muchos casos en los que el rendimiento es crítico, no parecería descabellado imaginar que se hubieran realizado intentos para cree un sistema de tipos que intente hacer al menos algunas declaraciones sobre las características de almacenamiento y tiempo de ejecución de los programas.
language-design
Klaas van Schelven
fuente
fuente
if condition then expensive_operation else cheap_operation?if (likely(operation_went_fine)) { // Do something } else if (unlikely(error_occured)) { // Do something else }Respuestas:
Podría imaginar un sistema de tipos lo suficientemente sofisticado como para estar relacionado con WCET o la complejidad del programa. Entonces, el problema es hacer un analizador de tipo de sonido (o un verificador), es decir, reglas de tipeo, para que eso sea posible e implementarlo lo suficientemente eficiente como para que sea razonablemente útil.
La mayoría de los sistemas tipo son lo suficientemente simples como para ser rápidos de calcular en la práctica (al menos para el conjunto razonable de programas que un desarrollador humano podría escribir manualmente).
Algunos lenguajes de programación académica (por ejemplo, AGDA ) tienen sistemas de tipos muy sofisticados que son completos de Turing, por lo que su compilador puede llevar una gran cantidad de tiempo (quizás infinito).
(Si entiendo bien, el trabajo de doctorado de Jérémie Salvucci en curso en LIP6 en París está bastante relacionado con su pregunta; le he enviado un correo electrónico al respecto; puede buscar regiones y tipos ...).
Sin embargo, tenga en cuenta el teorema de Rice y el problema de detención . Es posible que los sistemas de tipos no siempre sean la bala de plata que desea que sean (consulte el antiguo libro sin bala de plata ).
fuente
Parece eminentemente posible crear un sistema de tipos que clasifique la característica de rendimiento de los tipos(por ejemplo, "rápido / lento para acceso en serie," rápido / lento para acceso aleatorio "," memoria eficiente / ineficiente "). Esos rasgos podrían ser tipos abstractos colocados en la jerarquía de tal manera que los tipos más concretos heredaran de ellos. Sin embargo, el rendimiento de cualquier programa que use esos tipos dependerá de la forma en que realmente se usen / accedan. Para que el sistema de tipos haga declaraciones sobre el programa en sí, el uso de (acceso a) esos tipos debería representarse como tipos Esto significaría renunciar al uso de estructuras de control integradas (por ejemplo, bucles for / while) y, en su lugar, usar tipos que las implementen. Por lo tanto, la jerarquía podría tener un tipo de acceso en serie abstracto y un acceso en serie descendente, en serie en árbol -tipos de acceso, etc.La eficiencia del uso podría expresarse, al menos en parte, mediante la combinación y aplicación de estos tipos entre sí.
En un lenguaje funcional como Haskell, que casi no tiene estructuras de control de todos modos, esto me parece bastante práctico y exigible. En Java, sin embargo, un sistema de ese tipo parece mucho menos alcanzable (no por lo tanto de la aplicación como de la aplicabilidad / fiabilidad del resultado).
Haskell ya nos permite establecer definitivamente cuánto de un programa es puro y proporciona formas de limitar actividades particulares dentro de cajas selladas. Dado que el paralelismo / concurrencia en Haskell se implementa a través del sistema de tipos , se podría argumentar que ya es parte del camino (a lo que desea). Por el contrario, los lenguajes imperativos (incluso los de tipo estático como Java) ofrecen al codificador muchas, muchas formas de subvertir cualquier intento de hacerlo.
fuente