Commit 15c99916 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Typos + rewording in some places.

parent 80c23046
...@@ -50,8 +50,10 @@ ...@@ -50,8 +50,10 @@
\title{Intégration d'outils de programmation avancés dans un lagage avec types ensemblistes} \title{Intégration d'outils de programmation avancés dans un lagage avec types ensemblistes}
\subtitle{Sujet de thèse} % \\ {\small\emph{DRAFT, please do not distribute}}} \subtitle{Sujet de thèse} % \\ {\small\emph{DRAFT, please do not distribute}}}
\author{Proposants: Giuseppe Castagna, Kim Nguyen\\ \author{Encadrement: Giuseppe Castagna, Kim Nguyen
Candidat: Mickaël Laurent} %\\
%Candidat: Mickaël Laurent
}
\date{\today} \date{\today}
\begin{document} \begin{document}
...@@ -95,61 +97,54 @@ l'exécution. ...@@ -95,61 +97,54 @@ l'exécution.
Un exemple simple de règle de typage est celle qui Un exemple simple de règle de typage est celle qui
demande que l'opérateur de soustraction ne soit \emph{bien typé} que 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 sur des arguments numériques. Elle permet ainsi de détecter des
erreurs du programmeur qui essayerais de soustraire un tableau et une 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} chaîne de caractères (code qui n'aurait aucun sens). Les \emph{types}
sont objets associés aux expressions et valeurs du langage décrivant sont objets associés aux expressions et valeurs du langage et qui décrivent
leur domaine. Par exemple le type \texttt{Int} associé au constantes leur domaine. Par exemple le type \texttt{Int} associé au constantes
\texttt{1}, \texttt{2}, \ldots indique que de telles valeurs sont des \texttt{1}, \texttt{2}, \ldots{} indique que de telles valeurs sont des
entiers. entiers.
Le contexte de la thèse est plus précisément celui des langages de Le contexte de la thèse est plus précisément celui des langages de
programmation muni d'un système de type \emph{ensembliste}. Dans un programmation munis d'un système de types \emph{ensemblistes}. Dans un
tel système, les types ne sont pas simplement des objets syntaxiques tel système, les types ne sont pas simplement des objets syntaxiques
utilisé pour l'analyse (le typage) mais des ensembles de valeurs (au utilisé pour l'analyse (le typage) mais des ensembles de valeurs (au
sens mathématique). Cette définition \emph{sémantique} des types comme 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 des ensembles induit une algèbre de types très riche, comprenant par
exemple les opérateurs ensembliste d'union, d'intersection ou de exemple les opérateurs ensemblistes d'union, d'intersection ou de
complémentation, traditionnellement absents des langages de complémentation, traditionnellement absents des langages de
programmation généralistes. programmation généralistes.
Une première étape dans la théorie et conception des langages de Une première étape dans la théorie et conception des langages de
programmation à types ensembliste a été la définition et programmation à types ensemblistes a été la définition et
l'implémentation du langage CDuce \cite{BCF03}. 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 programmation avancée suivantes: 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 programmation avancée suivantes:
\begin{enumerate} \begin{enumerate}
\item typage d'occurrence \item typage d'occurrences
\item types ensemblistes (types union, intersection et négation) \item types ensemblistes (types union, intersection et négation)
\item typage graduel et inférence de types \item typage graduel et inférence de types
\item polymorphisme paramétrique \item polymorphisme paramétrique
\item types récursifs \item types récursifs
\item effets et ordre supérieur \item effets et ordre supérieur
\item raffinement de types \item raffinement de types
\end{enumerate} \end{enumerate}
Nous allons montrer par des exemples l'intérêt de chaque caractéristique: Nous allons montrer par des exemples l'intérêt de chaque caractéristique:
\paragraph{Typage d'occurrence:} \paragraph{Typage d'occurrences:}
Le typage de occurrence, ou \emph{occurrence typing}, est une technique Le typage de occurrences, ou \emph{occurrence typing}, est une technique
qui utilise les tests effectués par un programme afin de pouvoir raffiner 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'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'occurrence est donné par le l'échec du test. Un exemple d'application du typage d'occurrences est donné par le
code JavaScript suivant code JavaScript suivant
\begin{alltt} \begin{alltt}
function foo(x) \{ function foo(x) \{
...@@ -157,12 +152,12 @@ code JavaScript suivant ...@@ -157,12 +152,12 @@ code JavaScript suivant
\} \}
\end{alltt} \end{alltt}
Dans ce code on teste si l'argument de la fonction Dans ce code on teste si l'argument de la fonction
\code{foo} liée à \code{x} est de type \code{foo} lié à \code{x} est de type
\code{number}; si oui on renvoie le successeur de l'argument et si non \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 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} méthode définie seulement pour les valeurs de type \code{string}
(il s'agit d'une méthode du standard ECMAScript 5 qui élimines les espaces (il s'agit d'une méthode du standard ECMAScript 5 qui élimines les espaces
au début et à la fin d'une chaine de caractères) on peut facilement 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 déduire que l'argument de \code{foo} doit être de type \code{number} ou
\code{string}. C'est à dire il doit avoir le type ``union'' \code{string}. C'est à dire il doit avoir le type ``union''
\code{number|string}. Dans les \code{number|string}. Dans les
...@@ -172,7 +167,7 @@ pouvoir typer la fonction \code{foo} car ...@@ -172,7 +167,7 @@ pouvoir typer la fonction \code{foo} car
pas définie pour \code{string}. Ceci parce que les systèmes de types 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 standards ne prennent pas en compte le test de type effectué sur
\code{x}. Le typage d'occurrence est la technique qui utilise cette \code{x}. Le typage d'occurrence est la technique qui utilise cette
information pour spécialiser le type des occurrences de \code{x} 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 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}, alors nous pouvons supposer que
\code{x} est de type \code{number} dans la branche ``then'' du test, et \code{x} est de type \code{number} dans la branche ``then'' du test, et
...@@ -185,14 +180,15 @@ Initialement défini pour le langage Scheme pour pouvoir typer des programmes ...@@ -185,14 +180,15 @@ 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é 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 temoignent les langages Hack et Flow et utilisé dans l'industrie (en temoignent les langages Hack et Flow
développés par Facebook et Typescript développé par Microsoft) car il est développés par Facebook et Typescript développé par Microsoft) car il est
indispensable pour pourvoir analyser des patterns de programmation indispensable pour pourvoir analyser du code typiquement écrit dans
typiquement utilisés en programmation en langages dynamiques. ces langages de programmation en langages dynamiques.
\paragraph{Types ensemblistes:} \paragraph{Types ensemblistes:}
comme nous venons de voir les types ensemblistes sont intimement liés comme nous venons de le voir, les types ensemblistes sont intimement liés
à l'occurrence typing. Le type que on déduira pour la fonction à \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 \code{foo} sera \code{number|string $\to$ number|string}: une fonction
qui mappe un type union dans le même type union. Nous avons aussi déjà vu 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 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 branche ``else'' l'occurrence de \code{x} n'est pas de type
\code{number} cela signifie qu'elle est de type \code{number} cela signifie qu'elle est de type
...@@ -205,14 +201,14 @@ pourrait aussi utiliser un type intersection pour donner un type bien ...@@ -205,14 +201,14 @@ pourrait aussi utiliser un type intersection pour donner un type bien
plus précis à \code{foo} tel plus précis à \code{foo} tel
\code{(number$\to$number)\&(string$\to$string)} qui capture le fait \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 que \code{foo} appliquée à un entier renvoie un entier et qu'appliquée
à une chaine de caractères renvoie une chaine de caractères. On parle à une chaîne de caractères renvoie une chaîne de caractères. On parle
dans ce cas de polymorphisme ``ad hoc'', car dans ce cas de polymorphisme ``ad hoc'', car
il permet de typer des fonctions surchargées (en anglais il permet de typer des fonctions surchargées (en anglais
\emph{overloaded functions}) qui executent du code different sur des \emph{overloaded functions}) qui executent du code different sur des
arguments de types différents. arguments de types différents.
\paragraph{Typage graduel et inférence de types:} \paragraph{Typage graduel et inférence de types:}
nous avons déjà vu qu'une certaine dose de inférence de types est 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 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$ 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 number|string} ou, ce qui est encore plus difficile à déduire, de
...@@ -224,7 +220,8 @@ possibilité de mélanger des zones du programme typées statiquement avec ...@@ -224,7 +220,8 @@ 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} 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 qui permet d'annoter certaines parties du programme par un type inconnu
\dyn, qui signale au compilateur que le typage statique peut être \dyn, qui signale au compilateur que le typage statique peut être
relâché au cout d'un contrôle dynamique des types. Par exemple la 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: fonction \code{foo} pourrait être définie comme:
\begin{alltt} \begin{alltt}
function foo(x:\dyn) \{ function foo(x:\dyn) \{
...@@ -239,11 +236,13 @@ est liée à une chaine de caractères. ...@@ -239,11 +236,13 @@ est liée à une chaine de caractères.
\paragraph{Polymorphisme paramétrique:} le polymorphisme paramétrique \paragraph{Polymorphisme paramétrique:} le polymorphisme paramétrique
est désormais un outil incontournable dans un langage de programmation moderne pour est désormais un outil incontournable dans un langage de programmation
pouvoir programmer de manière générique et modulaire. \gcnote{Pas génial} 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 C++.
Un simple exemple de cette nécessitée peut être obtenu en Un simple exemple de cette nécessitée peut être obtenu en
modifiant légèrement le code de \code{foo} de façon que la branche modifiant légèrement le code de \code{foo} de façon à ce que la branche
``else'' renvoie l'argument inchangé: ``else'' renvoie l'argument inchangé:
\begin{alltt} \begin{alltt}
function foo(x) \{ function foo(x) \{
...@@ -278,12 +277,16 @@ A l'instar du polymorphisme paramétrique, les types récursifs, les ...@@ -278,12 +277,16 @@ A l'instar du polymorphisme paramétrique, les types récursifs, les
effets et les fonctions d'ordre supérieure sont des caractéristiques effets et les fonctions d'ordre supérieure sont des caractéristiques
importantes dans un langage de programmation moderne. Ici il ne s'agit importantes dans un langage de programmation moderne. Ici il ne s'agit
pas de trouver des nouvelles fonctionnalités mais d'étudier comment pas de trouver des nouvelles fonctionnalités mais d'étudier comment
intégrer ces caractéristiques avec celle énoncées ci dessus. intégrer ces caractéristiques avec celle énoncées ci dessus. En effet,
\gcnote{developper?} chacun des traits cités interragit de manière subtile avec le système
de type et la sémantique du langage. Par exemple, les effets impose un
ordre d'évaluation et demande d'imposer certaines restrictions sur le
polymorphisme pour garantir la sûreté du typage.
\paragraph{Raffinement de types:} \paragraph{Raffinement de types:}
nous avons déjà montré deux ex amples de raffinent de types: le typage nous avons déjà montré deux exemples de raffinent de types: le typage
d'occurrence permet de raffiner le type des occurrences d'une d'occurrences permet de raffiner le type des occurrences d'une
expression de manière différente dans les branches d'un test; une expression de manière différente dans les branches d'un test; une
meilleure inférence des types permettrait de raffiner le type meilleure inférence des types permettrait de raffiner le type
\code{number|string $\to$ number|string} de \code{foo} dans le type \code{number|string $\to$ number|string} de \code{foo} dans le type
...@@ -301,18 +304,15 @@ raffiner son type par $\{x\in t~|~e\}$ dans la branche ``then'' et ...@@ -301,18 +304,15 @@ raffiner son type par $\{x\in t~|~e\}$ dans la branche ``then'' et
$\{x\in t~|~\neg e\}$ dans la branche ``else''. $\{x\in t~|~\neg e\}$ dans la branche ``else''.
\section{Objectifs}
\subsection{Objectifs}
La plupart de ces sujets ont été étudiés séparément et pour certains La plupart de ces sujets ont été étudiés séparément et pour certains
on a étudié leur combinaison. Mais l’intégration de toutes ses ont été étudiés en combinaison. Mais l’intégration de toutes ses
caractéristiques ensemble dans un langage unique pose de nouveaux caractéristiques dans un langage unique pose de nouveaux
défis qui demandent non seulement des avancées sur chaqun de ces défis qui demandent non seulement des avancées sur chacun d'eux
sujets mais aussi le développement de nouvelles techniques qui en mais aussi le développement de nouvelles techniques qui en
permettent la combinaison. L'inférence de types intersection pour les permettent la combinaison. L'inférence de types intersection pour les
fonctions nécessitera d'une analyse fine que sera fournie par le fonctions nécessitera une analyse fine que sera fournie par le
typage d'occurrence et une analyse de contrôle de flot que on typage d'occurrence et une analyse de contrôle de flot que on
tachera d'intégrer avec cette dernière. Cette analyse pourra aussi 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 être utilisée pour l'intégration des effets. Pour ces derniers nous
...@@ -331,19 +331,15 @@ nombre de contrôles dynamiques. ...@@ -331,19 +331,15 @@ nombre de contrôles dynamiques.
\section{Contexte Sociétal, Économique et Industriel} \section{Contexte Sociétal, Économique et Industriel}
Un résultat immédiat de cette thèse est la possibilité de typer, au Un résultat immédiat de cette thèse est la possibilité de typer, au
moins partiellement, des programmes écrits dans des langages moins partiellement, des programmes écrits dans des langages
dynamiques tels que JavaScript ou Python. En effet, le typage dynamiques tels que JavaScript ou Python. En effet, le typage
d'occurrence et les types ensemblistes permettent d'analyser des d'occurrences et les types ensemblistes permettent d'analyser des
programmes ayant des comportements non-uniformes selon le type de leurs programmes ayant des comportements non-uniformes selon le type de leurs
entrées, ce qui est une caractéristique des langages entrées, ce qui est une caractéristique des programmes écrits dans des langages
dynamiques. L'inférence de type permet de déduire le types de tels dynamiques. L'inférence de type permet de déduire le types de tels
programmes même en l'absence d'annotations de type de la part du programmes même en l'absence d'annotations de types de la part du
programmeur. Enfin, le typage graduel permet de typer partiellement programmeur. Enfin, le typage graduel permet de typer partiellement
des programmes et de circonscrire précisément les parties trop « des programmes et de circonscrire précisément les parties trop «
dynamiques » n'ayant pas pu être analysées. dynamiques » n'ayant pas pu être analysées.
...@@ -356,12 +352,18 @@ pour les statistiques et JavaScript pour la programmation ...@@ -356,12 +352,18 @@ pour les statistiques et JavaScript pour la programmation
Web). L'amélioration de tels langages dans ce contexte est l'un des Web). L'amélioration de tels langages dans ce contexte est l'un des
objectifs de la chaire de recherche « Langages de programmation objectifs de la chaire de recherche « Langages de programmation
Orientés Données » de la fondation Paris-Saclay, portée par K. Nguyen. Orientés Données » de la fondation Paris-Saclay, portée par K. Nguyen.
Cette chaire, financée par une donation d'Oracle Labs. Il est prévu Cette chaire est financée par une donation d'Oracle Labs. Il est prévu
que la chaire prennent entre autre en charge les missions du doctorant que cette chaire soit utilisée pour financer les missions et
ou de la doctorante retenu pour cette thèse. l'équipement du doctorant ou de la doctorante retenu pour cette thèse.
\section{Déroulement de la thèse} \section{Déroulement de la thèse}
\subsection{Encadrement}
La thèse s'effectuera en co-encadrement entre Giuseppe Castagna (DR
CNRS, IRIF, Université de Paris, 50\%) et Kim Nguyen (Maître de
Conférences en Informatique, LRI, équipe VALS, Université
Paris-Saclay, 50\%).
\subsection{Première année} \subsection{Première année}
L'objectif pour la première année est la définition théorique et implémentation L'objectif pour la première année est la définition théorique et implémentation
au sein d'un prototype d'un langage alliant typage d'occurrences, au sein d'un prototype d'un langage alliant typage d'occurrences,
...@@ -380,7 +382,7 @@ langage purement fonctionnel défini lors de la première année. La ...@@ -380,7 +382,7 @@ langage purement fonctionnel défini lors de la première année. La
combinaison entre types ensemblistes, polymorphismes et effets n'a combinaison entre types ensemblistes, polymorphismes et effets n'a
jusqu'à présent jamais été étudiée. Elle pose des problèmes théoriques jusqu'à présent jamais été étudiée. Elle pose des problèmes théoriques
(en particulier, la sûreté du typage avec occurrences repose sur une (en particulier, la sûreté du typage avec occurrences repose sur une
notion de « réduction parallèle » des sous-termes syntaxiquement notion de « réductions parallèles » des sous-termes syntaxiquement
identiques, qui n'est plus possible dès lors que le langage est identiques, qui n'est plus possible dès lors que le langage est
impur). Une piste à explorer est l'utilisation d'effets algébriques, impur). Une piste à explorer est l'utilisation d'effets algébriques,
introduits par Plotkin \emph{et al}. \cite{PlotkinP03, PlotkinP13} qui introduits par Plotkin \emph{et al}. \cite{PlotkinP03, PlotkinP13} qui
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment