Commit 61c4ba05 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

new version

parent ad8d1bea
...@@ -122,7 +122,7 @@ l'implantation du langage CDuce \cite{}. ...@@ -122,7 +122,7 @@ l'implantation du langage CDuce \cite{}.
Le but the cette thèse est d'arriver à définir et étudier un langage de programmation fonctionnel statiquement typé qui combine les characteristiques 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 avancée suivantes:
\begin{enumerate} \begin{enumerate}
\item typage d'occurrence \item typage d'occurrence
...@@ -131,63 +131,64 @@ Le but the cette thèse est d'arriver à définir et étudier un langage de prog ...@@ -131,63 +131,64 @@ Le but the cette thèse est d'arriver à définir et étudier un langage de prog
\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 recursifs \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 characteristique: Nous allons montrer par des exemples l'intérêt de chaque caractéristique:
\paragraph{Typage d'occurrence:} \paragraph{Typage d'occurrence:}
Le typage de occurrence, ou \emph{occurrence typing} est un technique Le typage de occurrence, ou \emph{occurrence typing} est un technique
qui analyse les test effectués par un programme pour pouvoir raffiner qui analyse les test effectués par un programme pour pouvoir raffiner
l'analyses de types dans le code à executer en cas de reussite ou l'analyses de types dans le code à exécuter en cas de réussite ou
d'échec du test. Un example d'application du typage d'occurrence est donné par le d'échec du test. Un exemple d'application du typage d'occurrence est donné par le
code suivant JavaScript code suivant JavaScript
\begin{alltt} \begin{alltt}
function foo(x) { function foo(x) {
(typeof(x) === "number")? x++ : x.trim() (typeof(x) === "number")? x++ : x.trim()
} }
\end{alltt} \end{alltt}
Dans ce code on teste si l'argument de la fonction \code{x} et de type Dans ce code on teste si l'argument de la fonction \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 lui envoie le message \code{trim()}. Puisque \code{trim} est une on lui envoie 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}
(c'est une méthode du standard ECMAScript 5 qui elimines les espeace (c'est une méthode du standard ECMAScript 5 qui élimines les espaces
au debut et à la fin d'une chaine de caractères) on peut facilement au début et à la fin d'une chaine de caractères) on peut facilement
déduire que l'argument de \code{foo} doit être ou un \code{number} ou déduire que l'argument de \code{foo} doit être de type \code{number} ou
un \code{string}. C'est à dire il doit avoir le type \code{string}. C'est à dire il doit avoir le type
\code{number|string}. Cette information n'est pas suffisante dans le \code{number|string}. Dans les
systèmes de types standard pour typer la fonction \code{foo} car systèmes de types standard cette information n'est pas suffisante pour
\code{trim()} n'est pas défini pour \code{numbers} et \code{++} n'est pouvoir typer la fonction \code{foo} car
\code{trim()} n'est pas défini pour \code{number} et \code{++} n'est
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
standard ne prennent pas en compte le test de type effectué sur standard 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écializer le type des occurrences de \code{x} dans information pour spécialiser le type des occurrences de \code{x} dans
les differentes branches du test: puisque le programme à 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 branch ``then'' du test, et \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'' qu'il \emph{n'est pas} de type \code{number} dans la branche ``else''
et du fait qu'il doit être ou \code{number} ou \code{string} déduire et du fait qu'il doit être ou \code{number} ou \code{string} déduire
qu'il est de type \code{string} dans cette branche. qu'il est de type \code{string} dans cette branche.
Initialement défini pour Scheme pour pouvoir typer des programme Initialement défini pour le langage Scheme pour pouvoir typer des programme
Schemes non typés\cite{THF08,THF10}, il est de plus en plus développé Scheme non typés\cite{THF08,THF10}, il est de plus en plus développé
et utilisé dans l'industrie (Hack, Typescript, Flow) car il est et utilisé dans l'industrie (Hack, Typescript, Flow) car il est
indispensable pour pourvoir analyser des patterns de programmation indispensable pour pourvoir analyser des patterns de programmation
typiques de la programmation en langages dynamiques. typiquement utilisé en programmation par des langages dynamiques.
\paragraph{Types ensemblistes:} \paragraph{Types ensemblistes:}
comme nous vénons de voir les types ensemblistes sont intimement liés comme nous venons de voir les types ensemblistes sont intimement liés
à l'occurrence typing. Le type que on déduira pour la fonction à l'occurrence typing. Le type que 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 un type union. Nous avons aussi déjà vu qui mappe un type union dans un type union. Nous avons aussi déjà vu
l'utilisation du type negation: 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
\code{$\neg$number}. Et puisque \code{x} doit aussi avoir le type \code{$\neg$number}. Et puisque \code{x} doit aussi avoir le type
...@@ -198,8 +199,8 @@ branche ``else'' l'occurrence de \code{x} n'est pas de type ...@@ -198,8 +199,8 @@ branche ``else'' l'occurrence de \code{x} n'est pas de type
pourrait aussi utiliser un type intersection pour donner un type bien 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é à un entier renvoie un entrier et qu'appliquée que \code{foo} appliquée à un entier renvoie un entier et qu'appliquée
à une chaine de caaractères renvoie une chaine de caractères. à une chaine de caractères renvoie une chaine de caractères.
\paragraph{Typage graduel et inférence de types:} \paragraph{Typage graduel et inférence de types:}
nous avons déjà vous que une certaine dose de inférence de types est nous avons déjà vous que une certaine dose de inférence de types est
...@@ -207,64 +208,106 @@ nécessaire: la fonction \code{foo} n'a pas d'annotation de type mais ...@@ -207,64 +208,106 @@ 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
type \code{(number$\to$number)\&(string$\to$string)}. Si la première type \code{(number$\to$number)\&(string$\to$string)}. Si la première
deduction est déjà possible, la deuxième le sera surement grâce aux 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 une tel déduction techniques développés dans cette thèse. Toutefois une tel déduction
n'est pas toujours possible, c'est pourquoi il faudra avoir la n'est pas toujours possible, c'est pourquoi il faudra avoir la
possibilité de mélanger de zone du programme typés statiquement avec possibilité de mélanger des zones du programme typées statiquement avec
d'autres zones types. 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 certaine partie du programme par un type inconnu qui permet d'annoter certaines parties du programme par un type inconnu
\dyn, qui signale au compilateur que du typage statique peut être \dyn, qui signale au compilateur que le typage statique peut être
relaché au cout d'un controôle dynamique des types. Par example la relâche au cout d'un contrôle dynamique des types. Par exemple la
fonction \code{foo} pourrait définie comme: fonction \code{foo} pourrait être définie comme:
\begin{alltt} \begin{alltt}
function foo(x:\dyn) { function foo(x:\dyn) {
(typeof(x) === "number")? x++ : x.trim() (typeof(x) === "number")? x++ : x.trim()
} }
\end{alltt} \end{alltt}
elle serait donc typé par \code{\dyn$\to$(number|string)} mais le elle serait donc typée par \code{\dyn$\to$(number|string)} et le
compilateur introduirait de test dynamique qui controleraient à compilateur introduirait des tests dynamiques qui contrôleraient à
l'execution que lors de l'execution de \code{x++} la variable est liée lexécution que lors de lexécution de \code{x++} la variable est liée
à un entier et que lors de l'exécution de \code{x.trim()} la variable à un entier et que lors de l'exécution de \code{x.trim()} la variable
est liée à une chaine de caractères. est liée à une chaine de caractères.
\paragraph{Polymorphisme parametrique:} le polymorphisme parametrique \paragraph{Polymorphisme paramétrique:} le polymorphisme paramétrique
est desormais nécessaire dans un langage de programmation moderne pour est désormais un outil incontournable dans un langage de programmation moderne pour
typer ... pouvoir capturer ...
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 legèrement le code de \code{foo} de façon que la brabch modifiant légèrement le code de \code{foo} de façon que la branche
``else'' renvoie l'argument inchangée: ``else'' renvoie l'argument inchangé:
\begin{alltt} \begin{alltt}
function foo(x) { function foo(x) {
(typeof(x) === "number")? x++ : x (typeof(x) === "number")? x++ : x
} }
\end{alltt} \end{alltt}
dans ce cas il est clair que \code{foo} renvoie toujours un resultat dans ce cas il est clair que \code{foo} renvoie toujours un résultat
qui a le même type que l'argument. Ceci est exprimé par le type qui a le même type que l'argument. Ceci est exprimé par le type
polymorphe $\forall\alpha.\alpha\to\alpha$. Mais il se peut que le polymorphe $\forall\alpha.\alpha\to\alpha$. Mais il se peut que le
polymorphisme parametrique doive se combiner avec les caracteristique polymorphisme paramétrique doive se combiner avec les caractéristiques
précédente. Si par exemple la branche ``then'' teste si l'argument est précédentes. Si par exemple la branche ``then'' teste si l'argument est
égal à 42 égal à 42
\begin{alltt} \begin{alltt}
function foo(x) { function foo(x) {
(typeof(x) === "number")? (x==42) : x (typeof(x) === "number")? (x==42) : x
} }
\end{alltt} \end{alltt}
alor le type que on veut déduire pour cette fonction est: 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 $\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 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} booléen, sinon s'il est applique à un type qui n'est pas \code{number}
il renvoie un resultat du même type. il renvoie un résultat du même type.
\paragraph{Types récursifs, effets et ordre supérieur:}
comme le polymorphisme paramétrique, ainsi les types récursifs les
effets et les fonctions d'ordre supérieure sont 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 celle énoncées ci dessus.
[developper?]
CHALLENGES \paragraph{Raffinement de types:}
nous avons déjà montré deux ex amples de raffinent de types: le typage
d'occurrence permet de raffiner le type des occurrence 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
langages par le biais de proposition logique. Par exemple on voudrait
définir le type de nombre impair comme il suit $\texttt{Odd} = \{
x\in\texttt{Int}~|~x\mod 2 = 1\}$: \texttt{Odd} est 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 de 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 $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''.
Tous ces sujets ont été étudiés separament ainsi que pour certains
leur combinaison. Mais l'integration de toutes ses characteristiques
ensemble pose de nouveaux défis qui demande non seulment des avances
sur chaqun de ses sujets mais ...
\subsection{Objectifs}
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
caractéristiques ensemble dans un langage unique pose de nouveaux
défis qui demandent non seulement des avances sur chaque de ses sujets
mais sur leur combinaison. L'inférence de types intersection pour le
fonctions nécessitera d'une analyse fine que sera fournie par le
typage des occurrence et une analyse de contrôle de flot que on
tachera d'intégrer avec cette dernière. Cette analyse pourra aussi
être utilisée pour al gestion des effets. Pour ces derniers nous
envisageons d'utiliser les travaux sur les effets algébriques en le
combinant avec l'expressivité logiques des types
ensemblistes L'inférence de type polymorphe sera basée sur la
génération d'ensemble de contraintes dont la solution utilisera les
types récursifs et les types ensemblistes. Le typage d'occurrence sera
utilisé pour optimiser la compilation de systèmes graduels afin de
réduire le nombre de contrôles dynamiques.
...@@ -287,13 +330,13 @@ dynamiques » n'ayant pas pu être analysées. ...@@ -287,13 +330,13 @@ dynamiques » n'ayant pas pu être analysées.
Cette analyse statique de langages dynamiques est particulièrement Cette analyse statique de langages dynamiques est particulièrement
importante dans le contexte actuel de la science des données. En importante dans le contexte actuel de la science des données. En
effet, les langages de choix des analystes de données sont usuelement effet, les langages de choix des analystes de données sont usuellement
des langages dynamiques (en particulier Python pour la physique, R des langages dynamiques (en particulier Python pour la physique, R
pour les statistiques et JavaScript pour la programmation 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 donnation d'Oracle Labs. Il est prévu Cette chaire, 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 la chaire prennent entre autre en charge les missions du doctorant
ou de la doctorante retenu pour cette thèse. ou de la doctorante retenu pour cette thèse.
...@@ -305,7 +348,7 @@ au sein d'un prototype d'un langage alliant typage d'occurrences, ...@@ -305,7 +348,7 @@ au sein d'un prototype d'un langage alliant typage d'occurrences,
sous-typage sémantique polymorphisme et inférence de sous-typage sémantique polymorphisme et inférence de
types. Les points d'attention dans ce premier pan de la recherche sont types. Les points d'attention dans ce premier pan de la recherche sont
en particulier la définition formelle du langage, qui devra être en particulier la définition formelle du langage, qui devra être
suffisemment modulaire pour être étendue avec d'autres aspects, un suffisamment modulaire pour être étendue avec d'autres aspects, un
cadre théorique permettant la définition d'heuristiques et leur cadre théorique permettant la définition d'heuristiques et leur
expérimentation pour l'inférence de types et un implémentation expérimentation pour l'inférence de types et un implémentation
raisonnablement efficace (en particulier de l'algorithme de génération raisonnablement efficace (en particulier de l'algorithme de génération
......
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