Commit 80c23046 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more

parent 623be6ab
......@@ -31,8 +31,10 @@
% Please use \hhnote etc... for comments, feel free to tweak to your
% liking.
\usepackage{fixme}
\fxsetup{theme=color,mode=multiuser}
\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}
......@@ -145,29 +147,30 @@ Nous allons montrer par des exemples l'intérêt de chaque caractéristique:
\paragraph{Typage d'occurrence:}
Le typage de occurrence, ou \emph{occurrence typing}, est une technique
qui analyse les test effectués par un programme afin de pouvoir raffiner
l'analyses de types dans le code à exécuter en cas de réussite ou
d'échec du test. Un exemple d'application du typage d'occurrence est donné par le
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'occurrence est donné par le
code JavaScript suivant
\begin{alltt}
function foo(x) {
function foo(x) \{
(typeof(x) === "number")? x++ : x.trim()
}
\}
\end{alltt}
Dans ce code on teste si l'argument liée à \code{x} de la fonction \code{foo} est de type
Dans ce code on teste si l'argument de la fonction
\code{foo} liée à \code{x} est de type
\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 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 élimines les espaces
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 de type \code{number} ou
\code{string}. C'est à dire il doit avoir le type ``union''
\code{number|string}. Dans les
systèmes de types standard cette information n'est pas suffisante pour
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
standard 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
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
......@@ -175,7 +178,7 @@ de manière différente dans chaque branche du test: puisque le programme a test
\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
qu'il est de type \code{string} dans cette branche).
qu'il est de type \code{string} dans cette dernière branche).
Initialement défini pour le langage Scheme pour pouvoir typer des programmes
......@@ -183,7 +186,7 @@ Scheme non typés~\cite{THF08,THF10}, le typage d'occurrence est de plus en plus
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
indispensable pour pourvoir analyser des patterns de programmation
typiquement utilisés en programmation en langages dynamiques.
typiquement utilisés en programmation en langages dynamiques.
\paragraph{Types ensemblistes:}
comme nous venons de voir les types ensemblistes sont intimement liés
......@@ -209,24 +212,24 @@ il permet de typer des fonctions surchargées (en anglais
arguments de types différents.
\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à vu qu'une certaine dose de 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 une tel déduction
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âche au cout d'un contrôle dynamique des types. Par exemple la
relâché au cout d'un contrôle dynamique des types. Par exemple la
fonction \code{foo} pourrait être définie comme:
\begin{alltt}
function foo(x:\dyn) {
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 à
......@@ -237,26 +240,31 @@ 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 moderne pour
pouvoir capturer ...
pouvoir programmer de manière générique et modulaire. \gcnote{Pas génial}
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
``else'' renvoie l'argument inchangé:
\begin{alltt}
function foo(x) {
function foo(x) \{
(typeof(x) === "number")? x++ : x
}
\}
\end{alltt}
dans ce cas il est clair que \code{foo} renvoie toujours un résultat
dans ce cas il est clair que, independamment du resultat 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$. Mais il se peut que le
polymorphe $\forall\alpha.\alpha\to\alpha$ (même si ce types est
typique de 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) {
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
......@@ -266,23 +274,23 @@ 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
A l'instar du polymorphisme paramétrique, 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?]
\gcnote{developper?}
\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
d'occurrence 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
langages par le biais de proposition logique. Par exemple on voudrait
définir le type de nombre impair comme il suit $\texttt{Odd} = \{
langages par le biais de propositions logique.s 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} 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
......@@ -301,19 +309,25 @@ $\{x\in t~|~\neg e\}$ dans la branche ``else''.
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
défis qui demandent non seulement des avancées sur chaqun de ces
sujets mais aussi le développement de nouvelles techniques qui en
permettent la combinaison. L'inférence de types intersection pour les
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
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
être utilisée pour al gestion des effets. Pour ces derniers nous
être utilisée pour l'intégration 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.
combinant avec l'expressivité logique des types ensemblistes.
L'inférence de type polymorphe sera basée sur la génération d'ensembles
de contraintes dont la solution utilisera les types récursifs et les
types ensemblistes. Le typage d'occurrence n'est actuellement utilisé
que dans des car très particuliers (des tests des types sur des
variables); il faudra le generaliser à des tests quelconques de types,
en utilisant l'expressivité logique donnée par les types ensemblistes
et pour le combiner avec des types polymorphes. On l'étendra ensuite à
la présence d'effets. Le typage d'occurrence sera ensuite utilisé pour
optimiser la compilation de systèmes graduels afin de réduire le
nombre de contrôles dynamiques.
......
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