01/02/2001: Didier Remy (INRIA)
Une généralisation des exceptions et des opérateurs de contrôle.
Résumé
(Travail ancien, en collaboration avec Jon Riecke et Carl Gunter)
Les opérateurs de contrôle dérivés du "call/cc" du langage scheme ont eu un
grand succès à la fin des années 80 conduisant à un foisonnement de
nouvelles espèces. Son apparition dans le langage SML au début des années
90 a soulevé de sérieux problèmes de typage. En fait, le typage dérivé de la
translation par double négation n'est pas vraiment satisfaisant, car il
repose sur une vue fermée du monde, ne permet qu'un résultat de correction
faible, et oblige ainsi le toplevel à quelques acrobaties mystérieuses.
Dans c'est exposé je présenterai des travaux menés en 95 pour résoudre ce
problème de typage. Je montrerai comment nous avons été amenés à introduire
une nouvelle opération "cupto" (call up to) obligeant la capture de la
continuation à faire référence à un point précis du calcul (prompt)
introduit explicitement par le programmeur.
Nous donnerons des règles de typage pour cette construction qui permettent
un résultat de correction forte (préservation du typage au cours de la
réduction). Nous montrerons également que cette construction généralise la
plupart des constructions proposées jusqu'alors (1995) y compris le
mécanisme d'exception de ML. Nous verrons aussi sur des exemples concrets
que le cupto est un opérateur plus facile à manipuler que ses cousins et
parents. Mais l'usage des continuations dans la programmation reste délicat,
même avec le "cupto", et est finalement réservé à des applications très
spécifiques.