Commit 51edc655 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents 7c8c08b8 f13486b0
......@@ -95,22 +95,28 @@ 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 essayerai de soustraire un tableau et une
erreurs du programmeur qui essayerais de soustraire un tableau et une
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
leur domaine. Par exemple le type \texttt{Int} associé au constantes
\texttt{1}, \texttt{2}, \ldots indique que de telles valeurs sont des
entiers.
De nombreux langages définissent en plus des types une relation de
\emph{sous-typage} entre les types. Informellement, cette dernière
indique que les valeurs d'un sous-type sont aussi des valeurs d'un
type plus général. Par exemple, dire que le type \texttt{Int} des
entiers est un sous-type du type \texttt{Real} des nombres réels
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
tel système, les types ne sont pas simplement des objets syntaxiques
utilisé 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 ensembliste d'union, d'intersection ou de
complémentaire, traditionnellement absent des langages de
programmation généralistes.
Une première étape dans la théorie et conception des langages de
programmation à types ensembliste a été la définition et
l'implantation du langage CDuce \cite{}.
Dans la théorie des langages de programmation typés la notion de
\emph{sous-typage} joue un rôle important. Elle peut être
......@@ -266,6 +272,54 @@ sur chaqun de ses sujets mais ...
\section{Contexte Sociétal, Économique et Industriel}
Un résultat immédiat de cette thèse est la possibilité de typer, au
moins partiellement, des programmes écrits dans des langages
dynamiques tels que JavaScript ou Python. En effet, le typage
d'occurrence et les types ensemblistes permettent d'analyser des
programmes ayant des comportements non-uniformes selon le type de leurs
entrées, ce qui est une caractéristique des langages
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
programmeur. Enfin, le typage graduel permet de typer partiellement
des programmes et de circonscrire précisément les parties trop «
dynamiques » n'ayant pas pu être analysées.
Cette analyse statique de langages dynamiques est particulièrement
importante dans le contexte actuel de la science des données. En
effet, les langages de choix des analystes de données sont usuelement
des langages dynamiques (en particulier Python pour la physique, R
pour les statistiques et JavaScript pour la programmation
Web). L'amélioration de tels langages dans ce contexte est l'un des
objectifs de la chaire de recherche « Langages de programmation
Orientés Données » de la fondation Paris-Saclay, portée par K. Nguyen.
Cette chaire, financée par une donnation d'Oracle Labs. Il est prévu
que la chaire prennent entre autre en charge les missions du doctorant
ou de la doctorante retenu pour cette thèse.
\section{Déroulement de la thèse}
\subsection{Première année}
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,
sous-typage sémantique polymorphisme et inférence de
types. Les points d'attention dans ce premier pan de la recherche sont
en particulier la définition formelle du langage, qui devra être
suffisemment modulaire pour être étendue avec d'autres aspects, un
cadre théorique permettant la définition d'heuristiques et leur
expérimentation pour l'inférence de types et un implémentation
raisonnablement efficace (en particulier de l'algorithme de génération
de contraintes pour le typage polymorphe).
\subsection{Deuxième année}
L'objectif, ambitieux, est l'intégration d'un système d'effets au
langage purement fonctionnel défini lors de la première année. La
combinaison entre types ensemblistes, polymorphismes et effets n'a
jusqu'à présent jamais été étudiée.
\end{document}
%%% Local Variables:
......
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