Acontrolled approach of exception handling in functional programming
Une approche contrôlée du traitement d'exceptions en programmation fonctionnelle
Résumé
By analysing the way ML exceptions can escape their scope of declaration, Philippe de Groote proposed in TLCA'95 a simply typed lambda-calculus of "static" exception handling ensuring that a well typed term cannot lead to a uncaught exception. The underlying idea was to keep the handlers active during the entire execution of the program. We propose a study of this concept in a realistic programming context authorizing general recursion by means of a fixed-point operator. The resulting calculus is described using three semantical forms: reduction rules, operational semantics and CPS semantics. We establish that these three interpretations are equivalent for a particular class of terms (the programs), thus showing that static exception handling can sometimes be considered as an acceptable alternative to classical, "dynamic" exception handling.
A partir de l'analyse du processus par lequel des exceptions en ML peuvent échapper à leur champ de déclaration, Philippe de Groote a proposé lors de TLCA'95 un lambda-calcul simplement typé de traitement d'exceptions statique assurant qu'un terme correctement typé ne pouvait donner lieu à une exception non capturée. Le principe permettant d'aboutir à un tel résultat consiste à garantir que chaque gestionnaire d'exception reste accessible pendant toute la durée d'exécution du programme. Nous nous proposons d'étudier ce concept dans un cadre de programmation réaliste autorisant la récursion générale par l'ajout au calcul d'un opérateur de point fixe.Le calcul ainsi obtenu est présenté sous trois formes sémantiques:respectivement un système de règles de réduction, une sémantique opérationnelle et un modèle dénotationnel basé sur la notion de transformation par continuations. En établissant que ces trois interprétations sont équivalentes sur une classe particulière de termes (les programmes), nous montrons en quoi l'approche statique du traitement d'exceptions peut être considérée dans certains cas comme une alternative raisonnable au traitement classique.