Commit 9e0ca4a8 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

revised introduction:

 - revised so that type schemes are in the appendix
 - added a list of contributions
 - stressed type inference
 - added enumitem.sty (latest version)
 - added a TODO.txt file with modification to do
parent 73e043ca
On ne modifie rien jusqu'à la section 2.5 (seulement quelques adaptations aux modifs suivantes)
DONE
On peut probablement déplacer les type schemes en appendice mais alors il faudrait terminer la section 2.5 par une sous-section discutant les différentes formes de complétude. En particulier il faut déplacer le A.30 dans le texte et le discuter, et discuter de la complétude avec les type schemes. Autrement dit il faut bien faire passer l'idée que l'incomplétude est seulement théorique, mais que en pratique nous utiliserions toujours des restrictions complètes.
Je déplacerais la règle [OverApp] de la section 4 à la section 3.2 (faut-il changer des preuves?). Et en section 4 je utiliserais la règle [AbsInf++] actuellement en appendice B, avec le texte qui vient avec.
Je laisserai la section sur les records, mais il faut souligner qu'il ne s'agit pas d'une extension triviale et ceci pour deux raisons: nous devons changer les expressions CDuce pour les adapter à l'occurrence typing et nous allons typer des enregistrements avec extension et deletion. Or que je sache seulement CDuce est capable de typer cela (vous en connaissez d'autres?). Et dans JavaScript il y a
delete object.property
Comment Flow gère cela? Et Typed Racket? Dans Racket il y a
record-remove rec kw
est-ce que quelqu'un a envie de voir comment ils le typent et comment, s'ils le typent, font l'occurence typing?
Il faut bien étendre la section sur les related work. En ajoutant un commentaire sur les références données par STH:
> Semantic Subtyping with an SMT Solver [Hritcu et al, 2010]
> features semantic set-theoretic types, type tests, type refinements,
> and more, although in a first-order context. Nested Refinements [Chugh
> et al, 2012] features set-theoretic types, type tests, type
> refinements, and application to an existing untyped language
> (JavaScript). Practical Optional Types for Clojure [Bonnaire-Sargeant
> et al, 2016] features set-theoretic type connectives, occurrence
> typing, and functional records.
Il faut aussi réécrire la comparaisons avec TypedRacket pour bien expliquer que les deux approches sont différents (type-theoretic vs control-flow) et que donc c'est normale que on fasse pas le même choses. On pourrait donner en appendice un flavor de analyse de flot pour montrer que ce que on fait pas on peut le faire en intégrant les idées des Typed Racket. Et peut être ajouter un pique sur le polymorphisme (comment on étend leur approche aux types polymorphes? Nous on donne une idée dans l'appendice).
Il faut probablement insister plus sur la contribution de l'inférence des types intersection.
Voilà
B.
This diff is collapsed.
......@@ -25,7 +25,7 @@ type \code{number\,|\,string} and they would fail, since the successor is
not defined for strings and the method \code{trim()} is not defined
for numbers. This is so because standard disciplines do not take into account the type
test performed on \code{x}. Occurrence typing is the typing technique
that uses the information provided by the test to specialize---precisely to \emph{refine}---the type
that uses the information provided by the test to specialize---precisely, to \emph{refine}---the type
of the occurences of \code{x} in the branches of the conditional: since the program tested that
\code{x} is of type \code{number}, then we can safely assume that
\code{x} is of type \code{number} in the ``then'' branch, and that it
......@@ -52,8 +52,11 @@ function \code{foo} has type
such details.} But it is clear that a more precise type would be
one that states that \code{foo} returns a number when it is applied to
a number and returns a string when it is applied to a string, so that the type deduced for, say, \code{foo(42)} would be \code{number} rather than \code{number|string}. This is
exactly what the intersection type \code{(number$\to$number) \&
(string$\to$string)} states (intuitively, an expression has an intersection of types, noted \code{\&}, if and only if it has all the types of the intersection) and corresponds in Flow to declaring \code{foo} as follows:
exactly what the \emph{intersection type}
\begin{equation}\label{eq:inter}
\code{(number$\to$number) \& (string$\to$string)}
\end{equation}
states (intuitively, an expression has an intersection of types, noted \code{\&}, if and only if it has all the types of the intersection) and corresponds in Flow to declaring \code{foo} as follows:
\begin{alltt}\color{darkblue}
var foo : \textcolor{darkred}{(number => number) & (string => string)} = x => \{
(typeof(x) === "number")? x++ : x.trim() \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foo2}
......@@ -91,7 +94,8 @@ occurrence typing approach will refine not only the types of variables
but also the types of generic expressions (bypassing usual type
inference). Second, the result of our analysis can be used to infer
intersection types for functions, even in the absence of precise type
annotations such as the one in the definition of \code{foo} in~\eqref{foo2}. Third, we
annotations such as the one in the definition of \code{foo} in~\eqref{foo2}: in practice, we are able to
infer the type~\eqref{eq:inter} for the unannotated pure JavaScript code of \code{foo}. Third, we
show how to combine occurrence typing with gradual typing, and in
particular how the former can be used to optimize the compilation of
the latter.
......@@ -135,8 +139,8 @@ $\Int\vee\String$ and from that it is not hard to deduce that~\eqref{two}
has type $\Int\vee\String$. Let us see this in detail. The expression in~\eqref{two} is
typed in the following type environment:
$x_1:(\Int\to\Int)\wedge(\String\to\String), x_2:\Int\vee\String$. All we
can deduce is then that the application $x_1x_2$ has type
$\Int\vee\String$ which is not enough to type either the ``then'' branch
can deduce, then, is that the application $x_1x_2$ has type
$\Int\vee\String$, which is not enough to type either the ``then'' branch
or the ``else'' branch. In order to type the ``then'' branch
$(x_1x_2)+x_2$ we must be able to deduce that both $x_1x_2$ and $x_2$
are of type \Int. Since we are in the ``then'' branch, then we know that
......@@ -165,12 +169,12 @@ $(\Int\vee\String)\wedge\String$ (i.e., again \String).
We have seen that we can specialize in both branches the type of the
whole expression $x_1x_2$, the type of the argument $x_2$,
but what about the type of $x_1$? Well, this depends on the type of
but what about the type of the function $x_1$? Well, this depends on the type of
$x_1$ itself. In particular, if instead of an intersection type $x_1$
is typed by a union type, then the test may give us information about
the type of the function in the various branches. So for instance if in the expression
in~\eqref{typical} $x_1$ is of type, say, $(s_1\to t)\vee(s_2\to\neg t)$, then we can
assume that $x_1$ has type $(s_1\to t)$ in the branch ``then'' and
assume for the expression~\eqref{typical} that $x_1$ has type $(s_1\to t)$ in the branch ``then'' and
$(s_2\to \neg t)$ in the branch ``else''.
As a more concrete example, if
$x_1:(\Int{\vee}\String\to\Int)\vee(\Bool{\vee}\String\to\Bool)$ and
......@@ -205,7 +209,7 @@ is of type $t$ or not, and suppose we know that the static types of
$e_1$ and $e_2$ are $t_1$ and $t_2$ respectively. If the application $e_1e_2$ is
well typed, then there is a lot of useful information that we can deduce from it:
first, that $t_1$ is a functional type (i.e., it denotes a set of
well-typed lambda-abstractions, the values of functional type) whose domain, denoted by $\dom{t_1}$, is a type denoting the set of all values that are accepted by any function in
well-typed $\lambda$-abstractions, the values of functional type) whose domain, denoted by $\dom{t_1}$, is a type denoting the set of all values that are accepted by any function in
$t_1$; second that $t_2$ must be a subtype of the domain of $t_1$;
third, we also know the type of the application, that is the type
that denotes all the values that may result from the application of a
......@@ -274,7 +278,7 @@ $t$. Therefore, we can exclude from $t_1$ all the functions that, when applied t
in $t_2^+$, yield a result not in $t$.
It can be obtained simply by removing from $t_1$ the functions in
$t_2^+\to \neg t$, that is, we refine the type of $e_1$ in the ``then'' branch as
$t_1^+=t_1\setminus (t_2^+\to\neg t))$.
$t_1^+=t_1\setminus (t_2^+\to\neg t)$.
Note that this also removes functions diverging on $t_2^+$ arguments.
In particular, the interpretation of a type $t\to s$ is the set of all functions that when applied to an argument of type $t$
either diverge or return a value in $s$. As such the interpretation of $t\to s$ contains
......@@ -350,10 +354,10 @@ will also be the type of the whole expression in \eqref{bistwo}. Now imagine
that the application $e(42)$ reduces to a Boolean value, then the whole
expression in \eqref{bistwo} reduces to $e$; but this has type
$\Int\to t$ which, in general, is \emph{not} a subtype of $(\Int\to
t)\setminus(\Int\to\neg\Bool)$, and therefore type is not preserved by the reduction. To cope with this problem, in
Section~\ref{sec:language} we resort to \emph{type schemes} a
t)\setminus(\Int\to\neg\Bool)$, and therefore type is not preserved by the reduction. To cope with this problem, the proof
of type preservation (see Appendix~\ref{app:subject-reduction}) resorts to \emph{type schemes}, a
technique introduced by~\citet{Frisch2008} to type expressions by
sets of types, so that the expression in \eqref{bistwo} will have both the types at issue.
sets of types, so that the expression in \eqref{bistwo} will have both the types at issue.
The second corner case is a modification of the example above
where the positive branch is $e(42)$, e.g.,
......@@ -404,6 +408,7 @@ by retyping the expression without that assumption (see rule
\Rule{Env\Aa} in Section~\ref{sec:algorules}).
\subsubsection*{Outline} In Section~\ref{sec:language} we formalize the
ideas presented in this introduction: we define the types and
expressions of our system, their dynamic semantics and a type system that
......@@ -424,3 +429,33 @@ joint to the submission.
\else
available online.
\fi
\subsubsection*{Contributions} The main contributions of our work can be summarized as follows:
\begin{itemize}[left=0pt .. \parindent]
\item We provide a theoretical framwork to refine the type of
expressions occurring in type tests, thus removing the limitations
of current approaches which require both the tests and the refinement
to take place on variables.
\item We define a type-theoretic approach that is alternative to the
current flow-based approaches. As such it provides different
results and it can be thus profitably combined with flow-based techniques.
\item We use our analysis for defining a formal framework that
reconstructs intersection types for unannotated or
partially-annotated functions, something that, in our ken, no
system did so far.
\item We prove the soundness of our system. We define algorithms to
infer the types that we prove to be sound and show different completeness results
which in practice yield the completeness of any reasonble implementation.
\item We show how to extend to and combine occurrence typing with
gradual typing and apply our results to optimze the compilation of the
latter.
\item We show how it is possible to extend our framework to
exploit the richer information provided by polymorphic types.
\end{itemize}
......@@ -250,7 +250,7 @@
We say that an environment $\Gamma$ is ordinary iff its domain only contains variables.
\end{definition}
\subsubsection{Subject Reduction}
\subsubsection{Subject Reduction}\label{app:subject-reduction}
\begin{property}[$\valsemantic \_$ properties]
\begin{align*}
......
......@@ -16,7 +16,7 @@
\usepackage{mathpartir}
\usepackage{color}
\usepackage{listings}
\usepackage[shortlabels]{enumitem}
\definecolor{darkblue}{rgb}{0,0.2,0.4}
......
@article{PlotkinP13,
author = {Gordon D. Plotkin and
Matija Pretnar},
title = {Handling Algebraic Effects},
journal = {Logical Methods in Computer Science},
volume = {9},
number = {4},
year = {2013},
url = {https://doi.org/10.2168/LMCS-9(4:23)2013},
doi = {10.2168/LMCS-9(4:23)2013},
timestamp = {Tue, 14 May 2019 16:31:14 +0200},
biburl = {https://dblp.org/rec/journals/corr/PlotkinP13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{PlotkinP03,
author = {Gordon D. Plotkin and
John Power},
title = {Algebraic Operations and Generic Effects},
journal = {Applied Categorical Structures},
volume = {11},
number = {1},
pages = {69--94},
year = {2003},
url = {https://doi.org/10.1023/A:1023064908962},
doi = {10.1023/A:1023064908962},
timestamp = {Fri, 02 Nov 2018 09:31:44 +0100},
biburl = {https://dblp.org/rec/journals/acs/PlotkinP03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{THF10,
author = {Tobin-Hochstadt, Sam and Felleisen, Matthias},
title = {Logical types for untyped languages},
booktitle = {Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
series = {{ICFP} '10},
year = {2010},
isbn = {978-1-60558-794-3},
location = {Baltimore, Maryland, {USA}},
pages = {117--128},
numpages = {12},
url = {http://doi.acm.org/10.1145/1863543.1863561},
doi = {10.1145/1863543.1863561},
acmid = {1863561},
publisher = {{ACM}},
address = {New York, NY, {USA}},
keywords = {logic, type systems, untyped languages},
}
@INPROCEEDINGS{BCF03,
AUTHOR = {V\'eronique Benzaken and Giuseppe Castagna and Alain Frisch},
TITLE = {{CD}uce: an {XML}-Centric General-Purpose Language},
BOOKTITLE = {ICFP~'03, 8th ACM International Conference on Functional Programming},
url = {http://doi.acm.org/10.1145/944746.944711},
PAGES ={51--63},
ADDRESS = {Uppsala, Sweden},
DMI-CATEGORY = {intc},
PUBLISHER = {ACM Press},
YEAR = {2003},
}
@Manual{typescript,
title = {{TypeScript}},
url = {https://www.typescriptlang.org/},
organization = {Microsoft},
year = {\mbox{\!}}
}
@Manual{Flow,
title = {{Flow}},
url = {https://flow.org/},
organization = {Facebook},
year = {\mbox{\!}}}
}
@inproceedings{THF08,
author = {Tobin-Hochstadt, Sam and Felleisen, Matthias},
title = {The Design and Implementation of Typed Scheme},
booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
series = {POPL '08},
year = {2008},
isbn = {978-1-59593-689-9},
location = {San Francisco, California, USA},
pages = {395--406},
numpages = {12},
url = {http://doi.acm.org/10.1145/1328438.1328486},
doi = {10.1145/1328438.1328486},
acmid = {1328486},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {scheme, type systems},
}
@article{Frisch2008,
author = {Frisch, Alain and Castagna, Giuseppe and Benzaken, V{\'e}ronique},
title = {Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types},
journal = {Journal of the {ACM}},
issue_date = {September 2008},
volume = {55},
number = {4},
month = sep,
year = {2008},
issn = {0004-5411},
pages = {19:1--19:64},
url = {http://doi.acm.org/10.1145/1391289.1391293},
publisher = {{ACM}},
}
\ No newline at end of file
\documentclass[DIV=11,10pt]{scrartcl}
\usepackage[cm]{fullpage}
\usepackage[utf8]{inputenc}
\usepackage{textcomp}
% \usepackage[utf8]{eurosym}
\usepackage[french]{babel}
\usepackage{hyperref}
\usepackage[T1]{fontenc}
% \usepackage{lmodern}
\usepackage{microtype}
\usepackage{xcolor}
\usepackage{paralist}
\usepackage{alltt}
\usepackage{amsmath,amssymb}
\usepackage{cleveref}
% \usepackage{fourier}
\usepackage{tgadventor}
\usepackage{xspace}
\usepackage{bm}
% \addtokomafont{disposition}{\rmfamily}
\addtokomafont{descriptionlabel}{\rmfamily}
% Please use \hhnote etc... for comments, feel free to tweak to your
% liking.
\usepackage[draft]{fixme}
% Uncomment to remove notes
% \usepackage[final]{fixme}
\fxsetup{layout=inline,theme=color,mode=multiuser}
\FXRegisterAuthor{eg}{aneg}{\color{blue}EG}
\FXRegisterAuthor{gc}{angc}{\color{blue}GC}
\FXRegisterAuthor{hh}{anhh}{\color{blue}HH}
\FXRegisterAuthor{tz}{antz}{\color{blue}TZ}
\DeclareMathSymbol{\qm}{\mathalpha}{operators}{"3F}
\DeclareMathAlphabet{\mathbbm}{U}{bbold}{m}{n}
\newcommand{\dyn}{\ensuremath{\mathbbm%
{\qm}}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\unk}{\texttt{?}}
\title{Intégration d'outils de programmation avancés dans un langage avec types ensemblistes}
\subtitle{Sujet de thèse} % \\ {\small\emph{DRAFT, please do not distribute}}}
\author{Encadrement: Giuseppe Castagna, Kim Nguyen
%\\
%Candidat: Mickaël Laurent
}
\date{\today}
\begin{document}
\maketitle
% Après pour parler science, on souhaitait te faire travailler sur une
% théorie et mise unifiée d'un langage de programmation moderne,
% statiquement typé avec le sous-typage sémantique au cœur du système.
% Le constat est que même si la méta-théorie de semsub + X est écrite
% et marche (où X \in { polymorphisme, gradual, occurrence typing }),
% mettre le tout dans un langage sans que ça casse, avec une
% méta-théorie unique pose de gros challenge, de formalisation et
% d'implémentation (est-ce que ça peut être fait de manière « modulaire
% » ?)
% Certains points sont encore balbutiant : occurence typing (manque
% l'analyse de flot de contrôle), gestion des effets dans un tel langage
% (grosse inconnue), inférence de type, notion de type principale (au
% moins pour un fragment du langage) sont des axes de recherche
% complètement nouveau.
% Pour les aspects de transfert ou d'impact dans l'industrie, il y a une
% application directe de ce travail pour l'inférence de type de code
% Javascript pour pouvoir l'utiliser dans la base de données Oracle. Je
% viens de recevoir un grant d'Oracle pour étudier ces aspects, et ton
% travail poserait les fondements théoriques pour développer de tels
% outils.
% Voilà, on te tient au courant, avec la propal détaillée et les infos
% de comment on se réparti l'encadrement. Essaye d'avoir la date exacte
% de la deadline pour qu'on ne la rate pas :-)
\section{Description du sujet}
Cette thèse s'inscrit dans la thématique des langages de programmation
et en particulier dans celle des langages de programmation
statiquement typés. Dans des tels langages, des règles de typage
permettent de garantir l'absence de certaines classes d'erreurs à
l'exécution.
Un exemple simple de règle de typage est celle qui
demande que l'opérateur de soustraction ne soit \emph{bien typé} que
sur des arguments numériques. Elle permet ainsi de détecter des
erreurs du programmeur qui essayerait de soustraire un tableau et une
chaîne de caractères (code qui n'aurait aucun sens). Les \emph{types}
sont des objets associés aux expressions et aux valeurs du langage et ils en décrivent
le domaine. Par exemple le type \texttt{Int} associé au constantes
\texttt{1}, \texttt{2}, \ldots{} indique que de telles valeurs sont des
entiers.
Le contexte de la thèse est plus précisément celui des langages de
programmation munis d'un système de types \emph{ensemblistes}. Dans un
tel système, les types ne sont pas simplement des objets syntaxiques
utilisés pour l'analyse (le typage) mais des ensembles de valeurs (au
sens mathématique). Cette définition \emph{sémantique} des types comme
des ensembles induit une algèbre de types très riche, comprenant par
exemple les opérateurs ensemblistes d'union, d'intersection ou de
complémentation, traditionnellement absents des langages de
programmation généralistes.
Une première étape dans la théorie et conception des langages de
programmation à types ensemblistes a été la définition et
l'implantation du langage CDuce \cite{BCF03}. Ce dernier est un
langage fonctionnel statiquement typé, muni de types ensemblistes et
de polymorphisme.
Le but de cette thèse est d'arriver à définir et étudier un langage de
programmation fonctionnel statiquement typé qui combine les
caractéristiques de programmation avancée suivantes:
\begin{enumerate}
\item typage d'occurrences
\item types ensemblistes (types union, intersection et négation)
\item typage graduel et inférence de types
\item polymorphisme paramétrique
\item types récursifs
\item effets et ordre supérieur
\item raffinement de types
\end{enumerate}
Nous allons montrer par des exemples l'intérêt de chaque caractéristique:
\paragraph{Typage d'occurrences:}
Le typage d'occurrences, ou \emph{occurrence typing}, est une technique
qui utilise les tests effectués par un programme afin de pouvoir raffiner
l'analyse de types dans le code à exécuter en prenant en compte la réussite ou
l'échec du test. Un exemple d'application du typage d'occurrences est donné par le
code JavaScript suivant
\begin{alltt}
function foo(x) \{
(typeof(x) === "number")? x++ : x.trim()
\}
\end{alltt}
Dans ce code on teste si l'argument de la fonction
\code{foo} lié à \code{x} est de type
\code{number}; si oui on renvoie le successeur de l'argument et si non
on envoie à l'argument le message \code{trim()}. Puisque \code{trim} est une
méthode définie seulement pour les valeurs de type \code{string}
(il s'agit d'une méthode du standard ECMAScript 5 qui élimine les espaces
au début et à la fin d'une chaîne de caractères) on peut facilement
déduire que l'argument de \code{foo} doit être de type \code{number} ou
\code{string}. C'est à dire qu'il doit avoir le type ``union''
\code{number|string}. Dans les
systèmes de types standards cette information n'est pas suffisante pour
pouvoir typer la fonction \code{foo} car
\code{trim()} n'est pas défini pour \code{number} (et donc pas pour un argument de type \code{number|string}) et \code{++} n'est
pas définie pour \code{string}. Ceci parce que les systèmes de types
standards ne prennent pas en compte le test de type effectué sur
\code{x}. Le typage d'occurrence est la technique qui utilise cette
information pour spécialiser le type des occurrences de \code{x}
de manière différente dans chaque branche du test: puisque le programme a testé que
\code{x} est de type \code{number}, alors nous pouvons supposer que
\code{x} est de type \code{number} dans la branche ``then'' du test, et
qu'il \emph{n'est pas} de type \code{number} dans la branche ``else''
(et de cela et du fait qu'il doit être ou \code{number} ou \code{string}, déduire
que \code{x} est de type \code{string} dans cette dernière branche).
Initialement défini pour le langage Scheme pour pouvoir typer des programmes
Scheme non typés~\cite{THF08,THF10}, le typage d'occurrence est de plus en plus étudié, développé
et utilisé dans l'industrie (en témoignent les langages Hack et Flow
développés par Facebook et Typescript développé par Microsoft) car il est
indispensable pour pourvoir analyser du code typiquement écrit dans
ces langages de programmation en langages dynamiques.
\paragraph{Types ensemblistes:}
comme nous venons de le voir, les types ensemblistes sont intimement liés
à \emph{l'occurrence typing}. Le type que l'on déduira pour la fonction
\code{foo} sera \code{number|string $\to$ number|string}: une fonction
qui associe à une valeur de type union un résultat du même type
union. Nous avons aussi déjà vu
l'utilisation du type négation: quand nous avons dit que dans la
branche ``else'' l'occurrence de \code{x} n'est pas de type
\code{number} cela signifie qu'elle est de type
\code{$\neg$number}. Et puisque \code{x} doit aussi avoir le type
\code{number|string} on déduit que cette occurrence aura
\emph{l'intersection} de deux types, c'est-à-dire
\code{(number|string)\&$\neg$number} =
\code{(number|string)$\setminus$number} = \code{string}. Mais on
pourrait aussi utiliser un type intersection pour donner un type bien
plus précis à \code{foo} tel
\code{(number$\to$number)\&(string$\to$string)} qui capture le fait
que \code{foo} appliquée à un entier renvoie un entier et qu'appliquée
à une chaîne de caractères renvoie une chaîne de caractères. On parle
dans ce cas de polymorphisme ``ad hoc'', car
il permet de typer des fonctions surchargées (en anglais
\emph{overloaded functions}) qui exécutent du code différent sur des
arguments de types différents.
\paragraph{Typage graduel et inférence de types:}
nous avons déjà vu qu'une certaine dose d'inférence de types est
nécessaire: la fonction \code{foo} n'a pas d'annotation de type mais
on veut déduire qu'elle est de type \code{number|string $\to$
number|string} ou, ce qui est encore plus difficile à déduire, de
type \code{(number$\to$number)\&(string$\to$string)}. Si la première
déduction est déjà possible dans les systèmes actuels, la deuxième le sera surement grâce aux
techniques développés dans cette thèse. Toutefois un tel genre de déduction
n'est pas toujours possible, c'est pourquoi il faudra avoir la
possibilité de mélanger des zones du programme typées statiquement avec
d'autres zones typées dynamiquement C'est exactement le but du \emph{typage graduel}
qui permet d'annoter certaines parties du programme par un type inconnu
\dyn, qui signale au compilateur que le typage statique peut être
relâché, avec la contrainte d'ajouter un contrôle dynamique des types
(lors de l'exécution du programme). Par exemple la
fonction \code{foo} pourrait être définie comme:
\begin{alltt}
function foo(x:\dyn) \{
(typeof(x) === "number")? x++ : x.trim()
\}
\end{alltt}
elle serait donc typée par \code{\dyn$\to$(number|string)} et le
compilateur introduirait des tests dynamiques qui contrôleraient à
l’exécution que lors de l’exécution de \code{x++} la variable est liée
à un entier et que lors de l'exécution de \code{x.trim()} la variable
est liée à une chaine de caractères.
\paragraph{Polymorphisme paramétrique:} le polymorphisme paramétrique
est désormais un outil incontournable dans un langage de programmation
typé moderne pour pouvoir programmer de manière générique et modulaire. Cette
fonctionnalité se retrouve en effet sous le nom de \emph{generics}
dans le langage Java ou encore \emph{template} dans le langage \code{C++} et est l'une des caractéristiques distinctives des langages fonctionnels typés.
Un simple exemple de cette nécessité peut être obtenu en
modifiant légèrement le code de \code{foo} de façon à ce que la branche
``else'' renvoie l'argument inchangé:
\begin{alltt}
function foo(x) \{
(typeof(x) === "number")? x++ : x
\}
\end{alltt}
dans ce cas il est clair que, indépendamment du résultat du test de
type, \code{foo} renvoie toujours un résultat
qui a le même type que l'argument. Ceci est exprimé par le type
polymorphe $\forall\alpha.\alpha\to\alpha$ (même si ce type est
distinctif des langages de la famille \texttt{ML}, la présence du test de
type rend nécessaire
l'expressivité des types ensemblistes pour pouvoir le déduire pour
cette fonction). Mais il se peut que le
polymorphisme paramétrique doive se combiner avec les caractéristiques
précédentes. Si par exemple la branche ``then'' teste si l'argument est
égal à 42
\begin{alltt}
function foo(x) \{
(typeof(x) === "number")? (x==42) : x
\}
\end{alltt}
alors le type que on veut déduire pour cette fonction est:
$\forall\alpha.$\code{(number$\to$boolean)\&(($\alpha\setminus$number)$\to$($\alpha\setminus$number))}. Autrement
dit, si \code{foo} est appliqué à un entier alors il renvoie un
booléen, sinon s'il est applique à un type qui n'est pas \code{number}
il renvoie un résultat du même type.
\paragraph{Types récursifs, effets et ordre supérieur:}
Les types récursifs, les
effets et les fonctions d'ordre supérieur sont, à l'instar du
polymorphisme paramétrique, des caractéristiques
importantes dans un langage de programmation moderne. Ici il ne s'agit
pas de trouver des nouvelles fonctionnalités mais d'étudier comment
intégrer ces caractéristiques avec celles énoncées ci dessus. En effet,
chacun des traits cités interagit de manière subtile avec le système
de type et la sémantique du langage. Par exemple, la presence d'effets force un
ordre d'évaluation et demande d'imposer certaines restrictions sur le
polymorphisme pour garantir la sûreté du typage. De plus, cette
interaction rend les techniques algorithmiques existantes caduques:
par exemple, en présence de types ensemblistes, les algorithmes
d'unification ne sont plus suffisants pour l'inférence de types
polymorphes.
\paragraph{Raffinement de types:}
nous avons déjà montré deux exemples de raffinement de types: le typage
d'occurrences permet de raffiner le type des occurrences d'une
expression de manière différente dans les branches d'un test; une
meilleure inférence des types permettrait de raffiner le type
\code{number|string $\to$ number|string} de \code{foo} dans le type
\code{(number$\to$number)\&(string$\to$string)} qui est bien plus
précis. On voudrait ajouter la possibilité de raffiner les types du
langage par le biais de propositions logiques. Par exemple, on voudrait
définir le type des nombres impairs comme il suit: $\texttt{Odd} = \{
x\in\texttt{Int}~|~x\mod 2 = 1\}$. \texttt{Odd} serait un raffinement du
type \texttt{Int}. Il existe déjà une littérature abondante sur ce
sujet. La spécificité dans cette thèse serait d'utiliser ces types en
combinaison avec les types ensemblistes pour généraliser le typage
d'occurrence: si nous avons un test sur une expression booléenne $e$
et si $x$ est une variable libre dans $e$ de type $t$, alors on pourrait
raffiner son type par $\{x\in t~|~e\}$ dans la branche ``then'' et
$\{x\in t~|~\neg e\}$ dans la branche ``else''.
\section{Objectifs}
La plupart de ces sujets ont été étudiés séparément et pour certains
ont été étudiés en combinaison. Mais l’intégration de toutes ses
caractéristiques dans un langage unique pose de nouveaux
défis qui demandent non seulement des avancées sur chacun d'eux
mais aussi le développement de nouvelles techniques qui en
permettent la combinaison. L'inférence de types intersection pour les
fonctions nécessitera une analyse fine que sera fournie par le
typage d'occurrence et une analyse de contrôle de flot que l'on
tachera d'intégrer avec cette dernière. Cette analyse pourra aussi
être utilisée pour l'intégration des effets. Pour ces derniers nous
envisageons d'utiliser les travaux sur les effets algébriques en les