Une approche de la détection statique d'exceptions non rattrapées en appel par nom
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
Initially, exceptions have been introduced in call-by-value languages. For call-by-name evaluation, the usual solution is to encode them with a monadic construction. While theoretically elegant, this solution has several practical drawbacks: non-automatic propagation, the use of exceptions forces call-by-value evaluation and modularity is somewhat compromised. In this thesis, we make the choice of a primitive mechanism of exceptions which does not have the drawbacks of an encoding. We propose a type System where the types of a term give an account on which exceptions the term mentions. To that end, we introduce two type constructions. The first one, the union, characterises terms that may evaluate to an exception and is crucial to type the capture of exceptions. The second one, the corruption, gives an account on a phenomenon specific to call-by-name evaluation: an exception can be "buried" in a term by β-reduction without having the resulting term necessarily evaluating to the exception. Based on a subtyping relation, corruption provides a typing of exceptions which is both modular and favors code re-usability. The first chapters study these type constructions in the setting of the simply typed A-calculus. Afterwards we propose a few natural extensions of the obtained calculus. Lastly, we ex tend this calculus to second-order types. Moreover, we propose realizability models for each of the calculi, providing a precise semantics to the main original notion of this work, corruption.
Abstract FR:
Les exceptions ont d'abord été introduites dans les langages en appel par valeur. Pour les langages en appel par nom, la solution habituelle consiste à les encoder à l'aide d'une construction monadique. Bien qu'élégante théoriquement, cette solution présente plusieurs désavantages pratiques: propagation non automatique, l'utilisation des exceptions force l'appel par valeur et la modularité est en partie compromise. Dans cette thèse, nous faisons le choix d'un mécanisme d'exceptions primitif ne possédant pas les désavantages d'un encodage. Nous en proposons un système de type où les types d'un terme rendent compte des exceptions qu'il mentionne. À cette fin, nous introduisons deux constructions de types. La première, l'union, caractérise les termes pouvant s'évaluer sur une exception et est cruciale pour typer la capture d'exception. La seconde, la corruption, rend compte d'un phénomène propre à l'appel par nom: une exception peut se voir "enfouie" dans un terme par β-réduction, sans que le terme résultant ne s'évalue nécessairement sur l'exception en question. Reposant sur une relation de sous-typage, la corruption offre un typage des exceptions à la fois modulaire et favorisant la réutilisation de code. Les premiers chapitres étudient ces constructions de types dans le cadre du lambda-calcul simplement typé. Nous proposons ensuite quelques extensions naturelles du calcul obtenu. Enfin, nous étendons ce calcul aux types du second-ordre. De plus, nous proposons pour chacun des calculs des modèles de réalisabilité, offrant ainsi une sémantique précise à la principale notion originale de ces travaux, la corruption.