Commit 2179a668 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

last pass

parent 15c99916
...@@ -91,7 +91,7 @@ ...@@ -91,7 +91,7 @@
Cette thèse s'inscrit dans la thématique des langages de programmation Cette thèse s'inscrit dans la thématique des langages de programmation
et en particulier dans celle des langages de programmation et en particulier dans celle des langages de programmation
statiquement typés. Dans un tel langage, des règles de typage statiquement typés. Dans des tels langages, des règles de typage
permettent de garantir l'absence de certaines classes d'erreurs à permettent de garantir l'absence de certaines classes d'erreurs à
l'exécution. 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
...@@ -99,8 +99,8 @@ demande que l'opérateur de soustraction ne soit \emph{bien typé} que ...@@ -99,8 +99,8 @@ 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 essayerait 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 et qui décrivent sont des objets associés aux expressions et aux valeurs du langage et ils en décrivent
leur domaine. Par exemple le type \texttt{Int} associé au constantes le 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.
...@@ -120,7 +120,9 @@ l'implantation du langage CDuce \cite{BCF03}. Ce dernier est un ...@@ -120,7 +120,9 @@ l'implantation du langage CDuce \cite{BCF03}. Ce dernier est un
langage fonctionnel statiquement typé, muni de types ensemblistes et langage fonctionnel statiquement typé, muni de types ensemblistes et
de polymorphisme. 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 de programmation avancée suivantes:
\begin{enumerate} \begin{enumerate}
\item typage d'occurrences \item typage d'occurrences
...@@ -173,12 +175,12 @@ de manière différente dans chaque branche du test: puisque le programme a test ...@@ -173,12 +175,12 @@ 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 \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 de cela et du fait qu'il doit être ou \code{number} ou \code{string} déduire (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 dernière branche). 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 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 témoignent 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 du code typiquement écrit dans indispensable pour pourvoir analyser du code typiquement écrit dans
ces langages de programmation en langages dynamiques. ces langages de programmation en langages dynamiques.
...@@ -204,7 +206,7 @@ que \code{foo} appliquée à un entier renvoie un entier et qu'appliquée ...@@ -204,7 +206,7 @@ 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 à 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 exécutent du code différent 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:}
...@@ -239,7 +241,7 @@ est liée à une chaine de caractères. ...@@ -239,7 +241,7 @@ est liée à une chaine de caractères.
est désormais un outil incontournable dans un langage de programmation 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 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} fonctionnalité se retrouve en effet sous le nom de \emph{generics}
dans le langage Java ou encore \emph{template} dans le langage C++. 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é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 à ce que la branche modifiant légèrement le code de \code{foo} de façon à ce que la branche
...@@ -249,11 +251,11 @@ modifiant légèrement le code de \code{foo} de façon à ce que la branche ...@@ -249,11 +251,11 @@ modifiant légèrement le code de \code{foo} de façon à ce que la branche
(typeof(x) === "number")? x++ : x (typeof(x) === "number")? x++ : x
\} \}
\end{alltt} \end{alltt}
dans ce cas il est clair que, independamment du resultat du test de dans ce cas il est clair que, indépendamment du résultat du test de
type, \code{foo} renvoie toujours un résultat type, \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$ (même si ce types est polymorphe $\forall\alpha.\alpha\to\alpha$ (même si ce type est
typique de langages de la famille \texttt{ML}, la présence du test de distinctif des langages de la famille \texttt{ML}, la présence du test de
type rend nécessaire type rend nécessaire
l'expressivité des types ensemblistes pour pouvoir le déduire pour l'expressivité des types ensemblistes pour pouvoir le déduire pour
cette fonction). Mais il se peut que le cette fonction). Mais il se peut que le
...@@ -273,15 +275,20 @@ il renvoie un résultat du même type. ...@@ -273,15 +275,20 @@ il renvoie un résultat du même type.
\paragraph{Types récursifs, effets et ordre supérieur:} \paragraph{Types récursifs, effets et ordre supérieur:}
A l'instar du polymorphisme paramétrique, les types récursifs, les 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, à l'instar du
polymorphisme paramétrique, 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. En effet, intégrer ces caractéristiques avec celles énoncées ci dessus. En effet,
chacun des traits cités interragit de manière subtile avec le système chacun des traits cités interagit de manière subtile avec le système
de type et la sémantique du langage. Par exemple, les effets impose un 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 ordre d'évaluation et demande d'imposer certaines restrictions sur le
polymorphisme pour garantir la sûreté du typage. polymorphisme pour garantir la sûreté du typage. En 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:} \paragraph{Raffinement de types:}
...@@ -292,11 +299,11 @@ meilleure inférence des types permettrait de raffiner le type ...@@ -292,11 +299,11 @@ 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
\code{(number$\to$number)\&(string$\to$string)} qui est bien plus \code{(number$\to$number)\&(string$\to$string)} qui est bien plus
précis On voudrait ajouter la possibilité de raffiner les types du précis On voudrait ajouter la possibilité de raffiner les types du
langages par le biais de propositions logique.s Par exemple on voudrait langages par le biais de propositions logiques. Par exemple on voudrait
définir le type des nombres impairs comme il suit $\texttt{Odd} = \{ 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 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 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 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 combinaison avec les types ensemblistes pour généraliser le typage
d'occurrence: si nous avons un test sur une expression booléenne $e$ 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 et $x$ est une variable libre dans $e$ de type $t$ alors on pourrait
...@@ -322,7 +329,7 @@ L'inférence de type polymorphe sera basée sur la génération d'ensembles ...@@ -322,7 +329,7 @@ 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 de contraintes dont la solution utilisera les types récursifs et les
types ensemblistes. Le typage d'occurrence n'est actuellement utilisé types ensemblistes. Le typage d'occurrence n'est actuellement utilisé
que dans des car très particuliers (des tests des types sur des que dans des car très particuliers (des tests des types sur des
variables); il faudra le generaliser à des tests quelconques de types, variables); il faudra le généraliser à des tests quelconques de types,
en utilisant l'expressivité logique donnée par les types ensemblistes en utilisant l'expressivité logique donnée par les types ensemblistes
et pour le combiner avec des types polymorphes. On l'étendra ensuite à 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 la présence d'effets. Le typage d'occurrence sera ensuite utilisé pour
......
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