Existe-t-il des systèmes de type (statique) qui tentent de formaliser les caractéristiques de performance des programmes? Je ne trouve pas semble trouver de telles tentatives.
Étant donné que les systèmes de types sont (l'un des) les outils les plus puissants de l'arsenal du programmeur pour faire des déclarations sur les programmes et qu'il existe de nombreux cas dans lesquels les performances sont critiques, il ne semble pas exagéré d'imaginer que des tentatives ont été entreprises pour créer un système de type qui tente de faire au moins quelques déclarations sur les caractéristiques de stockage et d'exécution des programmes.
language-design
Klaas van Schelven
la source
la source
if condition then expensive_operation else cheap_operation?if (likely(operation_went_fine)) { // Do something } else if (unlikely(error_occured)) { // Do something else }Réponses:
Vous pourriez imaginer un système de type suffisamment sophistiqué pour être lié à WCET ou à la complexité du programme. Ensuite, le problème est de créer un analyseur de type de son (ou vérificateur) - c'est-à-dire des règles de frappe - pour rendre cela possible, et l'implémenter suffisamment efficacement pour le rendre raisonnablement utile.
La plupart des systèmes de type sont assez simples pour être rapides à calculer dans la pratique (au moins pour l'ensemble raisonnable de programmes qu'un développeur humain pourrait écrire manuellement).
Certains langages de programmation académique (par exemple AGDA ) ont des systèmes de type très sophistiqués qui sont complets de Turing, donc leur compilateur peut prendre une grande quantité (peut-être infinie) de temps.
(Si je comprends bien, le travail de doctorat en cours de Jérémie Salvucci au LIP6 à Paris est assez lié à votre question; je lui ai envoyé un mail à ce sujet; vous pourriez chercher des régions et des types ...).
Soyez cependant conscient du théorème de Rice et du problème de l' arrêt . Les systèmes de typage ne sont pas toujours la solution miracle que vous voudriez qu'ils soient (voir l'ancien livre « no silver bullet »).
la source
Il semble éminemment possible de créer un système de types qui catégorise la caractéristique de performance des types(par exemple, "rapide / lent pour l'accès série", "rapide / lent pour l'accès aléatoire", "efficace en mémoire / inefficace"). Ces traits peuvent être des types abstraits placés dans la hiérarchie de telle manière que les types les plus concrets en héritent. Cependant, les performances de tout programme utilisant ces types dépendraient de la façon dont ils sont réellement utilisés / accédés. Pour que le système de types fasse des déclarations sur le programme lui-même, l'utilisation de (l'accès à) ces types devrait elle-même être représentée comme des types . Cela impliquerait de renoncer à l'utilisation de structures de contrôle intégrées (par exemple des boucles for / while) et d'utiliser à la place des types qui les implémentent. -types d'accès et ainsi de suite.L'efficacité de l'utilisation pourrait alors s'exprimer au moins en partie par la combinaison et l'application de ces types les uns aux autres.
Dans un langage fonctionnel comme Haskell - qui n'a presque pas de structures de contrôle de toute façon - cela me semble assez pratique et exécutoire. En Java, cependant, un tel système semble beaucoup moins réalisable (non pas tant de la mise en œuvre que de l'applicabilité / fiabilité du résultat).
Haskell nous permet déjà de dire de façon définitive quelle partie d'un programme est pure et fournit des moyens de confiner des activités particulières dans des boîtes scellées. Étant donné que le parallélisme / la concurrence dans Haskell est implémenté via le système de type , on pourrait affirmer qu'il fait déjà partie du chemin (vers ce que vous voulez). En revanche, les langages impératifs (même ceux typés statiquement comme Java) offrent au codeur de nombreuses façons de renverser toute tentative.
la source