Comments on Typage en informatique

Damien (2005-01-10T18:26:22Z)

Sinon, Pierce prévoit une suite à son livre pour février 2005 : Advanced Topics in Types and Programming Languages.

Damien (2005-01-09T13:42:06Z)

Autre livre que j'aime bien sur les thème des langages, et qui a un bon équilibre théorie/pratique est Programming Language Design Concepts, de Watt.

koxinga (2005-01-05T18:04:00Z)

"Pour ce qui est du contrôle des ressources, c'est quelque chose qui me semble manquer complètement dans les langages qui existent : par exemple, si je ne peux pas dire « récupérer un bout de code sur le réseau et l'exécuter dans une sandbox à usage mémoire et CPU limités »"

Pour moi, ce n'est pas le rôle du langage, mais plutôt celui de l'OS. Le Hurd par exemple permet de faire des choses comme cela : "It offers the possibility of implementing sandboxes, where you can run a program but have another program monitoring all its I/O to make sure it doesn't start writing in files it wasn't expected to." (<URL:http://kerneltrap.org/node/4484 >)

sinon, merci pour les explications (ca me plait de plus en plus tout ca

nycboy (2005-01-05T16:39:12Z)

Il existe des systèmes avec contrôle de ressources, mais ce n'est pas géré au niveau des langages mais de l'OS… Comme l'unix AIX par exemple: la mémoire que peut demander un process (par allocations dynamiques) est limitée au total.

phi (2005-01-05T14:03:26Z)

Boris:
On emploie souvent "linéaire" pour dire "affine"… cependant, ici, ça revient au même car °C et °K sont équivalents pour les dimnesions, comme d'ailleurs m et km. Là on est encore dans l'arithmétique qui a des chances d'être décidable. Distinguer °C et °K au niveau du typage serait pire que distinguer nombres positifs et négatifs, et je ne vois pas à quoi cela pourrait servir.

Je ne connaissais pas dependentML! où trouve-t-on les références?

Ruxor:
En C, tous les objets sont potentiellement de 1ere classe…
C'est quand même pratique, l'inférence de type… Pour moi, le plus important est que le compilateur se contente de proposer un type et n'impose pas de restrictions absurdes (genre Pascal UCSD).
Il y a quand même une faiblesse avec le typage dynamique: certaines erreurs donnent des types seulement arbitrairement complexes (genre liste de liste de…) alors qu'un typage statique détecte immédiatement le type à boucle infinie.

Ruxor (2005-01-05T09:40:13Z)

koxinga → J'ai un livre qui n'est pas mal du tout sur les interpréteurs de langages de programmation (comment en écrire, et comment en changeant un peu l'interpréteur on change la sémantique du langage, ce genre de choses), qui explique ce genre de notions ; malheureusement, je ne me rappelle plus le titre ni l'auteur, et le livre lui-même est resté chez mes parents. La citoyenneté de première classe d'un concept, c'est le fait que le langage le permette de le manipuler comme les objets les plus manipulables (typiquement, les nombres) : par exemple, un langage de programmation est fonctionnel quand les fonctions (ou, en fait, mieux : les clôtures) ont la citoyenneté de première classe, tu peux stocker une fonction dans une variable, passer une fonction en argument à une autre, ce genre de choses. ML, par exemple, est un langage fonctionnel parce que les foncitons ont cette citoyenneté de première classe ; en revanche, les types ne l'ont pas, on ne peut pas stocker un type dans une variable ni le passer en argument à une fonction (alors qu'en Java, dans une certaine mesure, on peut) ; en Scheme, les continuations (qui représentent quelque chose comme la pile d'appel à un moment de l'exécution du programme) ont citoyenneté de première classe, etc. Ensuite, pour hâtif/paresseux, un langage paresseux (comme Haskell) c'est un langage qui ne va faire les évaluations qu'au moment où elles sont absolument nécessaires, alors qu'un langage hâtif (comme ML) va les faire dès qu'elles sont rencontrées. Notamment, dans un langage paresseux, si tu écris f(1/0) et que la fonction f n'utilise pas son argument, il n'y aura pas d'erreur, parce que 1/0 ne sera pas évalué. Le comportement paresseux est parfois très utile et permet de programmer de façon très agréable, mais il est malheureusement d'un coût de performance monstrueux (les programmes en Haskell même compilé tournent à une lenteur totalement déraisonnable, alors que Caml est un langage de fait très rapide), aussi bien en espace qu'en temps d'ailleurs. Avoir la possibilité de faire du paresseux si on le veut, c'est très utile, mais quand c'est aussi envahissant qu'en Haskell ça en devient plutôt gênant.

Boris → J'avais cette idée sur le typage statique versus dynamique bien avant de lire ce livre, hein : il ne m'a juste pas fait changer d'avis. Globalement, ce que je trouve dommage, c'est quand on bride la richesse sémantique (par exemple Caml qui a un typage sérieusement limité — même s'il part dans tous les sens) au nom de certaines considérations d'implémentation (comme le fait de pouvoir automatiser l'inférence de types) : je préfère largement un langage qui a un système de types très riches mais où il faut que le programmeur annote tout explicitement parce que l'inférence est indécidable, qu'un langage où on a bridé le système de types pour rendre l'inférence possible (mais évidemment, dans le système plus riche, si certains sous-systèmes bien définis sont décidables, autant que dans ce cas-là la construction automatique soit faite) ; et un raisonnement assez semblable se fait pour le statique versus sémantique : limiter le système de types à ce qu'on peut faire en statique, c'est une contrainte beaucoup trop forte. De toute façon, globalement, la notion même de compilation ne m'intéresse pas, pour moi (dans l'optique d'imaginer la sémantique d'un langage idéal, je veux dire, hein !) un compilateur est une optimisation sans intérêt théorique par rapport à un interpréteur (et sur un interpréteur, la notion de statique vs. dynamique, elle disparaît assez). Pour ce qui est du contrôle des ressources, c'est quelque chose qui me semble manquer complètement dans les langages qui existent : par exemple, si je ne peux pas dire « récupérer un bout de code sur le réseau et l'exécuter dans une sandbox à usage mémoire et CPU limités », il me semble qu'il manque vraiment quelque chose ; actuellement, à cause de ça, on n'a aucun système qui permette d'exécuter du code non-sûr en se prémunissant à la fois contre les attaques directes que contre les DoS.

phi → Pour moi, c'est au programmeur de résoudre l'équation linéaire. L'interpréteur ou compilateur, il se contente de vérifier que les annotations de type qui ont été données sont bonnes.

Boris (2005-01-05T08:59:27Z)

phi> Pourquoi seulement linéaires, et pas affines (conversion °C -> °F par exemple) ? Certains compilateurs résolvent déjà des problèmes difficiles pendant le typage : dans DependentML, la longueur des tableaux est connue, et l'inférence de types nécessite de résoudre des systèmes d'équations dans l'arithmétique de Pressburger (un problème qui est décidable).

Quant à l'interprétation abstraite, des sources bien informées disent que Cousot a continué a travaillé dessus, et <propagande> que tout n'est que conséquence/instance/whatever d'un problème d'interprétation abstraite </propagande>.

Muriel (2005-01-04T22:55:45Z)

Ce serait bien de développer la phrase de conclusion, ça donne envie, les gens comme moi se disent : "tiens, je comprends cette phrase, s'il pouvait la développer en un paragraphe qu'en plus je comprenne, quel régal !"

phi (2005-01-04T19:15:51Z)

Pour avoir des "preuves", ou du moins des tests de cohérence généralisés, il faudrait d'abord spécifier toutes les opérations primitives dans le système additionnel. Par exemple, si on introduit les unités de mesure (en les codant par leurs exposants dimensionnels), il faut indiquer que l'addition de longueurs donne une longueur et leur produit une aire, que l'exponentiation est invalide.
Tant que les preuves relèvent de l'unification bête, c'est facile. Avec les unités de mesure, déjà, la synthèse de type conduirait à résoudre des systèmes d'équations linéaires.
P. Cousot avait étudié ce qu'il appelait "interprétation abstraite" vers 1975; je ne sais pas ce que c'est devenu.

Boris (2005-01-04T19:06:09Z)

Conclusion très réaliste ! (quoi c'était du second degré ?).

Il est amusant qu'après avoir lu le TAPL tu arrives à des phrases comme "pour moi, le typage statique ne doit être qu'une optimisation sur le typage dynamique" (je pense que Benjamin Pierce serait quelque peu choqué). Ça ma paraît d'autant plus compromis que la quantité d'information à vérifier qu'il faudrait conserver à l'exécution (dans un langage dans lequel tout serait de premier ordre) serait très importante (et coûteux en temps).

Par ailleurs, des problématiques très courantes en recherche (compilation séparée, migration de code, confidentialité…) n'apparaissent pas dans tes objectifs. En revanche, pourquoi un contrôle aussi fin des ressources te semble-t-il important ?

En tout cas, avec le (peu de) recul que j'ai sur les progrès du domaine pendant les 30 dernières années, je te donne rendez-vous en 2040. Peut-être verra-t-on alors des langages qui commenceront à correspondre à ce que tu envisages…

koxinga (2005-01-04T18:30:31Z)

sans vouloir paraitre lourd, as-tu une idée d'un site me permettrant de comprendre ce que tu as écris ? parce que là, pour le non-initié, la majorité des caractéristiques de ton langage idéal sont difficiles à comprendre. J'ai deux ou trois bases, mais des expressions comme "citoyenneté de première classe" ou "hâtif par défaut mais optionnellement localement paresseux" sont assez absconses.

(ou même un livre s'il est vraiment bien)